The proof rule for definite iteration

Definite iteration means doing something to each member of a composite, or each thing in a sequence of things. In Icon, this is typically an "every" construct.

For example, suppose that you have a list L and you want to run the Munge() procedure on every element of L. Here is how the procedure might look:

    #   [ munge every element of L ]
    def mungeList ( L ):
        for x in L:
            # [ munge x ]
            munge(x)

Here's the proof rule for definite iteration. The overall intended function looks like this:

    [ f(S) ]
    for x in S:
        p(x)

There are two parts to the proof:

1. If S is empty, does doing nothing do f(S)?
2. If S is nonempty, then call the first element first(S), and call the remaining elements rest(S): does doing p(first(S)), followed by doing f(rest(S)), do f(S)?

Last updated: 2002/09/28 01:25:55
URL: http://www.nmt.edu/~shipman/soft/clean/proofdef.html