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

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

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

Polyspace for Ada可帮助您：

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