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.

2 files changed, 25 insertions, 26 deletions

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index a16cf603..adf97863 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -7,7 +7,7 @@ class ExtensibleArray<T> {
   var length: int;

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

 

-  function Valid(): bool

+  predicate Valid()

     reads this, Repr;

   {

     // shape of data structure

@@ -17,21 +17,21 @@ class ExtensibleArray<T> {
         more in Repr && more.Repr <= Repr && this !in more.Repr && elements !in more.Repr &&

         more.Valid() &&

         |more.Contents| != 0 &&

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

+        forall j :: 0 <= 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]) &&

+            forall k :: 0 <= 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 &&

+    0 <= 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])

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

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

   }

 

   constructor Init()

@@ -50,7 +50,7 @@ class ExtensibleArray<T> {
 

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

     requires Valid();

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

+    requires 0 <= i < |Contents|;

     ensures t == Contents[i];

     decreases Repr;

   {

@@ -64,7 +64,7 @@ class ExtensibleArray<T> {
 

   method Set(i: int, t: T)

     requires Valid();

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

+    requires 0 <= i < |Contents|;

     modifies Repr;

     ensures Valid() && fresh(Repr - old(Repr));

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

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;

 }