# How to find the loop invariant in hoare triples

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.

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