Invert LHS sub-expressions in forall assignment statements, which gives the opportunity to designate a good trigger.

2 files changed, 19 insertions, 1 deletions

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
index a9d36932..a4bdf0a0 100644
--- a/Test/vstte2012/RingBufferAuto.dfy
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -56,6 +56,24 @@ class {:autocontracts} RingBuffer<T>
     Contents := Contents + [x];

   }

 

+  method ResizingEnqueue(x: T)

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

+  {

+    if data.Length == len {

+      var more := data.Length + 1;

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

+      forall i | 0 <= i < data.Length {

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

+      }

+      N, data, start := N + more, d, if len == 0 then 0 else 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];

+  }

+

   method Dequeue() returns (x: T)

     requires Contents != [];

     modifies Repr;

diff --git a/Test/vstte2012/RingBufferAuto.dfy.expect b/Test/vstte2012/RingBufferAuto.dfy.expect
index aeb37948..b06ff8fc 100644
--- a/Test/vstte2012/RingBufferAuto.dfy.expect
+++ b/Test/vstte2012/RingBufferAuto.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 13 verified, 0 errors

+Dafny program verifier finished with 15 verified, 0 errors