CODEWITHSUNDEEP
pythoncorrectnessproof-of-correctness
Dew Man7
Dew Man7

Reputation: 33

Loop Iterative Program Correctness Example - Loop Invariants and Program Termination

I need help proving the correctness of an iterative program:

def term_ex_2(x,y):
 ''' Pre: x and y are natural numbers '''
 a = x
 b = y
 while a >= 0 or b >= 0:
     if a > 0:
         a -= 1
     else:
         b -= 1
 return x * y

I know that I need to somehow find a loop invariant and prove it by induction on a loop. The problem is that the if/else statements here confuse me on how to come up with one.

I also have to prove whether the program terminates or not after that.

I have a general understanding on what the step by step process is but I don't know where to start on this example from the homework.

Any advice will be appreciated.

Upvotes: 0

Views: 254

Answers (1)

swag2198
swag2198

Reputation: 2696

Note that in every iteration of your outer while loop, either a or b decreases by 1.

Since x and y are assumed to be natural numbers, both of them are initially > 0.

Loop Invariant: a >= 0 (Other possibilities might be there!)

Also, the program does not terminate, which is quite evident from the loop invariant above as it forces the while loop to evaluate to true always.

Proof sketch: As long as a > 0, the loop keeps on decrementing a till it reaches 0. Then the else condition starts executing which continues to decrement b forever as a == 0 makes the while loop iterate again and again.

Classic use of putting a loop invariant itself in the loop termination condition to make the loop loop infinitely!

Upvotes: 0

Related Questions