Accession Number:
ADA007563
Title:
Automatic Program Verification III: A Methodology for Verifying Programs
Descriptive Note:
Technical rept.
Corporate Author:
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Personal Author(s):
Report Date:
1974-12-01
Pagination or Media Count:
47.0
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 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.
Descriptors:
Subject Categories:
- Computer Programming and Software