带有 return 的 Dafny 循环

Question

如何证明以下 Dafny 程序？

method return_loop() returns (r:int)
ensures r == 5
{
  var i := 0;
  while i < 10
    invariant 0<= i <= 10
  {
    if i == 5{
       return i;
    }
    i := i + 1;
  }
  return i;
 }

我读过类似的文章Dafny 对带中断的循环了解多少？，但仍然无法证明上面的程序。

Answer 1

我添加了一个

found

标志，它起作用了：

method return_loop() returns (r:int)
  ensures r == 5
{
  var i := 0;
  var n := 10;
  var found := false;
  while i < n
  decreases n - i
  invariant 0<= i <= n
  {
    if i == 5{
       found := true;
       return i;
    }
    i := i + 1;
  }
  assert (!found  ==> r != 5) || (found && r == 5);
  return i;
}

有没有更好的方法来证明这一点？