Issue No. 03 - May (1977 vol. 3)
B. Wegbreit , Xerox Palo Alto Research Center
Most current approaches to mechanical program verification transform a program and its specifications into first-order formulas and try to prove these formulas valid. Since the first-order predicate calculus is not decidable, such approaches are inherently limited. This paper proposes an alternative approach to program verification: correctness proofs are constructively established by proof justifications written in an algorithmic notation. These proof justifications are written as part of the program, along with the executable code and correctness specifications. A notation is presented in which code, specifications, and justifications are interwoven. For example, if a program contains a specification 3x P(x), the program also contains a justification that exhibits the particulat value of x that makes P true. Analogously, justifications may be used to state how universally quantified formulas are to be instantiated when they are used as hypotheses. Programs so justifiled may be verified by proving quantifier-free formulas. Additional classes of justifications serve related ends. Formally, justifications reduce correctness to a decidable theory. Informally, justifications establish the connection between the executable code and correctness specifications, documenting the reasoning on which the correctness is based.
Constructive program verification, first-order logic, instantiations, program verification, programming language design, programming languages, programming methodology, proof justifications, proving programs correct.
B. Wegbreit, "Constructive Methods in Program Verification," in IEEE Transactions on Software Engineering, vol. 3, no. , pp. 193-209, 1977.