Next / Previous / Contents / Shipman's homepage

6.2. The alternation rule

This rule is for subdividing some prime A into an if construct with this general form:

# [ A ]
if B:
    # [ C ]
    ...
else:
    # [ D ]
    ...

The proof rule is:

Doing the intended function C when B is true, or doing the intended function D when B is false, must have the same net affect as doing the intended function for A.

Here's a brief example.

def sqrt(x):
    '''Return the square root of x.

      [ x is a number ->
          if x is nonnegative ->
            return the square root of x
          else -> raise ValueError ]
    '''
    #-- 1
    if x >= 0:
        #-- 1.1
        # [ return x to the one-half power ]
        return x**0.5
    else:
        #-- 1.2
        # [ raise ValueError ]
        raise ValueError("You can't take the square root of a "
            "negative number like {0:g}.".format(x))