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
else:
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,
`john@nmt.edu`
##### Last updated: 2002/09/28 01:20:13

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