如何找到该程序的循环不变

Question

可能是一个非常简单的解决方案，我只是愚蠢的，但是我找不到循环时不变的。为了证明(a b(＆lt; = 2x，您可以接受(x y> a b(，所以这可能是不变的第一部分，但在第二部分中，以证明2x＆lt; =(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);
}