diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-07-07 17:24:46 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-07-07 17:24:46 -0700 |
| commit | 661faf59f8e1003cdbf339260d1293e8dd77f2df (patch) | |
| tree | 37e11e8a86658fe4d69b38572f3b6fadd8d287c9 /Test/vstte2012 | |
| parent | 8de9fcae1a91acce9a1e59f292f05a95c81b3dbc (diff) | |
| parent | 93d9965a347b1a6ad70007822f01c2b032ea5436 (diff) | |
Merge
Diffstat (limited to 'Test/vstte2012')
| -rw-r--r-- | Test/vstte2012/Answer | 24 | ||||
| -rw-r--r-- | Test/vstte2012/RingBufferAuto.dfy | 18 | ||||
| -rw-r--r-- | Test/vstte2012/RingBufferAuto.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/vstte2012/runtest.bat | 23 |
4 files changed, 19 insertions, 48 deletions
diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer deleted file mode 100644 index 43eddcb1..00000000 --- a/Test/vstte2012/Answer +++ /dev/null @@ -1,24 +0,0 @@ -
--------------------- Two-Way-Sort.dfy --------------------
-
-Dafny program verifier finished with 4 verified, 0 errors
-
--------------------- Combinators.dfy --------------------
-
-Dafny program verifier finished with 25 verified, 0 errors
-
--------------------- RingBuffer.dfy --------------------
-
-Dafny program verifier finished with 13 verified, 0 errors
-
--------------------- RingBufferAuto.dfy --------------------
-
-Dafny program verifier finished with 13 verified, 0 errors
-
--------------------- Tree.dfy --------------------
-
-Dafny program verifier finished with 15 verified, 0 errors
-
--------------------- BreadthFirstSearch.dfy --------------------
-
-Dafny program verifier finished with 22 verified, 0 errors
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
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat deleted file mode 100644 index 7e597fd4..00000000 --- a/Test/vstte2012/runtest.bat +++ /dev/null @@ -1,23 +0,0 @@ -@echo off
-setlocal
-
-set BINARIES=..\..\Binaries
-set DAFNY_EXE=%BINARIES%\Dafny.exe
-
-%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Two-Way-Sort.dfy Combinators.dfy RingBuffer.dfy RingBufferAuto.dfy Tree.dfy
-
-echo.
-echo -------------------- BreadthFirstSearch.dfy --------------------
-%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /vcsMaxKeepGoingSplits:10 %* BreadthFirstSearch.dfy
-
-rem for %%f in (
-rem Two-Way-Sort.dfy
-rem Combinators.dfy
-rem RingBuffer.dfy RingBufferAuto.dfy
-rem Tree.dfy
-rem BreadthFirstSearch.dfy
-rem ) do (
-rem echo.
-rem echo -------------------- %%f --------------------
-rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-rem )
|