Suppose we have the following program that computes the quotient and remainder when dividing a by b: r = a q 0 while r >= b: r = r b q += 1 and precondition: (a > 0) ^ (6 > 0) postcondition: (a = bq+r) 1 (0