Proofs of Correctness

AbstractA proof of correctness is a mathematical proof that a computer program or a part thereof will, when executed, yield correct results, i.e. results fulfilling specific requirements. Before proving a program correct, the theorem to be proved must, of course, be formulated. The hypothesis of such a correctness theorem is typically a condition that the relevant program variables must satisfy immediatelybeforethe program is executed. This condition is called the precondition. The thesis of the correctness theorem is typically a condition that the relevant program variables must satisfy immediatelyafterexecution of the program. This latter condition is called the postcondition. The thesis of a correctness theorem may be a statement that the final values of the program variables are a particular function of their initial values.By interpreting the termprogram variablesufficiently broadly to include input and output data.The various approaches to proving a program correct can be categorized in different ways. Often a distinction is made between those that (1) view the program as a transformation between preconditions and postconditions and (2) view the program as a function mapping the initial values of the relevant program variables to their final values. Although this distinction is in principle clear, in practical application it often becomes blurred.In practice, it is important to distinguish between two situations: (1) the program in question terminates (i.e., its execution proceeds to the end in finite time) and yields a correct result (i.e., a result fulfilling the postcondition) and (2) the program in question may or may not terminate, but if it does, then the result is correct. A program of the first type above is said to be totally correct; a program of the second type, partially correct. Typically, quite different types of arguments are appropriate for these two proofs.Another approach to proving a program correct is to prove that it is equivalent in some appropriate sense to another program that was assumed, has been defined, or has been proven to be correct. Such an approach can be useful when the program in question is the result of a series of refinement steps.The definition of correctness need not be a single one but may take on the form of a hierarchy of specifications. The safety relevant correctness theorem, being mathematically weaker than the functional correctness theorem, will typically be easier to prove.