# Prove that the following algorithm for division and remainders of natural numbers is correct

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

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

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.

• (While additional whitespace isn't trivial in markdown, line breaks are: just append two spaces to line you want a break after.) Aug 25, 2021 at 8:09
• Greybeard, and you’re telling me that now after double spacing text for years… Aug 25, 2021 at 13:21
• This is the standard written calculation procedure, performed in the binary base. Oct 21, 2022 at 17:23