Proof of algorithm correctness

Question

I am studying about algorithm correctness and have enctountered this problem.

function add(y,z)
comment Return y + z, where y,z are natural numbers
x :=0; c:=0; d:=1;
while(y>0)v(z>0)v(c>0) do
    a := y mod 2;
    b := z mod 2;
    if a XOR b XOR c then x := x+d;
    c:= (a AND b) v (b AND c) v (a AND c);
    d :=2d; y:= floor(y/2);
    z := floor(z/2);

The book that I'm reading says that loop invariant is $(y_j + z_j + c_j)d_j + x_j = y_0 + z_0$ and I honestly can't understand the conclusion. How do you come up with this? Why is this true?

Answer 1

In order to prove an algorithm correctness a loop invariant should include:

1. Initialization:It is true prior to the first iteration of the loop.
2. Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration.
3. Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.

Let's look at your invariant:

Initialization then is before entering the loop, so choose any number for $y$ or $z$ such that $y,z \in N$ (I'll use $n_1$ and $n_2$ respectively) then you will have that your property is satisfied since at this point: $d=1$, $c=0$ and $x=0$. So your invariant will be: $(n_1 + n_2 + 0)*1 + 0 = n_1 + n_2$.

Maintenance: This one you can prove it with induction. Here a complete example with induction. Is slightly more complicated, but you can see in your case that it holds, since at every iteration you "divide" $y$ and $z$ by 2, but $d$ duplicates every time, therefore balancing the division. The $c$ is there in case of odd numbers.

Loop termination: at this point according to the while, nor $y$ nor $z$ nor $c$ can be higher than $0$, but at the same time they are all natural numbers, therefore they are all $0$. Now we have that $x = y+z$ and if you plug it into the invariant you have: $(0 + 0 + 0)*d + x = y_0 +z_0 \Rightarrow y + z = y_0 + z_0$