0

我有以下 zaMap（在此处查看完整代码：http ://rise4fun.com/Dafny/LCaM ）：

class zaMap {
  var busybits :array<bool>;
  var keys : array<int>;
  var values : array<int>;

  predicate wellformed ()
    reads busybits, keys, values, this
  {
    busybits != null && keys != null && values != null &&
    keys != values &&
    busybits.Length == keys.Length &&
    keys.Length == values.Length
  }

  // ... more predicates and methods follow


  method put(k : int, v : int) returns (success : bool)
    requires wellformed()
    modifies busybits, keys, values
    ensures !success ==> full()
    ensures success ==> mapsto(k, v)
  {
    var i := findEmpty();
    if (i < 0)
    {
      success := false;
      return;
    }
    assert !busybits[i];
    busybits[i] := true;
    keys[i] := k;
    values[i] := v;
    success := true;
  }
//...

现在我想为该put方法添加更多规范。例如，我想ensure，如果返回值为success == true，则映射!full()在函数调用之前，或者等效地，如果映射不是full()，则保证put存在。

问题是，在前置条件“需要”中我还不知道它会返回什么，而在后置条件中“确保”我不再有原始地图。人们对此怎么办？

4

1 回答 1

1

您可以使用old关键字。让我们看一个例子。以下方法将包含该元素的数组的所有位置设置为零x，其余部分保持原样。这是代码：

method setToZero(a: array<int>, x : int )
requires a != null;
modifies a;
ensures forall i :: 0 <= i < a.Length && old(a[i]) == x ==> a[i] == 0;
ensures forall i :: 0 <= i < a.Length && old(a[i]) != x ==> a[i] == old(a[i]);
{
  var j := 0;
  while (j < a.Length)
  invariant 0 <= j <= a.Length;
  invariant forall i :: 0 <= i < j && old(a[i]) == x ==> a[i] == 0;
  invariant forall i :: 0 <= i < j && old(a[i]) != x ==> a[i] == old(a[i]);
  invariant forall i :: j <= i < a.Length ==> a[i] == old(a[i]);
   {
    if (a[j] == x) {
      a[j] := 0;
    }
    j := j + 1;
  }
}
于 2015-06-11T10:26:43.243 回答