A discipline for loop construction

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 inducive stepwise refinement. This discipline for loop construction leads naturally to a scheme for classifying loop mechanisms. It also leads to a proposal for a weak 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 funOamental transformation rules.