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

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

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

Polyspace for Ada帮助你:

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