Consider the program segment S.

initial assertion p: m Z + {0}, x R

i := 0

exp := 1

while i =/(does not equal) m

exp := exp x

i := i + 1

(a) What is the final assertion q for this program segment?

(b) Let r be the assertion: exp = x n and i = n. Prove that r is a loop invariant for this loop.

(c) Prove that if the loop terminates, is satisfies your final assertion.

(d) Prove that the loop terminates.