Loop invariant Hoare Logic

Question

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?

Answer 1

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.