From 9e55540491db3979e83ee588e475a5c1fd255462 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/vstte2012/Answer             |  4 +++
 Test/vstte2012/RingBufferAuto.dfy | 76 +++++++++++++++++++++++++++++++++++++++
 Test/vstte2012/runtest.bat        |  2 +-
 3 files changed, 81 insertions(+), 1 deletion(-)
 create mode 100644 Test/vstte2012/RingBufferAuto.dfy

(limited to 'Test/vstte2012')

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