diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny1/ExtensibleArray.dfy | 16 | ||||
| -rw-r--r-- | Test/vstte2012/RingBuffer.dfy | 35 |
2 files changed, 25 insertions, 26 deletions
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index a16cf603..adf97863 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -7,7 +7,7 @@ class ExtensibleArray<T> { var length: int;
var M: int; // shorthand for: if more == null then 0 else 256 * |more.Contents|
- function Valid(): bool
+ predicate Valid()
reads this, Repr;
{
// shape of data structure
@@ -17,21 +17,21 @@ class ExtensibleArray<T> { more in Repr && more.Repr <= Repr && this !in more.Repr && elements !in more.Repr &&
more.Valid() &&
|more.Contents| != 0 &&
- forall j :: 0 <= j && j < |more.Contents| ==>
+ forall j :: 0 <= j < |more.Contents| ==>
more.Contents[j] != null && more.Contents[j].Length == 256 &&
more.Contents[j] in Repr && more.Contents[j] !in more.Repr &&
more.Contents[j] != elements &&
- forall k :: 0 <= k && k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]) &&
+ forall k :: 0 <= k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]) &&
// length
M == (if more == null then 0 else 256 * |more.Contents|) &&
- 0 <= length && length <= M + 256 &&
+ 0 <= length <= M + 256 &&
(more != null ==> M < length) &&
// Contents
length == |Contents| &&
- (forall i :: 0 <= i && i < M ==> Contents[i] == more.Contents[i / 256][i % 256]) &&
- (forall i :: M <= i && i < length ==> Contents[i] == elements[i - M])
+ (forall i :: 0 <= i < M ==> Contents[i] == more.Contents[i / 256][i % 256]) &&
+ (forall i :: M <= i < length ==> Contents[i] == elements[i - M])
}
constructor Init()
@@ -50,7 +50,7 @@ class ExtensibleArray<T> { method Get(i: int) returns (t: T)
requires Valid();
- requires 0 <= i && i < |Contents|;
+ requires 0 <= i < |Contents|;
ensures t == Contents[i];
decreases Repr;
{
@@ -64,7 +64,7 @@ class ExtensibleArray<T> { method Set(i: int, t: T)
requires Valid();
- requires 0 <= i && i < |Contents|;
+ requires 0 <= i < |Contents|;
modifies Repr;
ensures Valid() && fresh(Repr - old(Repr));
ensures Contents == old(Contents)[i := t];
diff --git a/Test/vstte2012/RingBuffer.dfy b/Test/vstte2012/RingBuffer.dfy index 8684b1c8..35e95165 100644 --- a/Test/vstte2012/RingBuffer.dfy +++ b/Test/vstte2012/RingBuffer.dfy @@ -1,13 +1,17 @@ class RingBuffer<T>
{
- // public fields that are used to define the abstraction:
+ // public view of the class:
ghost var Contents: seq<T>; // the contents of the ring buffer
ghost var N: nat; // the capacity of the ring buffer
ghost var Repr: set<object>; // the set of objects used in the implementation
- // Valid encodes the consistency of RingBuffer objects (think, invariant).
- // An explanation of this idiom is explained in the README file.
- function Valid(): bool
+ // private implementation:
+ var data: array<T>;
+ var start: nat;
+ var len: nat;
+
+ // Valid encodes the consistency of RingBuffer objects (think, invariant)
+ predicate Valid()
reads this, Repr;
{
this in Repr && null !in Repr &&
@@ -19,11 +23,6 @@ class RingBuffer<T> else data[start..] + data[..start+len-N]
}
- // private implementation:
- var data: array<T>;
- var start: nat;
- var len: nat;
-
constructor Create(n: nat)
modifies this;
ensures Valid() && fresh(Repr - {this});
@@ -54,7 +53,7 @@ class RingBuffer<T> x := data[start];
}
- method Push(x: T)
+ method Enqueue(x: T)
requires Valid();
requires |Contents| != N;
modifies Repr;
@@ -68,7 +67,7 @@ class RingBuffer<T> Contents := Contents + [x];
}
- method Pop() returns (x: T)
+ method Dequeue() returns (x: T)
requires Valid();
requires Contents != [];
modifies Repr;
@@ -83,11 +82,11 @@ class RingBuffer<T> 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;
+ var b := new RingBuffer.Create(2);
+ b.Enqueue(x);
+ b.Enqueue(y);
+ var h := b.Dequeue(); assert h == x;
+ b.Enqueue(z);
+ h := b.Dequeue(); assert h == y;
+ h := b.Dequeue(); assert h == z;
}
|