I am currently brand new to the correctness proof method, and have stumbled upon this algorithm which I find very tricky.
Prove that the following algorithm for division and remainders of natural numbers is correct.
function divide(y,z)
comment Return $q,r \in \mathbb{N}$ such that $y=qz+r$ and $r<z$, where $y,z \in \mathbb{N}$
$r:=y; q:=0; w:=z;$
while $w \leq y$ do $w:=2w$
while $w>z$ do
$q:=2q; w:=\lfloor w/2\rfloor;$
if $w \leq r$ then
$r:=r-w; \space q=q+1;$
return(q,r)
The loop loop which I got for the following algorithm is $q_j w_j + r_j = y_0$ and $r_j < w_j$. And this is what I got so far.
In each iteration we calculate the following variables:
$w_{j+1} = \lfloor w_j / 2 \rfloor$, $q_{j+1}=2q_j$
$r_{j+1}=r_j-w_{j+1}$, $q_{j+1}=q_{j+1}+1=2q_{j}+1$ if $w_{j+1} \leq r_j$
To prove the loop invariant, I used mathematical induction.
Assume that it holds for some $j$, and let's prove that the loop invariant holds for $j+1$. First I tried proving that in $j+1$. iteration the if statement hold ($w_{j+1} \leq r_j$).
$q_{j+1}w_{j+1}+r_{j+1}=y_0$ and $r_{j+1} < w_{j+1}$
$(2q_j+1) \lfloor w_j/2 \rfloor + r_j-\lfloor w_j/2 \rfloor =y_0$ and $r_j-\lfloor w_j/2 \rfloor < \lfloor w_j/2 \rfloor$
$2q_j \lfloor w_j/2 \rfloor + q_j(w_j\space mod\space 2)-q_j(w_j\space mod\space 2)+r_j=y_0$ and $r_j < 2 \lfloor w_j/2 \rfloor$
$q_jw_j-q_j(w_j\space mod\space 2)+r_j=y_0$ and $r_j<w_j-(w_j \space mod \space 2)$
And then I stated that $(w_j\space mod\space 2) = 0$ in order for the inductive hypothesis to hold. And I got:
$q_jw_j+r_j=y_0$ and $r_j<w_j$
This is the first induction which I proved, the second would be if $w_{j+1} > r_j$.
My question is any of this which I wrote correct, or is there another way to prove the loop invariant. Any type of advice is helpful.
