This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Citation:
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.