Как доказать, что какое-то время всегда возвращает значение в Дафни?

Question

Я использовал оператор :| и преобразовал его в while, но теперь я не знаю, как доказать, что l oop всегда будет возвращать действительное 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;
  }
}

Как мне доказать это? Я сделал Po C на подъеме4fun: https://rise4fun.com/Dafny/LpRZA.

Большое спасибо!

Answer 1

Вроде бы достаточно добавить инвариант к l oop:

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
}