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

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

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

Polyspace for Ada帮助您:

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