prove the following loop

Question

If the predicate a+b = even is true, the prove the following loop is true
while (a >= 0 and a <= 100) {
a = a + 3;
b = b -1;
}

Answer 1

If a + b is even, then either both a and b are even or both are odd.

 

a could be written 2n or 2n+1, 2n-1 (even or odd, odd)

b could be written 2k or 2k+1, 2k-1 (even or odd, odd)

 

Substitute the even/odd representations in for a and b:

 

Even case:

a = 2n+3 = 2n+2+1 = 2(n+1) +1 which is odd

b = 2k-1 which is odd

 

Odd case:

a = (2n+1)+3 = 2n+4 = 2(n+2) which is even

b = (2k+1)-1 = 2k which is even

 

As the loop continues to add 3 to a each iteration it will eventually reach >=100 and run its course.

 

If a starts as any negative integer, it will not run.

 

I hope this helps.