Polyspace客户端™ 用于Ada和Polyspace服务器™ 对于Ada，提供代码验证，证明源代码中没有溢出、被零除、越界数组访问和某些其他运行时错误。他们使用静态代码分析不需要程序执行、代码检测或测试用例。Ada使用的Polyspace产品s manbetx 845形式化方法一种称为抽象解释以验证代码的技术。在运行时验证结果中，对每个Ada操作进行颜色编码，以指示它是否没有运行时错误、被证明失败、无法访问或未经验证，如下所示：

• 绿色：证明没有运行时错误
• 红色：每次执行操作时都被证明有故障
• 灰色：已证明无法访问（可能表示功能问题）
• 橙色：未经验证的所有运行时条件

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

Polyspace for Ada可帮助您：

• 检测难以发现的运行时错误和正式证明它们在Ada源代码中的缺失
• 轨道软件质量度量并确保软件质量目标满足
• 查看范围信息确定变量、函数参数和返回值的范围
• 关注运行时错误与以前的验证结果之间的差异
• 创建工件以根据标准（如DO-178）进行认证