The Semiautomatic Generation of Inductive Assertions for Proving Program Correctness.

摘要

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.