A Discipline for Loop Construction.
Abstract
A discipline for loop construction is presented which is based on the concept of a well-formed postcondition. A well-formed postcondition is seen to have an implicit logical structure which is made explicit by appropriate variable binding. This variable binding identifies the loop invariant and a determinate. Loops are then constructed by first identifying the weakest iterative mechanism capable of establishing the postcondition. Subsequent development proceeds by way of inductive stepwise refinement. This discipline for loop construction leads naturally to a scheme for classifying loop mechanisms. It also leads to a proposal for a week loop grammar (not in principle unlike Chomsky's phrase structure grammar) which helps to make explicit semantically important components of a loop structure. The grammar is enhanced by a set of fundamental transformation rules. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 30, 1983
- Accession Number
- ADA165893
Entities
People
- R. G. Dromey
Organizations
- University of Wollongong