Contact Us

The History of Artificial Intelligence

Inference rules for program annotation.

purl.stanford.edu/hs853nx1376
Title:
Inference rules for program annotation.
Author:
Dershowitz, Nachum and Manna, Zohar
Author (no Collectors):
Dershowitz, Nachum and Manna, Zohar
Description:
Methods are presented whereby an Algol-like program, given together with its specifications, can be documented automatically. The program is incrementally annotated with invariant relationships that hold between program variables at intermediate points in the program and explain the acutal workings of the program regardless of whether the program is correct. Thus this documentation can be used for proving the correctness of the program or may serve as an aid in the debugging of an incorrect program. The annotation techniques are formulated as Hoare-llike inference rules which derive invariants from the assignment statements, from the control structure of the program, or, heuristically, from suggested invariants. The application of these rules is demonstrated by two examples which have run on an experimental implementation.
Topic:
Computer science
Subject:
Stanford University. Computer Science Department
Language:
English
Physical Description:
1 text file
Publication Info:
cau and Stanford (Calif.)
Date:
October 01, 1977
Place created:
Stanford (Calif.)
Imprint:
Stanford (Calif.), October 1, 1977
Genre:
technical reports
Identifier:
CS-TR-1977-631
Repository:
Stanford University. Libraries. Department of Special Collections and University Archives
Collection:
Stanford University, Department of Computer Science, Technical Reports and Stanford Artificial Intelligence Laboratory records, 1963-2009
Manuscript number:
3840/2