Logical Refinement of Imperative Programs: generating code from verified conditions
Andrew M. Gravell · ePrints Soton (University of Southampton) · 2000
Most program development methods rely on a combination of programming and logical notations. Correctness is verified using refinement laws which often have logical side conditions. Checking these conditions involves a separate proof, breaking up the linear flow of the program derivation. This paper explores a variant of the refinement calculus in which only logical notation is used and the program under development is inferred from formulas which are, in effect, the verification conditions that would arise in a traditional derivation. It is preferable that these are verified first, in which case they should be called verified conditions. A polynomial algorithm exists for extracting the refinement argument, and hence the implementation, from these conditions. A prototype code generation system has been implemented in Prolog. The benefits and weaknesses of the approach are compared to those of more conventional refinement calculi.