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)
“Among the laws controlling human societies there is one more precise and clearer, it seems to me, than all the others. If men are to remain civilized or to become civilized, the art of association must develop and improve among them at the same speed as equality of conditions spreads.”
—Alexis de Tocqueville (1805–1859)