Next / Previous / Shipman's Home Sweet Homepage / Site map

## 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)?

Next: Using trace tables for verification
See also: Proof rules for Cleanroom control structures
Previous: The proof rules for the while loop
Site map
John W. Shipman, john@nmt.edu