University of Wollongong
Browse

A discipline for loop construction

Download (2.77 MB)
preprint
posted on 2024-11-16, 00:13 authored by R Geoff Dromey
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.

History

Article/chapter number

83-1

Total pages

60

Language

English

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC