The Semiautomatic Generation of Inductive Assertions for Proving Program Correctness.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1978
Accession Number
ADA061919

Entities

People

  • Bernard Elspas
  • Robert E. Shostak

Organizations

  • SRI International

Tags

Communities of Interest

  • Advanced Electronics
  • C4I

DTIC Thesaurus Topics

  • Air Force
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Concrete
  • Formal Languages
  • Information Science
  • Inventions
  • Language
  • Mathematics
  • Notation
  • Operating Systems
  • Programming Languages
  • Recursive Functions
  • Standards
  • System Software

Fields of Study

  • Computer science
  • Engineering

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Mathematical Modeling and Probability Theory.
  • Software Engineering.