Exercises for Chapter 3

As in all the other posted examples and exercises, I have used blank spaces only to indent the code lines. Please be careful not to mix tabs and blanks in your indentations.

1. Prove correct this recursively defined function:

# Q1:  double returns an int that is twice as large as its int argument, n"""
def double(n) :
    """{ pre  n >= 0
         post ans == 2 * n
         return ans
    }"""
    if n == 0 :
        ans = 0
    else :
        subans = double(n - 1)
        ans = subans + 2
    return ans

2. Insert the missing invariant and do the correctness proof for this loop program.

# Q2.py
n = readInt()
assert n >= 0
x = 0
y = 0

while x != n :
    """{ invariant   ? ? ? ?
         modifies  y, x  }"""
    y = y + n
    x = x + 1

# PROVE HERE THAT: y == n * n
print y

Note: the checker program sometimes has trouble proving assertions with polynomials (multiplications like a * b), since this exceeds the checker's automated expertise in linear algebra. If algebra fails to prove an equality, try subst instead.

3. Supply the missing assignment command and use the stated invariant to prove that the program is correct:

# Q3.py
m = readInt()
n = readInt()
ans = m
b = n

while  b != 0 :
    """{ invariant  ans == (m - n) + b
         modifies  a, b  }"""
    ans = ? ? ?    # insert an assignment here
    b = b - 1

# WHAT KNOWLEDGE ABOUT  ans'S  VALUE DO WE HAVE HERE?
# (HINT: the invariant holds and the test has gone False)
# PROVE A GOAL OF THE FORM,   ans == ???

4. Global invariants and loop invariants usually state the key rules of a game. Here is a "Price is Right" game, where a sequence of players make increasing bids on a "Showcase prize". The player who wins is the one with the highest bid that does not exceed the value of the Showcase. Prove that the loop maintains its invariant and that the global invariant is maintained by playround.

### "Price is Right" game:
target = readInt("Drew Carey types in the secret price of today's Showcase")
assert target > 0

### variables used by the game:
bestguess = 0     # the bid that is closest so far (without going over)

"""{ globalinv  bestguess <= target and target > 0 }"""   # this is the key rule of the game!

prize = 0         # a bonus cash prize that goes to the winner

def playround(next) :
    """plays the next round of the game with the  next  bid"""
    """{ pre next >= bestguess 
         post cash <= bestguess
         return cash
    }"""
    global bestguess
    if next <= target :
        bestguess = next 
        cash = 0
    else :
        cash = bestguess


###  the game is played here:

print "Let's ask our contestants to place their bids!"
while  nextguess < target :
    """{ invariant  prize <= target    # a secondary rule for this version of the game
         modifies   nextguess, prize, bestguess }"""
    nextguess = readInt("The next player's guess at the Showcase Price:")
    assert nextguess > bestguess     # the next player must "raise the bid" !
    prize = playround(nextguess)

# LOOP ENDS; GAME IS OVER
print "The winner gets the showcase and this much cash:",  prize 

5. (Please read; there's nothing to submit!) One of the first loop algorithms ever invented was Euclid's greatest-common-divisor algorithm. Euclid discovered an invariant property of divisors that he converted into the first known loop invariant. Please read the explanation at http://www.cs.uofs.edu/~mccloske/courses/cmps134/euclidalg.html.