How to find the loop invariant in hoare triples

Question

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.

Answer 1

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