Can someone help me prove the correctness of this algorithm:

   WHILE x≥b DO
   IF x=0 THEN

I had to prove that $x_n + b\cdot y_n = a$ by induction, where $x_n$ and $y_n$ are the values of the variable x and y after the loop has iterated n times.

I have done that, but I am not sure how to prove the correctness of the algorithm.

  • 3
    $\begingroup$ First step: define what correctness means, for this algorithm. $\endgroup$ – D.W. Oct 19 '17 at 5:32
  • 1
    $\begingroup$ Don't use images as main content of your post. This makes your question impossible to search and inaccessible to the visually impaired; we don't like that. Please transcribe text and mathematics (note that you can use LaTeX) and don't forget to give proper attribution to your sources! $\endgroup$ – Raphael Oct 19 '17 at 5:34
  • $\begingroup$ Which techniques where shown to you in class? $\endgroup$ – Raphael Oct 19 '17 at 5:35
  • 1
    $\begingroup$ @Raphael only induction and strong induction. We haven't been taught anything about correctness of algorithms or anything. But so far I've read a bit online, and I think that I have proven the loop invariant and now I have to use the loop invariant to prove the correctness of the algorithm $\endgroup$ – tonytouch Oct 19 '17 at 5:53
  • $\begingroup$ @D.W. Well I guess I have to show that the algorithm returns true when x=0 and false when x!=0. $\endgroup$ – tonytouch Oct 19 '17 at 5:55

To prove that the algorithm is correct, we assume that the loop invariant $x_n + by_n = a$ is true per induction.

we have the following two cases:

case 1:

If MUL(a,b) returns true, then $x_n = 0$ and $y_n = n$,


$x_n + by_n =a \rightarrow bn = a \rightarrow a$ is a multiplum of b

case 2:

if MUL(a,b) returns false, then $x_n \not= 0$, so we have

$x_n + by_n = a \rightarrow bn \not= a \rightarrow a$ is not a divisor of b.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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