Report Number: CS-TR-74-474
Institution: Stanford University, Department of Computer Science
Title: Automatic program verification III: a methodology for verifying programs.
Author: von Henke, Friedrich W.
Author: Luckham, David C.
Date: December 1974
Abstract: The paper investigates methods for applying an on-line interactive verification system designed to prove properties of PASCAL programs. The methodology is intended to provide techniques for developing a debugged and verified version starting from a program, that (a) is possibly unfinished in some respects, (b) may not satisfy the given specifications, e.g., may contain bugs, (c) may have incomplete documentation, (d) may be written in non-standard ways, e.g., may depend on user-defined data structures. The methodology involves (i) interactive application of a verification condition generator, an algebraic simplifier and a theorem-prover; (ii) techniques for describlng data structures, type constraints, and properties of programs and subprograms (i.e. lower level procedures); (iii) the use of (abstract) data types in structuring programs and proofs. Within each unit (i.e. segment of a problem), the interactive use is aimed at reduclng verification conditions to manageable proportions so that the non-trivial factors may be analysed. Analysis of verification conditions attempts to localize errors in the program logic, to extend assertions inside the program, to spotlight additional assumptions on program subfunctions (beyond those already specified by the programmer), and to generate appropriate lemmas that allow a verification to be completed. Methods for structuring correctness proofs are discussed that are similar to those of "structured programming". A detailed case study of a pattern matching algorithm illustrating the various aspects of the methodology (including the role played by the user) is given.