"""
Precondition, postcondition, invariant
A while-loop can be derived by filling in this template
with blocks S and T and condition P
that establish invariant I and postcondition I and not P
S
# pre: I
while (P):
# I
T
# post: I and not P
"""
def quotient(n, d):
"""
Divide n by d, integer division by repeated subtraction
n: dividend, d: divisor, q: quotient, r: remainder
The definition of integer division is: n == q*d + r and r < d
"""
assert n >= 0 and d > 0 # function precondition
r = n
q = 0
# assert n == q*d + r # loop precondition
while (r >= d):
# assert n == q*d + r # loop invariant
r = r - d
q = q + 1
# assert n == q*d + r and r < d # postcondition
return q
print '9/3 %s' % quotient(9,3)
print '8/3 %s' % quotient(8,3)
print '3/3 %s' % quotient(3,3)
print '2/3 %s' % quotient(2,3)
# what happens if preconditions are violated?