1
$\begingroup$

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.

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

1 Answer 1

0
$\begingroup$

A very simple loop invariant: w = z *2^k, and q and r are the correct result for division by w instead of division by z. k=0 proves the theorem.

$\endgroup$

Your Answer

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

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