program correctness proof

program correctness proof 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.

Note particularly that the overall proof of correctness is achieved not by consideration of execution histories, but rather by treating the program as a static mathematical object to which certain axioms and inference rules apply.

The central problem with such a proof is the devising of the intermediate assertions. This requires a full appreciation of the design of the program and of the semantics of the programming language. Often the key lies in finding appropriate intermediate assertions to attach inside the various loops in the program, i.e. loop invariants. Devising intermediate assertions for some arbitrary program is often extremely difficult and a constructive approach, in which program and proof are developed together, is definitely preferable.

In order to present a proof of termination it is necessary to demonstrate first that the program does not suffer from abortive termination and second that the program does not endlessly repeat some loop. A demonstration of the former may become very complex, e.g. it may be necessary to demonstrate that arithmetic overflow will not occur. A demonstration that the program will eventually exit from some loop can be based on a well-ordered set. For example, suppose that for some loop an expression E can be found such that the loop can be shown to terminate immediately if the value of E is negative. Further suppose that the value of E can be shown to decrease on each iteration around the loop. It then follows that the loop must terminate.

Proofs of correctness do not offer a complete solution to the problems of software reliability in practical systems. The sheer size and complexity of proofs presents many difficulties that are only partly alleviated by mechanical verifier systems. Issues such as the limitations of computer arithmetic, indeterminacy, and parallelism all present additional problems. It may be very difficult to develop a specification against which to verify a program, and impossible to demonstrate that this specification is itself “correct” in that it properly reflects the intentions of the developers (and even more difficult to prove that it satisfies the needs of the intended users).

Work on proofs of correctness has made a major contribution to software engineering in that many advances in the understanding of programming languages, principles, and methods have their origins in this work. In addition the scope for practical applications of program proofs is growing and the formal approach to program correctness is of increasing significance.