The Semiautomatic Generation of Inductive Assertions for Proving Program Correctness.
Final rept. 1 Jul 77-30 Jun 78,
SRI INTERNATIONAL MENLO PARK CA COMPUTER SCIENCE LAB
Pagination or Media Count:
This final report describes progress over the period 1 July 1977 through 30 June 1978 on a five-year project aimed at the problem of synthesizing so-called inductive assertions to support the Floyd-Hoare method for proving correctness of computer programs. In the fifth year of our research, reported here, we concentrated on using the Boyer-Moore system to prove several quite different kinds of programs. The first set of programs verified here form a system of LISP functions implementing a verification condition generator VCG for a simple block-structured language. The specifications for this VCG are given as standard Hoare axioms and rules. The second set of programs are algorithms for achieving synchronization among several clocks. This application arose in connection with the design of an operating system for a fault-tolerant avionics computer SIFT with hardware and software redundancy features.
- Computer Programming and Software