用于Ada的Polyspace Client™和用于Ada的Polyspace Server™提供了代码验证，以证明源代码中不存在溢出、除数为0、数组越界访问和某些其他运行时错误。他们使用静态代码分析这并不需要程序执行、代码插装或测试用例。用于Ada的Poly下载188bet金宝搏space产品正式的方法一种称为抽象解释的技术来验证代码。在运行时验证结果中，每个Ada操作都用不同的颜色编码，以表示它是否没有运行时错误、已被证明失败、不可到达或未被证明，如下所示:

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

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

Polyspace为Ada帮助您:

• 检测难以发现的运行时错误和正式的证明他们的缺席Ada源代码
• 跟踪软件质量度量确保你的软件质量目标得到满足
• 视图范围的信息确定变量、函数参数和返回值的范围
• 关注运行时错误与以前的验证结果之间的差异
• 创建工件以获得DO-178等标准的认证