diff options
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/ExtensibleArray.dfy | 108 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 2 |
3 files changed, 113 insertions, 1 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index d737a8cd..58d36d2d 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -11,6 +11,10 @@ Dafny program verifier finished with 22 verified, 0 errors Dafny program verifier finished with 24 verified, 0 errors
+-------------------- ExtensibleArray.dfy --------------------
+
+Dafny program verifier finished with 9 verified, 0 errors
+
-------------------- BinaryTree.dfy --------------------
Dafny program verifier finished with 24 verified, 0 errors
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy new file mode 100644 index 00000000..e60ab8ae --- /dev/null +++ b/Test/dafny1/ExtensibleArray.dfy @@ -0,0 +1,108 @@ +class ExtensibleArray<T> {
+ ghost var Contents: seq<T>;
+ ghost var Repr: set<object>;
+
+ var elements: array<T>;
+ var more: ExtensibleArray<array<T>>;
+ var length: int;
+ var M: int; // shorthand for: if more == null then 0 else 256 * |more.Contents|
+
+ function Valid(): bool
+ reads this, Repr;
+ {
+ // shape of data structure
+ this in Repr &&
+ elements != null && elements.Length == 256 && elements in Repr &&
+ (more != null ==>
+ 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| ==>
+ 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]))) &&
+
+ // length
+ M == (if more == null then 0 else 256 * |more.Contents|) &&
+ 0 <= length && 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])
+ }
+
+ method Init()
+ modifies this;
+ ensures Valid() && fresh(Repr - {this});
+ ensures Contents == [];
+ {
+ var arr := new T[256]; elements := arr;
+ more := null;
+ length := 0;
+ M := 0;
+
+ Contents := [];
+ Repr := {this}; Repr := Repr + {elements};
+ }
+
+ method Get(i: int) returns (t: T)
+ requires Valid();
+ requires 0 <= i && i < |Contents|;
+ ensures t == Contents[i];
+ decreases Repr;
+ {
+ if (M <= i) {
+ t := elements[i - M];
+ } else {
+ call arr := more.Get(i / 256);
+ t := arr[i % 256];
+ }
+ }
+
+ method Set(i: int, t: T)
+ requires Valid();
+ requires 0 <= i && i < |Contents|;
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures Contents == old(Contents)[i := t];
+ {
+ if (M <= i) {
+ elements[i - M] := t;
+ } else {
+ call arr := more.Get(i / 256);
+ arr[i % 256] := t;
+ }
+ Contents := Contents[i := t];
+ }
+
+ method Append(t: T)
+ requires Valid();
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures Contents == old(Contents) + [t];
+ decreases Repr;
+ {
+ if (length == 0 || length % 256 != 0) {
+ // there is room in "elements"
+ elements[length - M] := t;
+ } else {
+ if (length == 256) {
+ var mr := new ExtensibleArray<array<T>>; more := mr;
+ call mr.Init();
+ Repr := Repr + {mr} + mr.Repr;
+ }
+ // "elements" is full, so move it into "more" and allocate a new array
+ call more.Append(elements);
+ Repr := Repr + more.Repr;
+ M := M + 256;
+ var arr := new T[256]; elements := arr;
+ Repr := Repr + {elements};
+ elements[0] := t;
+ }
+ length := length + 1;
+ Contents := Contents + [t];
+ }
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index af1cd7bf..772d4fdb 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -11,7 +11,7 @@ for %%f in (BQueue.bpl) do ( %BPLEXE% %* %%f
)
-for %%f in (Queue.dfy PriorityQueue.dfy
+for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy
BinaryTree.dfy
UnboundedStack.dfy
SeparationLogicList.dfy
|