diff options
Diffstat (limited to 'Test/vstte2012')
| -rw-r--r-- | Test/vstte2012/RingBufferAuto.dfy | 18 | ||||
| -rw-r--r-- | Test/vstte2012/RingBufferAuto.dfy.expect | 2 |
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
|