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.

1 files changed, 17 insertions, 18 deletions

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;

 }