loops - 如何找到这个程序的循环不变量？

Question

可能这是一个非常简单的解决方案，我只是愚蠢，但我找不到这个 while 循环的不变量。为了证明 (a+b) <= 2x，你可以取 (x+y>a+b)，所以这可能是不变量的第一部分，但对于第二部分，为了证明 2x<= (a+b +1）......你到底在做什么？我尝试了一切，但为此浪费了两个小时。

我觉得它应该很明显，我只是看不到它。

我理解关于证明部分正确性的理论。我只是找不到循环不变量，所以不变量将不胜感激，无需解释理论。

证明下列程序的部分正确性

{a<b}
x = a;
y = b;

while x < y do

    x = x+1;
    y = y-1;
done;

{(a+b) <= 2x <= (a+b+1)}

Answer 1

这是一个保证断言的循环不变量：

a + b == x + y && x <= y + 1

请注意，您猜想的不变量x+y>a+b在进入循环时不成立。

这是一个证明断言的 Dafny 程序：

method blah (a: int, b: int)
requires a < b
{
  var x := a;
  var y := b;
  while x < y
  invariant a + b == x + y && x <= y + 1
  {
    x := x + 1;
    y := y - 1;
  }
  assert (a+b) <= 2*x <= (a+b+1);
}