Given positive integers a and b, we want to compute some integers s and t such that gcd(a, b) = sa + tb.

Consider the following iterative program LIN_COMB(a, b) which is supposed to accomplish this:

Initialize variables c = a, d = b, s0 = 1, t0 = 0, s1 = 0, t1 = 1

While c 6= d, do the following:

If c < d, then decrement d by c, decrement s1 by s0, decrement t1 by t0

Else if c > d, then decrement c by d, decrement s0 by s1, decrement t0 by t1

Return s0 and t0.

a) Prove that (c = s0a + t0b) ∧ (d = s1a + t1b) is a loop invariant for the while loop in LIN_COMB.

b) Assume, in addition to (a), that gcd(a, b) = gcd(c, d) is a loop invariant for the while loop in LIN_COMB. Prove that LIN_COMB satisfies partial correctness.

c) Prove that (c > 0) ∧ (d > 0) is a loop invariant for the while loop in LIN_COMB.

d) Use the well-ordering principle and (c) to prove that LIN_COMB satisfies termination.