Report Number: CS-TR-74-474
Institution: Stanford University, Department of Computer Science
Title: Automatic program verification III: a methodology for
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
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.