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 に答える