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?

  • 1
    $\begingroup$ 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$. $\endgroup$
    – plop
    Commented Feb 11, 2021 at 13:57
  • $\begingroup$ 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. $\endgroup$
    – plop
    Commented Feb 11, 2021 at 14:03
  • $\begingroup$ 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$. $\endgroup$
    – plop
    Commented Feb 11, 2021 at 14:04

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.