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:
“A fact is a proposition of which the verification by an appeal to the primary sources of our knowledge or to experience is direct and simple. A theory, on the other hand, if true, has all the characteristics of a fact except that its verification is possible only by indirect, remote, and difficult means.”
—Chauncey Wright (1830–1875)
“If there is a species which is more maltreated than children, then it must be their toys, which they handle in an incredibly off-hand manner.... Toys are thus the end point in that long chain in which all the conditions of despotic high-handedness are in play which enchain beings one to another, from one species to another—cruel divinities to their sacrificial victims, from masters to slaves, from adults to children, and from children to their objects.”
—Jean Baudrillard (b. 1929)