The Examiner can be requested to generate a set of Verification Conditions or VCs. VCs are used to attempt to establish certain properties hold for a given subprogram. At a minimum, the Examiner will generate VCs attempting to establish that the following run-time errors cannot occur within a subprogram:
- array index out of range
- type range violation
- division by zero
- numerical overflow.
If a postcondition is added to the specification, the Examiner will also generate VCs that require the user to show that the postcondition will hold for all possible paths through the subprogram.
Discharging these proof obligations is performed using the SPADE Simplifier (an automated theorem prover) and the SPADE Proof Checker (a manual theorem prover, used for those VCs too thorny for the Simplifier to automatically discharge).
Read more about this topic: SPARK (programming Language)
Famous quotes containing the words verification and/or conditions:
“Science is a system of statements based on direct experience, and controlled by experimental verification. Verification in science is not, however, of single statements but of the entire system or a sub-system of such statements.”
—Rudolf Carnap (1891–1970)
“... we have every reason to rejoice when there are so many gains and when favorable conditions abound on every hand. The end is not yet in sight, but it can not be far away. The road before us is shorter than the road behind.”
—Lucy Stone (1818–1893)