Generalizing Specifications for Uniformly Implemented Loops.
Abstract
The problem of generalizing functional specifications for WHILE loops is considered. This problem occurs frequently when trying to verify that an initialized loop satisfies some functional specification, i.e., produces outputs which are some function of the program inputs. The notion of a valid generalization of a loop specification is defined. A particularly simple valid generalization, a base generalization, is discussed. A property of many commonly occurring WHILE loops, that of being uniformly implemented, is defined. A technique is presented which exploits this property in order to systemically achieve a valid generalization of the loop specification. Two classes of uniformly implemented loops which are particularly susceptible to this form of analysis are defined and discussed. The use of the proposed technique is illustrated with a number of applications. Finally, an implication of the concept of uniform loop implementation for the validation of the obtained generalization is explained. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1981
- Accession Number
- ADA108585
Entities
People
- Douglas D. Dunlop
- Victor Basili
Organizations
- University of Maryland