Content area
To ably create or modify computer programs that behave according to specification, programmers find it necessary to reason about their programs' behavior. We have formalized, in a direct, natural way, the informal pattern of reasoning generally used with programs written in modular, imperative languages. This formal system provides a solid basis against which to check the soundness and (relative) completeness of an informal reasoning method.
Formal proof that a program meets a specification can be done in this new system or in existing systems (e.g., calculating weakest preconditions using Hoare-style axioms or using symbolic execution). Each system prescribes a way to translate the program-specification pair to a mathematical assertion whose truth implies that the program satisfies the specification. Alternative systems are distinguished, however, by how well they fit programmers' informal reasoning methods. Programmers think of the effect that the execution of a given statement will have on variables' values, and they consider what conditions must hold for those values in each branch of the program. The new method is organized accordingly, unlike previous methods, which are organized for the convenience of mathematicians.