diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-05 18:19:10 -0800 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-05 18:19:10 -0800 |
| commit | 9e55540491db3979e83ee588e475a5c1fd255462 (patch) | |
| tree | 91c50d53a73ad8f864bfdf94ee1a635268e8277d /Test/vstte2012 | |
| parent | a99b88779bd11f102ef69d94bc284d2a35b53888 (diff) | |
Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic specifications
Diffstat (limited to 'Test/vstte2012')
| -rw-r--r-- | Test/vstte2012/Answer | 4 | ||||
| -rw-r--r-- | Test/vstte2012/RingBufferAuto.dfy | 76 | ||||
| -rw-r--r-- | Test/vstte2012/runtest.bat | 2 |
3 files changed, 81 insertions, 1 deletions
diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer index 15a95de1..bca270c3 100644 --- a/Test/vstte2012/Answer +++ b/Test/vstte2012/Answer @@ -11,6 +11,10 @@ Dafny program verifier finished with 25 verified, 0 errors 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
diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy new file mode 100644 index 00000000..49f76713 --- /dev/null +++ b/Test/vstte2012/RingBufferAuto.dfy @@ -0,0 +1,76 @@ +class {:autocontracts} RingBuffer<T>
+{
+ // public fields that are used to define the abstraction:
+ ghost var Contents: seq<T>; // the contents of the ring buffer
+ ghost var N: nat; // the capacity of the ring buffer
+
+ // Valid encodes the consistency of RingBuffer objects (think, invariant).
+ // An explanation of this idiom is explained in the README file.
+ predicate Valid
+ {
+ data != null &&
+ data.Length == N &&
+ (N == 0 ==> len == first == 0 && Contents == []) &&
+ (N != 0 ==> len <= N && first < N) &&
+ Contents == if first + len <= N then data[first..first+len]
+ else data[first..] + data[..first+len-N]
+ }
+
+ // private implementation:
+ var data: array<T>;
+ var first: nat;
+ var len: nat;
+
+ constructor Create(n: nat)
+ ensures Contents == [] && N == n;
+ {
+ data := new T[n];
+ first, len := 0, 0;
+ Contents, N := [], n;
+ }
+
+ method Clear()
+ ensures Contents == [] && N == old(N);
+ {
+ len := 0;
+ Contents := [];
+ }
+
+ method Head() returns (x: T)
+ requires Contents != [];
+ ensures x == Contents[0];
+ {
+ x := data[first];
+ }
+
+ method Push(x: T)
+ requires |Contents| != N;
+ ensures Contents == old(Contents) + [x] && N == old(N);
+ {
+ var nextEmpty := if first + len < data.Length
+ then first + len else first + len - data.Length;
+ data[nextEmpty] := x;
+ len := len + 1;
+ Contents := Contents + [x];
+ }
+
+ method Pop() returns (x: T)
+ requires Contents != [];
+ ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);
+ {
+ x := data[first];
+ first, len := if first + 1 == data.Length then 0 else first + 1, len - 1;
+ Contents := Contents[1..];
+ }
+}
+
+method TestHarness(x: int, y: int, z: int)
+{
+ var b := new RingBuffer<int>.Create(2);
+ b.Push(x);
+ b.Push(y);
+ var h := b.Pop(); assert h == x;
+ b.Push(z);
+ h := b.Pop(); assert h == y;
+ h := b.Pop(); assert h == z;
+}
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat index 5145cb56..770f41dc 100644 --- a/Test/vstte2012/runtest.bat +++ b/Test/vstte2012/runtest.bat @@ -8,7 +8,7 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe for %%f in (
Two-Way-Sort.dfy
Combinators.dfy
- RingBuffer.dfy
+ RingBuffer.dfy RingBufferAuto.dfy
Tree.dfy
BreadthFirstSearch.dfy
) do (
|