CIS501 Exercise Friday Feb. 14
State, as best you can, the invariant that makes the loop run properly and leads to the goal.
####### This program computes remainder (modulo), a % b
# Read a and b :
a = (int)(raw_input("a:"))
b = (int)(raw_input("b:"))
assert a >=0 and b > 0 # no negatives, ok
rem = a # will become the remainder, a % b
count = 0 # counts how often the loop repeats
while rem >= b :
"""{ invariant a == (b * count) + rem }"""
print "count=", count, " a=", a, " b=", b, " rem=", rem
rem = rem - b
count = count + 1
# the goal is that rem == a % b
"""MORE PRECISELY: 0 <= rem < b , and
there exists int c >= 0, the quotient,
such that a - (c * b) == rem
PERHAPS YOU THINK OF REMAINDER LIKE THIS: rem == a - (trunc(a/b) * b) """
print "DONE: count=", count, " a=", a, " b=", b, " rem=", rem
raw_input()
"""Notice that var count ISN'T needed to compute the remainder. It is a
ghost/auxiliary variable that I included to make it easy to state the invariant.
Such ghost variables are required in practice and make it impossible for an
automated tool to discover invariants."""