Automatic Program Verification III: A Methodology for Verifying Programs
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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 1 interactive application of a verification condition generator, an algebraic simplifier and a theorem-prover 2 techniques for describing data structures, type constraints, and properties of programs and subprograms i.e. lower level procedures 3 the use of abstract data types in structuring programs and proofs.
- Computer Programming and Software