Automatic Program Verification 1: A Logical Basis and Its Implementation
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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.
- Computer Programming and Software