Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic specifications

6 files changed, 200 insertions, 2 deletions

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index ab10d944..023d80df 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -15,6 +15,10 @@ Dafny program verifier finished with 24 verified, 0 errors
 

 Dafny program verifier finished with 11 verified, 0 errors

 

+-------------------- ExtensibleArrayAuto.dfy --------------------

+

+Dafny program verifier finished with 11 verified, 0 errors

+

 -------------------- BinaryTree.dfy --------------------

 

 Dafny program verifier finished with 24 verified, 0 errors

diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy
new file mode 100644
index 00000000..f7f97deb
--- /dev/null
+++ b/Test/dafny1/ExtensibleArrayAuto.dfy
@@ -0,0 +1,113 @@
+class {:autocontracts} ExtensibleArray<T> {

+  ghost var Contents: seq<T>;

+

+  var elements: array<T>;

+  var more: ExtensibleArray<array<T>>;

+  var length: int;

+  var M: int;  // shorthand for:  if more == null then 0 else 256 * |more.Contents|

+

+  function Valid(): bool

+  {

+    // shape of data structure

+    elements != null && elements.Length == 256 &&

+    (more != null ==>

+        elements !in more.Repr &&

+        more.Valid() &&

+        |more.Contents| != 0 &&

+        forall j :: 0 <= j && j < |more.Contents| ==>

+            more.Contents[j] != null && more.Contents[j].Length == 256 &&

+            more.Contents[j] in Repr && more.Contents[j] !in more.Repr &&

+            more.Contents[j] != elements &&

+            forall k :: 0 <= k && k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]) &&

+

+    // length

+    M == (if more == null then 0 else 256 * |more.Contents|) &&

+    0 <= length && length <= M + 256 &&

+    (more != null ==> M < length) &&

+

+    // Contents

+    length == |Contents| &&

+    (forall i :: 0 <= i && i < M ==> Contents[i] == more.Contents[i / 256][i % 256]) &&

+    (forall i :: M <= i && i < length ==> Contents[i] == elements[i - M])

+  }

+

+  constructor Init()

+    ensures Contents == [];

+  {

+    elements := new T[256];

+    more := null;

+    length := 0;

+    M := 0;

+    

+    Contents := [];

+  }

+

+  method Get(i: int) returns (t: T)

+    requires 0 <= i && i < |Contents|;

+    ensures t == Contents[i];

+    decreases Repr;

+  {

+    if (M <= i) {

+      t := elements[i - M];

+    } else {

+      var arr := more.Get(i / 256);

+      t := arr[i % 256];

+    }

+  }

+

+  method Set(i: int, t: T)

+    requires 0 <= i && i < |Contents|;

+    ensures Contents == old(Contents)[i := t];

+  {

+    if (M <= i) {

+      elements[i - M] := t;

+    } else {

+      var arr := more.Get(i / 256);

+      arr[i % 256] := t;

+    }

+    Contents := Contents[i := t];

+  }

+

+  method Append(t: T)

+    ensures Contents == old(Contents) + [t];

+    decreases Repr;

+  {

+    if (length == 0 || length % 256 != 0) {

+      // there is room in "elements"

+      elements[length - M] := t;

+    } else {

+      if (more == null) {

+        more := new ExtensibleArray<array<T>>.Init();

+        Repr := Repr + {more} + more.Repr;

+      }

+      // "elements" is full, so move it into "more" and allocate a new array

+      more.Append(elements);

+      Repr := Repr + more.Repr;

+      M := M + 256;

+      elements := new T[256];

+      Repr := Repr + {elements};

+      elements[0] := t;

+    }

+    length := length + 1;

+    Contents := Contents + [t];

+  }

+}

+

