From 19895aaed833d16bad36a07e9459abc882ccd6b6 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 24 Jun 2014 10:44:38 -0700
Subject: Invert LHS sub-expressions in forall assignment statements, which
 gives the opportunity to designate a good trigger.

---
 Test/vstte2012/RingBufferAuto.dfy        | 18 ++++++++++++++++++
 Test/vstte2012/RingBufferAuto.dfy.expect |  2 +-
 2 files changed, 19 insertions(+), 1 deletion(-)

(limited to 'Test/vstte2012')

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
-- 
cgit v1.2.3