Renamed a variable in some test cases

2 files changed, 34 insertions, 25 deletions

diff --git a/Test/vstte2012/RingBuffer.dfy b/Test/vstte2012/RingBuffer.dfy
index 5262e462..8684b1c8 100644
--- a/Test/vstte2012/RingBuffer.dfy
+++ b/Test/vstte2012/RingBuffer.dfy
@@ -13,15 +13,15 @@ class RingBuffer<T>
     this in Repr && null !in Repr &&

     data != null && data in Repr &&

     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]

+    (N == 0 ==> len == start == 0 && Contents == []) &&

+    (N != 0 ==> len <= N && start < N) &&

+    Contents == if start + len <= N then data[start..start+len] 

+                                    else data[start..] + data[..start+len-N]

   }

 

   // private implementation:

   var data: array<T>;

-  var first: nat;

+  var start: nat;

   var len: nat;

 

   constructor Create(n: nat)

@@ -32,7 +32,7 @@ class RingBuffer<T>
     Repr := {this};

     data := new T[n];

     Repr := Repr + {data};

-    first, len := 0, 0;

+    start, len := 0, 0;

     Contents, N := [], n;

   }

 

@@ -51,7 +51,7 @@ class RingBuffer<T>
     requires Contents != [];

     ensures x == Contents[0];

   {

-    x := data[first];

+    x := data[start];

   }

 

   method Push(x: T)

@@ -61,8 +61,8 @@ class RingBuffer<T>
     ensures Valid() && fresh(Repr - old(Repr));

     ensures Contents == old(Contents) + [x] && N == old(N);

   {

-    var nextEmpty := if first + len < data.Length 

-                     then first + len else first + len - data.Length;

+    var nextEmpty := if start + len < data.Length 

+                     then start + len else start + len - data.Length;

     data[nextEmpty] := x;

     len := len + 1;

     Contents := Contents + [x];

@@ -75,8 +75,8 @@ class RingBuffer<T>
     ensures Valid() && fresh(Repr - old(Repr));

     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;

+    x := data[start];

+    start, len := if start + 1 == data.Length then 0 else start + 1, len - 1;

     Contents := Contents[1..];

   }

 }

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
index 712236a8..73a6c3fd 100644
--- a/Test/vstte2012/RingBufferAuto.dfy
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -6,25 +6,25 @@ class {:autocontracts} RingBuffer<T>
 

   // private implementation:

   var data: array<T>;

-  var first: nat;

+  var start: nat;

   var len: nat;

 

   // Valid encodes the consistency of RingBuffer objects (think, invariant)

-  predicate Valid

+  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]

+    (N == 0 ==> len == start == 0 && Contents == []) &&

+    (N != 0 ==> len <= N && start < N) &&

+    Contents == if start + len <= N then data[start..start+len] 

+                                    else data[start..] + data[..start+len-N]

   }

 

   constructor Create(n: nat)

     ensures Contents == [] && N == n;

   {

     data := new T[n];

-    first, len := 0, 0;

+    start, len := 0, 0;

     Contents, N := [], n;

   }

 

@@ -39,15 +39,24 @@ class {:autocontracts} RingBuffer<T>
     requires Contents != [];

     ensures x == Contents[0];

   {

-    x := data[first];

+    x := data[start];

   }

 

   method Enqueue(x: T)

-    requires |Contents| != N;

-    ensures Contents == old(Contents) + [x] && N == old(N);

+    //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;

+    if (len == data.Length) {

+      var more := data.Length;

+      var d := new T[data.Length + more];

+      parallel (i | 0 <= i < data.Length) {

+        d[if i < start then i else i + more] := data[i];

+      }

+      data := d;

+      N, start := N + more, start + more;

+    }

+    var nextEmpty := if start + len < data.Length 

+                     then start + len else start + len - data.Length;

     data[nextEmpty] := x;

     len := len + 1;

     Contents := Contents + [x];

@@ -57,8 +66,8 @@ class {:autocontracts} RingBuffer<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;

+    x := data[start];

+    start, len := if start + 1 == data.Length then 0 else start + 1, len - 1;

     Contents := Contents[1..];

   }

 }