diff options
| author |  rustanleino <unknown> | 2011-02-16 08:12:43 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-02-16 08:12:43 +0000 |
| commit | 79319c49d31f844b57c65c5adc7755ca788af7a6 (patch) | |
| tree | 22119904af405cd76056581475e13bf2e81f1634 /Test/dafny1/ExtensibleArray.dfy | |
| parent | ebebfa656798e7cf3c381d124625dffbc5236b8f (diff) | |
Dafny: added ExtensibleArray program as a test
Diffstat (limited to 'Test/dafny1/ExtensibleArray.dfy')
| -rw-r--r-- | Test/dafny1/ExtensibleArray.dfy | 108 |
1 files changed, 108 insertions, 0 deletions
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];
+ }
+}
|