# Proof of algorithm correctness

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?

• Think about how you add numbers in positional notation. In their case, in binary. At each step $d$ is the position that is being added. Well, $2$ raised to that position. The $x$ is the tail of the result of the sum of $y+z$. The part that has already been added. This is the remainder of $y+z$ modulo $d$.
– plop
Feb 11, 2021 at 13:57
• The $y_j,z_j$ are the quotients of $y$ and $z$ after division by $d$. These are the parts of $y$ and $z$ that hasn't been added yet. The $c$ is the carry over.
– plop
Feb 11, 2021 at 14:03
• Note that when $d$ becomes sufficiently large, then $y=z=c=0$ and the invariant equation becomes $0\cdot d+x=y+z$. So, $x=y+z$.
– plop
Feb 11, 2021 at 14:04

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.

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$$