Computer Science 15-112, Fall 2011
Class Notes:  Correctness

  1. Required Reading
  2. Buggy Example
  3. Preconditions
  4. Postconditions
  5. Invariants
  6. Test Functions
  7. Fixed Example
  8. Contracts
    1. With explicit functions
    2. With @contract
    3. Other contract implementations in Python
  1. Required Reading
    1. "Design by Contract" on Wikipedia
    2. 15-122 Lecture Notes on Contracts (a bit more rigorous than how we'll handle things in 15-112)
       
  2. Buggy Example
    def sqrt(x):
    # buggy function that uses bisection (binary search) to
    # find the square root of x
    epsilon = 0.00000001
    hi = x/2
    lo = 0
    while (hi - lo > epsilon):
        guess = (hi + lo)/2
        guessSquared = guess^2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
    return (hi + lo)/2

# problem....
print sqrt("two")  # fails, but opaquely

# solution...
  3. Preconditions
    def isReal(x):
    # From Python 2.6 onwards, can just do: isinstance(x, numbers.Real)
    # But we'll make this compatible with Python 2.5 (which runs on linux.andrew)
    return (isinstance(x, float) or isinstance(x, int) or isinstance(x, long))

def sqrt(x):
    # buggy function that uses bisection (binary search) to
    # find the square root of x
    assert (isReal(x) and (x >= 0))  # preconditions
    epsilon = 0.00000001
    hi = x/2
    lo = 0
    while (hi - lo > epsilon):
        guess = (hi + lo)/2
        guessSquared = guess^2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
    return (hi + lo)/2

print sqrt("two")  # still fails, but with a clear violation of a precondition

# another problem....
print sqrt(2) # prints 0

# part of the solution....
  4. Postconditions
    def isReal(x):
    # From Python 2.6 onwards, can just do: isinstance(x, numbers.Real)
    # But we'll make this compatible with Python 2.5 (which runs on linux.andrew)
    return (isinstance(x, float) or isinstance(x, int) or isinstance(x, long))

def almostEqual(d1, d2):
    epsilon = 0.000001  # use larger epsilon here...
    return abs(d1 - d2) < epsilon

def sqrt(x):
    # buggy function that uses bisection (binary search) to
    # find the square root of x
    assert (isReal(x) and (x >= 0))  # preconditions
    epsilon = 0.00000001
    hi = x/2
    lo = 0
    while (hi - lo > epsilon):
        guess = (hi + lo)/2
        guessSquared = guess^2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
    result = (hi + lo)/2
    assert (isReal(result) and almostEqual(result**2, x))  # postconditions
    return result

print sqrt(2) # still fails, but not quietly (now clearly violates a postcondition)
  5. Invariants
     
    1. Initial Code
      def isReal(x):
    # From Python 2.6 onwards, can just do: isinstance(x, numbers.Real)
    # But we'll make this compatible with Python 2.5 (which runs on linux.andrew)
    return (isinstance(x, float) or isinstance(x, int) or isinstance(x, long))

def almostEqual(d1, d2):
    epsilon = 0.000001
    return abs(d1 - d2) < epsilon

def sqrt(x):
    # buggy function that uses bisection (binary search) to
    # find the square root of x
    assert (isReal(x) and (x >= 0))  # preconditions
    epsilon = 0.00000001
    hi = x/2
    lo = 0
    while (hi - lo > epsilon):
        guess = (hi + lo)/2
        guessSquared = guess**2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
    result = (hi + lo)/2
    assert (isReal(result) and almostEqual(result**2, x))  # postconditions
    return result

print "Looks like it works..."
print "    sqrt(4.5) =", sqrt(4.5)

print "But it doesn't..."
print "    sqrt(4) =", sqrt(4)
    2. First (Unsuccessful) Try
      def isReal(x):
    # From Python 2.6 onwards, can just do: isinstance(x, numbers.Real)
    # But we'll make this compatible with Python 2.5 (which runs on linux.andrew)
    return (isinstance(x, float) or isinstance(x, int) or isinstance(x, long))

def almostEqual(d1, d2):
    epsilon = 0.000001
    return abs(d1 - d2) < epsilon

def sqrt(x):
    # buggy function that uses bisection (binary search) to
    # find the square root of x
    assert (isReal(x) and (x >= 0))  # preconditions
    epsilon = 0.00000001
    hi = x/2
    lo = 0
    while (hi - lo > epsilon):
        assert (lo < hi)             # invariant
        guess = (hi + lo)/2
        guessSquared = guess**2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
    result = (hi + lo)/2
    assert (isReal(result) and almostEqual(result**2, x))  # postconditions
    return result

print "Looks like it works..."
print "    sqrt(4.5) =", sqrt(4.5)

print "But it STILL doesn't..."
print "    sqrt(4) =", sqrt(4)
    3. Second (Successful) Try
      def isReal(x):
    # From Python 2.6 onwards, can just do: isinstance(x, numbers.Real)
    # But we'll make this compatible with Python 2.5 (which runs on linux.andrew)
    return (isinstance(x, float) or isinstance(x, int) or isinstance(x, long))

def almostEqual(d1, d2):
    epsilon = 0.000001
    return abs(d1 - d2) < epsilon

def sqrt(x):
    # buggy function that uses bisection (binary search) to
    # find the square root of x
    assert (isReal(x) and (x >= 0))  # preconditions
    epsilon = 0.00000001
    hi = x/2
    lo = 0
    while (hi - lo > epsilon):
        assert (lo < hi)             # invariant
        oldDelta = hi - lo
        guess = (hi + lo)/2
        guessSquared = guess**2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
        newDelta = hi - lo
        assert (newDelta < oldDelta) # invariant
    result = (hi + lo)/2
    assert (isReal(result) and almostEqual(result**2, x))  # postconditions
    return result

print "Looks like it works..."
print "    sqrt(4.5) =", sqrt(4.5)

print "Still fails, but not quietly now (cleary violates an invariant)"
print "    sqrt(4) =", sqrt(4)
  6. Test Functions
    def isReal(x):
    # From Python 2.6 onwards, can just do: isinstance(x, numbers.Real)
    # But we'll make this compatible with Python 2.5 (which runs on linux.andrew)
    return (isinstance(x, float) or isinstance(x, int) or isinstance(x, long))

def almostEqual(d1, d2):
    epsilon = 0.000001
    return abs(d1 - d2) < epsilon

def sqrt(x):
    # buggy function that uses bisection (binary search) to
    # find the square root of x
    assert (isReal(x) and (x >= 0))  # preconditions
    epsilon = 0.00000001
    hi = x/2.0
    lo = 0.0
    while (hi - lo > epsilon):
        assert (lo < hi)             # invariant
        oldDelta = hi - lo
        guess = (hi + lo)/2
        guessSquared = guess**2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
        newDelta = hi - lo
        assert (newDelta < oldDelta) # invariant
    result = (hi + lo)/2
    assert (isReal(result) and almostEqual(result**2, x))  # postconditions
    return result

def testSqrt():
    print "Testing sqrt()...",
    assert(almostEqual(sqrt(0), 0))
    assert(almostEqual(sqrt(123.45**2), 123.45))
    assert(sqrt(4) == 2.0) # say we require sqrts of perfect squares to have no fractional value
    assert(almostEqual(sqrt(2)*sqrt(2), 2))
    print "Passed!"

testSqrt()
  7. Fixed Example
    def isReal(x):
    # From Python 2.6 onwards, can just do: isinstance(x, numbers.Real)
    # But we'll make this compatible with Python 2.5 (which runs on linux.andrew)
    return (isinstance(x, float) or isinstance(x, int) or isinstance(x, long))

def almostEqual(d1, d2):
    epsilon = 0.000001
    return abs(d1 - d2) < epsilon

def sqrt(x):
    # uses bisection (binary search) to find the square root of x
    assert (isReal(x) and (x >= 0))  # preconditions
    epsilon = 0.00000001
    hi = x
    lo = 0.0
    while (hi - lo > epsilon):
        assert (lo < hi)             # invariant
        oldDelta = hi - lo
        guess = (hi + lo)/2
        guessSquared = guess**2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
        newDelta = hi - lo
        assert (newDelta < oldDelta) # invariant
    result = round((hi + lo)/2, 7)
    assert (isReal(result) and almostEqual(result**2, x))  # postconditions
    return result

def testSqrt():
    print "Testing sqrt()...",
    assert(almostEqual(sqrt(0), 0))
    assert(almostEqual(sqrt(123.45**2), 123.45))
    assert(sqrt(4) == 2.0) # say we require sqrts of perfect squares to have no fractional value
    assert(almostEqual(sqrt(2)*sqrt(2), 2))
    print "Passed!"

testSqrt()
  8. Contracts
    1. With explicit functions
      1. Without f_base
        def sqrt_requires(x):
    assert (isReal(x) and (x >= 0))  # preconditions

def sqrt_ensures(result, x):
    assert (isReal(result) and almostEqual(result**2, x))  # postconditions

def sqrt(x):
    # uses bisection (binary search) to find the square root of x
    sqrt_requires(x)
    epsilon = 0.00000001
    hi = x/2.0
    lo = 0.0
    while (hi - lo > epsilon):
        assert (lo < hi)             # invariant
        oldDelta = hi - lo
        guess = (hi + lo)/2
        guessSquared = guess**2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
        newDelta = hi - lo
        assert (newDelta < oldDelta) # invariant
    result = round((hi + lo)/2, 7)
    sqrt_ensures(result, x)
    return result
      2. With f_base
        def sqrt_requires(x):
    assert (isReal(x) and (x >= 0))  # preconditions

def sqrt_ensures(result, x):
    assert (isReal(result) and almostEqual(result**2, x))  # postconditions

def sqrt_base(x):
    # uses bisection (binary search) to find the square root of x
    epsilon = 0.00000001
    hi = x/2.0
    lo = 0.0
    while (hi - lo > epsilon):
        assert (lo < hi)             # invariant
        oldDelta = hi - lo
        guess = (hi + lo)/2
        guessSquared = guess**2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
        newDelta = hi - lo
        assert (newDelta < oldDelta) # invariant
    return round((hi + lo)/2, 7)

def sqrt(x):
    sqrt_requires(x)
    result = sqrt_base(x)
    sqrt_ensures(result, x)
    return result
    2. With @contract
      ############################
# "gray code" for @contract
# include this, but do not worry about how it works!
############################
import functools
def contract(f):
    def callIfExists(fn, suffix, *args, **kwargs):
        fnName = fn.__name__ + suffix
        if (fnName in globals()): return globals()[fnName](*args, **kwargs)
    @functools.wraps(f)
    def wrapper(*args, **kwargs):
        if (__debug__):
            reqResult = callIfExists(f, "_requires", *args, **kwargs)
        result = f(*args, **kwargs) 
        if (__debug__):
            if (reqResult == None):
                callIfExists(f, "_ensures", result, *args, **kwargs)
            else:
                callIfExists(f, "_ensures", reqResult, result, *args, **kwargs)
        return result
    return wrapper
############################

def sqrt_requires(x):
    assert (isReal(x) and (x >= 0))  # preconditions

def sqrt_ensures(result, x):
    assert (isReal(result) and almostEqual(result**2, x))  # postconditions

@contract
def sqrt(x):
    # uses bisection (binary search) to find the square root of x
    epsilon = 0.00000001
    hi = float(x) if (x > 1) else 1.0 # because sqrt(x)>=x for x in [0,1]
    lo = 0.0
    while (hi - lo > epsilon):
        assert (lo < hi)             # invariant
        oldDelta = hi - lo
        guess = (hi + lo)/2
        guessSquared = guess**2
        if (guessSquared > x):
            # guess is too high...
            hi = guess
        elif (guessSquared < x):
            # guess is too low...
            lo = guess
        else:
            # we got it exactly!
            break
        newDelta = hi - lo
        assert (newDelta < oldDelta) # invariant
    return round((hi + lo)/2, 7)
    3. Other contract implementations in Python

carpe diem   -   carpe diem   -   carpe diem   -   carpe diem   -   carpe diem   -   carpe diem   -   carpe diem   -   carpe diem   -   carpe diem