Use the loop invariant theorem to prove the conrrectness of the loop with respect to the pre- and post-conditions.

Pre-condition: a = A and A is a positive integer.

while (a > 0)

1. a := a - 2

end while

Post-condition: a = 0 if A is even and a = -1 if A is odd.

Loop invariant: I(n) is "Both a and A are even integers or both are odd integers and a ? -1."