# Proof of correctness of algorithm

Can someone help me prove the correctness of this algorithm:

MUL(a,b)
x=a
y=b
WHILE x≥b DO
x=x-b
y=y+1
IF x=0 THEN
RETURN(true)
ELSE
RETURN(false)

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.

• First step: define what correctness means, for this algorithm. – D.W. Oct 19 '17 at 5:32
• 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! – Raphael Oct 19 '17 at 5:34
• Which techniques where shown to you in class? – Raphael Oct 19 '17 at 5:35
• @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 – tonytouch Oct 19 '17 at 5:53
• @D.W. Well I guess I have to show that the algorithm returns true when x=0 and false when x!=0. – 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$$,

so

$$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.