CODEWITHSUNDEEP
algorithmpseudocodediscrete-mathematicsloop-invariant
NewDev90
NewDev90

Reputation: 399

Loop invariant proof on multiply algorithm

I'm currently stuck on a loop invariant proof in my home assignment. The algorithm that I need to prove correctness of, is:

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

I've tried to look at several examples of loop invariants and I have some sense of idea of how its supposed to work out. However in this algorithm above, I have two exit conditions, and I'm a bit lost on how to approach this in a loop invariant proof. In particular its the termination part I'm struggling with, around the IF and ELSE statements.

So far what I've constructed is simply by looking at the termination of the algorithm in which case if x = 0 then it returns the value of y containing the value of n (number of iterations in the while loop), where as if x is not 0, and x < b then it returns -1. I just have a feeling I need to prove this some how.

I hope someone can help share some light on this for me, as the similar cases I've found in here, have not been sufficient.

Thanks alot in advance for your time.

Upvotes: 0

Views: 1224

Answers (2)

Alex M
Alex M

Reputation: 915

Provided that the algorithm terminates (for this let's assume a>0 and b>0, which is sufficient), one invariant is that at every iteration of your while loop, you have x + by = a.

Proof:

  • at first, x = a and y = 0 so that's ok
  • If x + by = a, then (x - b) + (y + 1)b = a, which are the values of x and y for your next iteration

Illustration:

    Multiply(a,b)
        x=a
        y=0
        // x + by = a, is true
        WHILE x>=b DO
            // x + by = a, is true
            x=x-b // X = x - b
            y=y+1 // Y = y + 1
            // x + by = a
            // x - b + by + b = a
            // (x-b) + (y+1)b = a
            // X + bY = a, is still true
        // x + by = a, will remain true when you exit the loop
        // since we exited the loop, x < b
        IF x=0 THEN
            // 0 + by = a, and 0 < b
            // y = a/b
            RETURN(y)
        ELSE
            RETURN(-1)

This algorithm returns a/b when b divides a, and -1 otherwise. Multiply does not quite sound like an appropriate name for it...

Upvotes: 2

Edward Doolittle
Edward Doolittle

Reputation: 4100

We can't prove correctness without a specification of exactly what the function is supposed to do, which I can't find in your question. Even the name of the function doesn't help: as noted already, your function returns a/b most of the time when b divides a, and -1 otherwise. Multiply is an inappropriate name for it.

Furthermore, if b=0 and a>=b the "algorithm" doesn't terminate so it isn't even an algorithm.

As Alex M noted, a loop invariant for the loop is x + by = a. At the moment the loop exits, we also have x < b. There are no other guarantees on x because (presumably) a could be negative. If we had a guarantee that a and b are positive, then we could guarantee that 0<=x<b at the moment the loop exits, which would mean that it implements the division with remainder algorithm (at the end of the loop, y is quotient and x is remainder, and it terminates by an "infinite descent" type argument: a decreasing sequence of positive integers x must terminate). Then you could conclude that if x=0, b divides a evenly, and the quotient is returned, otherwise -1 is returned.

But that is not a proof, because we are lacking a specification for what the algorithm is supposed to do, and a specification on restrictions on its inputs. (Are a and b any positive integers? Negative and 0 not allowed?)

Upvotes: 0

Related Questions