program correctness proof
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.
"program correctness proof." A Dictionary of Computing. . Encyclopedia.com. (February 20, 2019). https://www.encyclopedia.com/computing/dictionaries-thesauruses-pictures-and-press-releases/program-correctness-proof
"program correctness proof." A Dictionary of Computing. . Retrieved February 20, 2019 from Encyclopedia.com: https://www.encyclopedia.com/computing/dictionaries-thesauruses-pictures-and-press-releases/program-correctness-proof
Encyclopedia.com gives you the ability to cite reference entries and articles according to common styles from the Modern Language Association (MLA), The Chicago Manual of Style, and the American Psychological Association (APA).
Within the “Cite this article” tool, pick a style to see how all available information looks when formatted according to that style. Then, copy and paste the text into your bibliography or works cited list.
Because each style has its own formatting nuances that evolve over time and not all information is available for every reference entry or article, Encyclopedia.com cannot guarantee each citation it generates. Therefore, it’s best to use Encyclopedia.com citations as a starting point before checking the style against your school or publication’s requirements and the most-recent information available at these sites:
Modern Language Association
The Chicago Manual of Style
American Psychological Association
- Most online reference entries and articles do not have page numbers. Therefore, that information is unavailable for most Encyclopedia.com content. However, the date of retrieval is often important. Refer to each style’s convention regarding the best way to format page numbers and retrieval dates.
- In addition to the MLA, Chicago, and APA styles, your school, university, publication, or institution may have its own requirements for citations. Therefore, be sure to refer to those guidelines when editing your bibliography or works cited list.