A DISCIPLINE FOR LOOP CONSTRUCTION

Australia. 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 identify-ing the weakest iterative mechanism capable of establishing the postcondition. Subsequent development proceeds by way of inOuct,ve 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