dafny - 如何证明一段时间总是在 Dafny 中返回一个值？

Question

我正在使用:|运算符并将其转换为 while，但现在我不知道如何证明循环将始终返回有效的x. 我有以下代码：

method test(a : array<int>) returns (z : int)
  requires exists x. 0 <= x < a.Length && P(a[x]);
  ensures P(a[x]);
{
  var x :| 0 <= x < a.Length && P(a[x]);
  return x;
}

我将其更改为：

method test(a : array<int>) returns (z : int)
  requires exists x. 0 <= x < a.Length && P(a[x]);
  ensures P(a[x]);
{
  var x := 0;
  while (x < a.Length) {
    if (P(a[x])) {
      return x;
    }
    x := x + 1;
  }
}

我该怎么证明？我在rise4fun 上做了一个PoC：https ://rise4fun.com/Dafny/LpRZA 。

非常感谢！

标签： dafny

Answer 1

似乎在循环中添加一个不变量就足够了：

method test(a : array<int>) returns (z : int)
  requires exists x. 0 <= x < a.Length && P(a[x]);
  ensures P(a[x]);
{
  var x := 0;
  while (x < a.Length) 
    invariant exists x' :: x <= x' < a.Length && P(a[x']);
  {
    if (P(a[x])) {
      return x;
    }
    x := x + 1;
  }

  assert false; // be sure that it does not reach here
}