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

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE