# Loop invariant Hoare Logic

I have a program, where I should find a loop invariant and then provide a proof.

{x>=0 && y>=0} // precondition res:=0; i:=0; while (i<y) do res:=res+x; i:=i+1; od {res:=x*y} //postcondition

The only logical loop invariant for me is res<=x*y, which is straightforward from postcondition, but I dont think that it the best one to go on with. Maybe any other suggestions?

## Answers

Would this work?

{x>=0 && y>=0} // precondition res:=0; i:=0; while (i<y) do {res=x*i} // invariant res:=res+x; i:=i+1; {res=x*i} // invariant end {res=x*y} //postcondition

By these conditions you should be able to show both that the program is partially correct (i.e. if the loop terminates, the answer is correct) and that it terminates. Although I suppose you need the precondition that y is an integer, too.