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