Question 1-6

Say you are to prove the following using our axiomatic scheme. 

{ n = 2k AND k >= 0 }     -- The caret `^' represents exponentiation
i := 0;
j := n;
while j > 1 loop
    j := j / 2;
    i := i + 1;
end loop;
{ n = 2i }
What is the loop invariant that will allow you to write the proof? Do not write the proof, just the invariant. Partial credit will be given for partially correct invariants.

Solution

n = j 2i AND j >= 1

Back to Review for Quiz 1