PolySpace™ Client™ for Ada 5.1.1

Product Description

• Introduction and Key Features
• Working with PolySpace Client for Ada
• Verifying Program Dynamics
• Typical Run-Time Errors Detected

Verifying Program Dynamics

Static analyzers, which return only a small number of significant warnings, and dynamic testing, which uses a very small number of test cases, can miss many errors, reducing your level of confidence in the code.

PolySpace products for Ada bridge the gap between these two approaches. They verify all executions of each instruction, taking into account all the possible values of every variable at every point in the code. They then provide a formal diagnostic for each operation in the code, as follows:

Green: Proven reliable under all operating conditions
Red: Proven faulty each time the operation is executed
Grey: Proven unreachable (may indicate a functional issue)
Orange: Unproven code section (a run-time error might occur under certain operating conditions)

By thoroughly examining program dynamics, PolySpace products for Ada prove the presence or absence of run-time errors, regardless of coding technique. The percentage of code designated green is an indicator of source-code reliability that you can use to set quality objectives.