+method Main() {

+  var a := new ExtensibleArray<int>.Init();

+  var n := 0;

+  while (n < 256*256+600)

+    invariant a.Valid() && fresh(a.Repr);

+    invariant |a.Contents| == n;

+  {

+    a.Append(n);

+    n := n + 1;

+  }

+  var k := a.Get(570); print k, "\n";

+  k := a.Get(0); print k, "\n";

+  k := a.Get(1000); print k, "\n";

+  a.Set(1000, 23);

+  k := a.Get(0); print k, "\n";

+  k := a.Get(1000); print k, "\n";

+  k := a.Get(66000); print k, "\n";

+}

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 524765cf..0ad75ffa 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -12,7 +12,8 @@ for %%f in (BQueue.bpl) do (
   %BPLEXE% %* %%f

 )

 

-for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy

+for %%f in (Queue.dfy PriorityQueue.dfy

+            ExtensibleArray.dfy ExtensibleArrayAuto.dfy

             BinaryTree.dfy

             UnboundedStack.dfy

             SeparationLogicList.dfy

diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer
index 15a95de1..bca270c3 100644
--- a/Test/vstte2012/Answer
+++ b/Test/vstte2012/Answer
@@ -11,6 +11,10 @@ Dafny program verifier finished with 25 verified, 0 errors
 

 Dafny program verifier finished with 13 verified, 0 errors

 

+-------------------- RingBufferAuto.dfy --------------------

+

+Dafny program verifier finished with 13 verified, 0 errors

+

 -------------------- Tree.dfy --------------------

 

 Dafny program verifier finished with 15 verified, 0 errors

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
new file mode 100644
index 00000000..49f76713
--- /dev/null
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -0,0 +1,76 @@
+class {:autocontracts} RingBuffer<T>

+{

+  // public fields that are used to define the abstraction:

+  ghost var Contents: seq<T>;  // the contents of the ring buffer

+  ghost var N: nat;  // the capacity of the ring buffer

+

+  // Valid encodes the consistency of RingBuffer objects (think, invariant).

+  // An explanation of this idiom is explained in the README file.

+  predicate Valid

+  {

+    data != null &&

+    data.Length == N &&

+    (N == 0 ==> len == first == 0 && Contents == []) &&

+    (N != 0 ==> len <= N && first < N) &&

+    Contents == if first + len <= N then data[first..first+len] 

+                                    else data[first..] + data[..first+len-N]

+  }

+

+  // private implementation:

+  var data: array<T>;

+  var first: nat;

+  var len: nat;

+

+  constructor Create(n: nat)

+    ensures Contents == [] && N == n;

+  {

+    data := new T[n];

+    first, len := 0, 0;

+    Contents, N := [], n;

+  }

+

+  method Clear()

+    ensures Contents == [] && N == old(N);

+  {

+    len := 0;

+    Contents := [];

+  }

+

+  method Head() returns (x: T)

+    requires Contents != [];

+    ensures x == Contents[0];

+  {

+    x := data[first];

+  }

+

+  method Push(x: T)

+    requires |Contents| != N;

+    ensures Contents == old(Contents) + [x] && N == old(N);

+  {

+    var nextEmpty := if first + len < data.Length 

+                     then first + len else first + len - data.Length;

+    data[nextEmpty] := x;

+    len := len + 1;

+    Contents := Contents + [x];

+  }

+

+  method Pop() returns (x: T)

+    requires Contents != [];

+    ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);

+  {

+    x := data[first];

+    first, len := if first + 1 == data.Length then 0 else first + 1, len - 1;

+    Contents := Contents[1..];

+  }

+}

+

+method TestHarness(x: int, y: int, z: int)

+{

+  var b := new RingBuffer<int>.Create(2);

+  b.Push(x);

+  b.Push(y);

+  var h := b.Pop();  assert h == x;

+  b.Push(z);

+  h := b.Pop();  assert h == y;

+  h := b.Pop();  assert h == z;

+}

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 5145cb56..770f41dc 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -8,7 +8,7 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 for %%f in (

     Two-Way-Sort.dfy

     Combinators.dfy

-    RingBuffer.dfy

+    RingBuffer.dfy RingBufferAuto.dfy

     Tree.dfy

     BreadthFirstSearch.dfy

   ) do (