summaryrefslogtreecommitdiff
path: root/Test/vstte2012
diff options
context:
space:
mode:
Diffstat (limited to 'Test/vstte2012')
-rw-r--r--Test/vstte2012/RingBufferAuto.dfy18
-rw-r--r--Test/vstte2012/RingBufferAuto.dfy.expect2
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