Verification of loops and exceptions
Ryan D. Stansifer · Purdue e-Pubs (Purdue University System) · 1986
We give a proof rule for a multiple-level exit construct not unlike the loopexit statement in the ADA* programming language.We give a novel, yet simple, semantics for the loop-exit with which we can prove that the rule is both sound and (relatively) complete in the logic of Hoare triples.Hence, we can be satisfied that the proof rule is sufficient to prove all true Hoare triples using the multiple-level exit statement and is suitable for inclusion in a formal verification system.A verification condition generator using these rules is developed using a general method based on attribute grammars.