Inference rules for program annotation
Abstract/Contents
- Abstract
- 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.
Description
Type of resource | text |
---|---|
Form | technical reports |
Extent | 1 text file |
Place | Stanford (Calif.) |
Date created | October 1, 1977 |
Language | English |
Digital origin | reformatted digital |
Creators/Contributors
Author | Dershowitz, Nachum | |
---|---|---|
Author | Manna, Zohar |
Subjects
Subject | Stanford University. Computer Science Department |
---|---|
Subject | Computer science |
Genre | Technical reports |
Bibliographic information
Finding Aid | |
---|---|
Technical Report # | CS-TR-1977-631 |
Location | https://purl.stanford.edu/hs853nx1376 |
Location | 3840/2 |
Repository | Stanford University. Libraries. Department of Special Collections and University Archives |
Access conditions
- Use and reproduction
- The materials are open for research use and may be used freely for non-commercial purposes with an attribution. For commercial permission requests, please contact the Stanford University Archives (universityarchives@stanford.edu).
Collection
Stanford University, Department of Computer Science, Technical Reports
View other items in this collection in SearchWorksStanford Artificial Intelligence Laboratory records, 1963-2009
View other items in this collection in SearchWorksAlso listed in
Loading usage metrics...