From dd99220a03dbb74d1191b68a9f8b0a6eb30b32ae Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 22 Apr 2013 13:52:13 -0700
Subject: Made Test/vstte2012/RingBuffer.dfy and
 Test/dafny1/ExtensibleArray.dfy more similar to RingBufferAuto.dfy and
 ExtensibleArrayAuto.dfy, respectively, so that the effect of {:autocontracts}
 is more easily seen.

---
 Test/vstte2012/RingBuffer.dfy | 35 +++++++++++++++++------------------
 1 file changed, 17 insertions(+), 18 deletions(-)

(limited to 'Test/vstte2012')

diff --git a/Test/vstte2012/RingBuffer.dfy b/Test/vstte2012/RingBuffer.dfy
index 8684b1c8..35e95165 100644
--- a/Test/vstte2012/RingBuffer.dfy
+++ b/Test/vstte2012/RingBuffer.dfy
@@ -1,13 +1,17 @@
 class RingBuffer<T>
 {
-  // public fields that are used to define the abstraction:
+  // public view of the class:
   ghost var Contents: seq<T>;  // the contents of the ring buffer
   ghost var N: nat;  // the capacity of the ring buffer
   ghost var Repr: set<object>;  // the set of objects used in the implementation
 
-  // Valid encodes the consistency of RingBuffer objects (think, invariant).
-  // An explanation of this idiom is explained in the README file.
-  function Valid(): bool
+  // private implementation:
+  var data: array<T>;
+  var start: nat;
+  var len: nat;
+
+  // Valid encodes the consistency of RingBuffer objects (think, invariant)
+  predicate Valid()
     reads this, Repr;
   {
     this in Repr && null !in Repr &&
@@ -19,11 +23,6 @@ class RingBuffer<T>
                                     else data[start..] + data[..start+len-N]
   }
 
-  // private implementation:
-  var data: array<T>;
-  var start: nat;
-  var len: nat;
-
   constructor Create(n: nat)
     modifies this;
     ensures Valid() && fresh(Repr - {this});
@@ -54,7 +53,7 @@ class RingBuffer<T>
     x := data[start];
   }
 
-  method Push(x: T)
+  method Enqueue(x: T)
     requires Valid();
     requires |Contents| != N;
     modifies Repr;
@@ -68,7 +67,7 @@ class RingBuffer<T>
     Contents := Contents + [x];
   }
 
-  method Pop() returns (x: T)
+  method Dequeue() returns (x: T)
     requires Valid();
     requires Contents != [];
     modifies Repr;
@@ -83,11 +82,11 @@ class RingBuffer<T>
 
 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;
+  var b := new RingBuffer.Create(2);
+  b.Enqueue(x);
+  b.Enqueue(y);
+  var h := b.Dequeue();  assert h == x;
+  b.Enqueue(z);
+  h := b.Dequeue();  assert h == y;
+  h := b.Dequeue();  assert h == z;
 }
-- 
cgit v1.2.3