diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-11-19 07:45:36 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-11-19 07:45:36 -0800 |
| commit | 3e6b9ca45da9eba02cf1cba553b129fd039f03df (patch) | |
| tree | 72cc5e190a788a53a706561db0a6000172f7ab37 /Test/dafny1 | |
| parent | 5c536e42edfe37a4c35191bedd02aa11f63a1c28 (diff) | |
Beautified a test program
Diffstat (limited to 'Test/dafny1')
| -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) {
|