用于Ada的Polyspace客户机™和用于Ada的Polyspace服务器™提供了代码验证，可以证明源代码中没有溢出、除零、数组越界访问和某些其他运行时错误。他们使用静态代码分析它不需要程序执行、代码插装或测试用例。Polyspace s manbetx 845Ada产品正式的方法技术称为抽象解释验证代码。在运行时验证结果中，每个Ada操作都用颜色编码，以表明其是否没有运行时错误、已证明失败、不可到达或未被证明，如下:

• 绿色:已证明没有运行时错误
• 红色的:每次执行操作时都被证明是错误的
• 灰色的:被证明无法到达(可能表明功能问题)
• 橙色:对所有运行时条件未经证明

Ada的Polyspace服务器允许您安排验证任务在计算机集群上运行。对于Ada，使用Polyspace客户机将作业提交到服务器。您可以将作业集成到自动构建过程中，并设置电子邮件通知。您可以通过Web浏览器查看缺陷和回归。

Polyspace for Ada帮助您:

• 检测难以找到运行时错误和正式的证明它们在Ada源代码中的缺失
• 跟踪软件质量度量并确保你的软件质量目标得到满足
• 视图范围的信息确定变量、函数参数和返回值的范围
• 关注与以前的验证结果相比，运行时错误的差异
• 创建用于认证标准(如DO-178)的工件