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
      else:
        return x**0.5

Last updated: 2002/09/28 01:20:13
URL: http://www.nmt.edu/~shipman/soft/clean/proofalt.html