Accession Number:

ADA061919

Title:

The Semiautomatic Generation of Inductive Assertions for Proving Program Correctness.

Descriptive Note:

Final rept. 1 Jul 77-30 Jun 78,

Corporate Author:

SRI INTERNATIONAL MENLO PARK CA COMPUTER SCIENCE LAB

Personal Author(s):

• Elspas,Bernard
• Shostak,Robert E.

Report Date:

1978-08-01

Pagination or Media Count:

116.0

Abstract:

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.

Descriptors:

• *COMPUTER PROGRAMMING
• *COMPUTER PROGRAM VERIFICATION
• ALGORITHMS
• AVIONICS
• PROGRAMMING LANGUAGES
• FINITE DIFFERENCE THEORY
• RECURSIVE FUNCTIONS
• SYNCHRONISM
• REDUNDANCY
• FAULT TOLERANT COMPUTING

Subject Categories:

• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE