1

这是一个例子，它接受一个整数lim并返回一个严格小于lim偶数的所有整数的序列。

只有第二个不变量中的向后方向... <==> ...不验证。我已经尝试过一段时间了，但我无法弄清楚。

任何帮助深表感谢！

method evens(lim : int) returns (ret : seq<int>)
  requires 0 < lim
{
  ret := [];

  var i := 0;

  while (i < lim)
    invariant 0 <= i <= lim
    invariant forall idx :: 0 <= idx < i ==> (idx % 2 == 0 <==> idx in ret)
  {
    if (i % 2 == 0) {
      ret := [i] + ret;
    }

    i := i + 1;
  }
}
4

1 回答 1

1

您需要添加此不变量：

invariant forall idx :: idx in ret ==> idx % 2 == 0

这意味着ret数组中的所有成员都可以被 2 整除。不变量

invariant forall idx :: 0 <= idx < i ==> (idx in ret ==> idx % 2 == 0)

失败是因为ret可能包含条件0 <= idx < i为真但不能被 2 整除的成员。考虑以下代码：http ://www.rise4fun.com/Dafny/W7RwL

于 2016-12-04T19:23:09.797 回答