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

## The proof rule for sequences

For a sequence of two primes *A* and *B*, the proof
rule is:

Does doing A, followed by doing B, do the overall intended function?

Sequences are not limited to two primes. For example, the sequence
A-B-C-D would use the proof rule: ``Does doing A, then B, then C, then
D, do the overall I/F?''

Here's a fairly trivial example:

# [ return i + 2 ]
def addTwo ( i ):
#-- 1 --
# [ j := i + 2 ]
j = i + 2
#-- 2 --
# [ return j ]
return j

It should be clear that doing prime 1 followed by prime 2 does
the overall intended function.

**Next:** The proof rule for alternation

**See also:** Proof rules for Cleanroom control structures

Site map

John W. Shipman,
`john@nmt.edu`
##### Last updated: 2002/09/28 01:18:51

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