循环不变Hoare逻辑

Question

我有一个程序，我应该找到一个循环不变量，然后提供一个证明。

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

唯一合乎逻辑的循环不变对我来说是res<=x*y，这是后置条件简单，但我不认为它最好的一个同去。也许还有其他建议？

Answer 1

这项工作？

{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 

通过这些条件，你应该能够同时显示，该方案是完全正确（即，如果循环结束，答案是正确的），它终止。尽管我认为你需要y是一个整数的前提条件。