The use of functional annotations in verifying imperative programs

Functional programming languages have been advocated as a means for writing more reliable programs, although imperative programming languages permit more efficient execution on conventional computer hardware. The authors advocate a means of using a functional notation to annotate imperative programs and present a method for verifying that the annotated sections of code achieve the results specified in the annotation. Examples are given to show how the method is used. These demonstrate that this approach to program correctness leads to verification conditions which are briefer, but more numerous, than those which result from verifying more conventionally annotated programs. A goal of the article is to provide a technique to facilitate the activity of operational decomposition in a formal method in which refinements of specifications to implementations are made