Programming with Verification Conditions

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.