In order to prove an algorithm correctness a loop invariant should include:
- Initialization:It is true prior to the first iteration of the
- Maintenance: If it is true before an iteration of the loop, it
remains true before the next iteration.
- 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$