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.

Bring your work with you to class on the 10th, so that we can review it on the board.

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. Here is a loop that computes n - m. Supply the missing assignment command and use the stated invariant to prove that the program is correct:

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

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

print "n - m ==", a

4. Loop invariants are strategies for playing and winning multi-round games. Here is a "Price is Right" game, where a player must guess an increasing sequence of positive numbers in some multiple and come as close as possible to a goal number without going over.

Here is an example of how to play the game: Drew Carey tells you that you will play "6s up to 38". That is, you must guess a sequence of positive ints such that the sequence is increasing, and every int you guess is a multiple of 6. You keep guessing ints and come as close as possible to 38 without going over. Here is one play by an OK but not-so-savvy player:

I guess 12.    Drew says, "CORRECT --- your score is +1!"
I guess 24.    Drew says, "CORRECT --- your score is now +2!"
I guess 30.    Drew says, "CORRECT --- your score is now +3!"
I guess 36.    Drew says, "CORRECT --- your score is now +4!"
Uhh,..., I quit.    Drew says. "YOUR FINAL SCORE IS +4!  You win 4*blahblah bucks!"

Here is a computer coding of a strategy for playing the game, where the jumping/multiples number and the goal number are the inputs. Prove that the strategy will always generate a maximal (winning) score.

#Q4.py   Plays a "Price Is Right" game: "jump s  up to  goal":
#  the program guesses some ints, in jumps (multiples),
#  without going over the  goal.   The output,  score,  is the number of jumps  made.
# The program generates the highest possible score, which is formalized by this output
# condition:   (score * jump) + gap == goal  and  (gap >= 0 and  gap < jump)
#                 where   score * jump  is the int value of the final guess
#                 and  gap  is the distance between the final int guess and the goal.
jump = readInt()
goal = readInt()
assert jump > 0
assert goal >= 0

gap = goal   # gap remembers how far away our current guess is from the goal.

# we must never go negative on the gap between the number guessed and the goal:
"""{ 1. gap == goal  premise
     globalinv  gap >= 0       # establishes the global invariant that  gap >= 0
     2. return 1               # remember the initial value of gap for now
}"""

guess = 0   # the number we have guessed so far
score = 0   # how many rounds we have guessed without going over

# How to play one round of the game:
def playRound():  
    #IMPORTANT: the invariant,  gap >= 0,  is implicit in both pre and post
    # that is, it's a premise on function entry and it must be proved on function exit
    """{ pre  gap >= jump
         post  guess_in + gap_in == guess + gap  and  guess == guess_in + jump 
    }""" 
    global guess, gap
    # guess_in = guess (the checker automatically adds this 'ghost assignment')
    # gap_in = gap     (same here)
    guess = guess + jump
    print "My next guess is",  guess, "!"
    gap = gap - jump
    
# to win the game, we repeatedly play rounds without going over:
while gap >= jump :
    """{ invariant  score * jump == guess  and  guess + gap == goal
         modifies  guess, gap, score, void     # see comment below about 'void'
    }"""
    void = playRound()   # the function returns no answer
    score = score + 1
    # REPROVE THE LOOP INVARIANT HERE

# PROVE HERE that the game was won with a maximum score:
"""{ 1. gap >= 0       globalinv      # a globalinv is a fact that is true "everywhere"
     # ... ADD MORE PROOF STEPS HERE AND PROVE ON THE LAST LINE THAT
     #  (score * jump) + gap == goal  and  (gap >= 0 and  gap < jump)
}"""

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/euclid_alg.html.