From 4bd03ca62ba3a97ec0d8dca33ce1993b577b153e Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Mon, 5 Mar 2012 18:19:10 -0800
Subject: Dafny: added experimental feature {:autocontracts} to de-clutter
 idiomatic specifications

---
 Test/dafny1/Answer                  |   4 ++
 Test/dafny1/ExtensibleArrayAuto.dfy | 113 ++++++++++++++++++++++++++++++++++++
 Test/dafny1/runtest.bat             |   3 +-
 3 files changed, 119 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny1/ExtensibleArrayAuto.dfy

(limited to 'Test/dafny1')

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
-- 
cgit v1.2.3