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

The proof rule for alternation

For a construct of the form ``if C then A else B'' uses this proof rule:

Does doing A if C is true, or doing B if C is false, do the overall I/F?

Here's an example:

    # [ if x has a square root ->
    #	  return that square root
    #   else ->
    #	  raise ValueError ]
    procedure sqrt ( x )
      if  x < 0:
        raise ValueError, "Can't take the square root of %g" % x
        return x**0.5

Next: The proof rules for the while loop
See also: Proof rules for Cleanroom control structures
Previous: The proof rule for sequences
Site map
John W. Shipman,
Last updated: 2002/09/28 01:20:13