pseudocode - Prove how the algorithm works

Question

Given the pseudocode

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

I have to prove how the algorithm works.

So far I have only explained how it works, but I am not sure how you are supposed to prove how it works.

Edit: Just to clarify. I did ask this question on another thread. But the two questions are separate. The assignment I am working on consists of 3 questions. The 1st question is where I explained how the algorithm works. The 2nd question is on my other thread and the 3rd question (this thread) is where I have to prove how the algorithm I explained in question 1 works. The reason why I asked this question is not to get the answer to the question, but simply an explationation as to what I am asked to do since I can't seem to figure it out myself. Personally I would just do the same as the 1st question, but that wouldn't make much sense.

Answer 1

Try to show the Pre-condition and Post-condition of the algorithm. Pre-condition predicates the initial state before execution and Post-condition predicates the final state after execution.

The algorithm is correct if it can be proved that if the pre-condition is true, the post-condition must be true.

check this out for more details: prove how algorithm works