CODEWITHSUNDEEP
proof-of-correctnesshoare-logic
nlimits
nlimits

Reputation: 113

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?

Upvotes: 1

Views: 573

Answers (1)

d125q
d125q

Reputation: 1666

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.

Upvotes: 1

Related Questions