proof-of-correctness - 循环不变霍尔逻辑

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 是整数的前提条件。