Accession Number:

ADA050806

Title:

Inference Rules for Program Annotation.

Descriptive Note:

Technical rept.,

Corporate Author:

STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1977-10-01

Pagination or Media Count:

53.0

Abstract:

Methods are presented whereby an ALGOL-like program, given together with its specifications, may be documented automatically. This documentation expresses invariant relationships that hold between program variables at intermediate points in the program, and explains the actual 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-like 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 our implemented system. Author

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE