diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny1/ExtensibleArrayAuto.dfy | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy index f7f97deb..3e91fa4b 100644 --- a/Test/dafny1/ExtensibleArrayAuto.dfy +++ b/Test/dafny1/ExtensibleArrayAuto.dfy @@ -6,7 +6,7 @@ class {:autocontracts} ExtensibleArray<T> { var length: int;
var M: int; // shorthand for: if more == null then 0 else 256 * |more.Contents|
- function Valid(): bool
+ predicate Valid()
{
// shape of data structure
elements != null && elements.Length == 256 &&
@@ -14,21 +14,21 @@ class {:autocontracts} ExtensibleArray<T> { 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()
@@ -43,7 +43,7 @@ class {:autocontracts} ExtensibleArray<T> { }
method Get(i: int) returns (t: T)
- requires 0 <= i && i < |Contents|;
+ requires 0 <= i < |Contents|;
ensures t == Contents[i];
decreases Repr;
{
@@ -56,7 +56,7 @@ class {:autocontracts} ExtensibleArray<T> { }
method Set(i: int, t: T)
- requires 0 <= i && i < |Contents|;
+ requires 0 <= i < |Contents|;
ensures Contents == old(Contents)[i := t];
{
if (M <= i) {
|