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:

- If
`S` is empty, does doing nothing do `f(S)`?
- 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`
##### Last updated: 2002/09/28 01:25:55

URL: http://www.nmt.edu/~shipman/soft/clean/proofdef.html