Accession Number:

AD0767331

Title:

Automatic Program Verification 1: A Logical Basis and Its Implementation

Descriptive Note:

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Report Date:

1973-05-01

Pagination or Media Count:

58.0

Abstract:

Defining the semantics of programming languages by axioms and rules of inference yields a deduction system within which proofs may be given that programs satisfy specifications. The deduction system herein is shown to be consistent and also deductive complete with respect to Hoares system. A subgoaler for the deductive system is described whose input is a significant subset of Pascal Programs plus inductive assertions. The output is a set of verification conditions or lemmas to be proved. Several non-trivial arithmetic and sorting programs have been shown to satisfy specifications by using an interactive theorem prover to automatically generate proofs of the verification conditions. Additional components for a more powerful verification system are under construction.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE