1
$\begingroup$

Hey I am new to Hoare triples, and I can't understand on finding the loop invariants in hypothesis. For example this while loop

[x>1 & y>1] WHILE x>0 DO x:=x-1; y:=y+2 END [x+y>5].

The invariant is [2x + y > 5] but I don't understand on how to find it. A step by step explanation on how to find it will be greatly appreciated.

$\endgroup$
1
$\begingroup$

First understand the meaning of the loop invariant. It means a condition which is true in every iteration of the program/algorithm at the begining as well as at the termination of the loop. Your program is something like this.

$$ x > 1 \text{ and } y >1 $$

$$\text{ While } x >0 $$

$$\hspace{4cm}\text{ Do } x:= x - 1, y:=y+2$$

$$\text{ End }$$

$$x + y > 5$$

$2x+y >5$ is an invariant as you described. It is visible from the program that both $x$ and $y$ will be greater than $1$ during the first iterataion of the loop. So in the first iteration of while loop $2x+y > 5$(you can prove it). Notice in each iteration of the while loop the value of the $x$ gets decrease by value $1$ and value of y is getting increase by two so inequality $2x+ y >5$ will be satisfied. You can prove it. Now come to the termination condition, at this point $x$ will be a negative number and my claim is value of $y$ is going to be at least $5$. Thus the invariant $2x+y > 5$ si true throught the iteration of the while loop.

Example :

Let $x=2$ and $y=2$, then $2 \times 2+2 = 6 > 5$ is satisfied. Now in the second iteration $x = 1, y=4$ so $1 \times 2+4 > 5$ satisfied. Now $x = 0, y = 6$, loop terminated, $2 \times 0+6 > 5$.

| cite | improve this answer | |
$\endgroup$

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.