This Article 
 Bibliographic References 
 Add to: 
Programming with Verification Conditions
March 1979 (vol. 5 no. 2)
pp. 148-159
M.H. Van Emden, Department of Computer Science, University of Waterloo
This paper contains an exposition of the method of programming with verification conditions. Although this method has much in common with the one discussed by Dijkstra in A Disciplne of Programming, it is shown to have the advantage in simplicity and flexibility. The simplicity is the result of the method's being directly based on Floyd's inductive assertions The method is flexible becasue of the way in which the program is constructed in two stages. In the first stage, a set of verification conditions is collected which corresponds to a program in "flowgraph" form. In this stage sequencing control is of no concern to the progmmer. Control is introduced in the second stage, which consists of automatable applications of translation and optimization rules, resulting in conventional code. Although our method has no use for the sequencing primitives of "structured programming," it is highly secure and systematic.
Index Terms:
verification, Bottom-up programming, control structure, correctness-oriented progrunming, invariant assertions, structured programming
M.H. Van Emden, "Programming with Verification Conditions," IEEE Transactions on Software Engineering, vol. 5, no. 2, pp. 148-159, March 1979, doi:10.1109/TSE.1979.234171
Usage of this product signifies your acceptance of the Terms of Use.