Overview

program correctness proof


Show Summary Details

Quick Reference

A formal mathematical demonstration that the semantics of a program are consistent with some specification for that program (see program specification). There are two prerequisites to the provision of such a proof: there must be a formal specification for the program, and there must be some formal definition of the semantics of the programming language. Such a definition may take the form of a set of axioms to cover the semantics of any simple statement in the language, and a set of inference rules that show how the semantics of any compound statement, including a complete program, can be inferred from the semantics of its individual component statements (simple or compound).

For a typical sequential program written in some imperative (procedural) language, the program specification can conveniently be given in the form of two assertions: an input assertion and an output assertion. These are expressed in terms of properties of certain program variables and relationships between them. The proof then consists of a formal demonstration that the semantics of the program are consistent with the input and output assertions; this demonstration is of course based upon the formal definition of the semantics of the programming language. Interpreted operationally, the assertions characterize program states and the proof shows that if execution of the program is initiated in a state for which the input assertion is “true” then the program will eventually terminate in a state for which the output assertion is “true”.

This kind of proof is known as a proof of total correctness. Historically, however, such a proof has often been resolved into two parts: first, a proof of partial correctness, which shows that if the program terminates then it does so in a state for which the output assertion is “true”, and second, a proof of termination, which shows that the program will indeed terminate (normally rather than abnormally).

A common approach to the proof of partial correctness begins by attaching the input and output assertions to the program text at the very beginning and very end respectively. Further assertions, called intermediate assertions, are attached to the program text both before and after every statement (simple or compound). The assertion attached immediately before and immediately after a statement are known respectively as the precondition and postcondition of that statement.

The proof of partial correctness consists of a formal demonstration that the semantics of each statement in the program, whether simple or compound, are consistent with its precondition and postcondition. This demonstration can begin at the level of the simple statements and then proceed through the various levels of compound statement until eventually it is demonstrated that the semantics of the complete program are consistent with its precondition and postcondition, i.e. with the input assertion and the output assertion. The semantics of an individual statement are shown to be consistent with its precondition and postcondition by applying to the precondition and postcondition the appropriate axiom or inference rule for that statement. This yields a theorem, called a verification condition, that must be proved using conventional mathematics in order to demonstrate the required consistency.

[...]

Subjects: Computing.


Reference entries

Users without a subscription are not able to see the full content. Please, subscribe or login to access all content.