diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-05 18:19:10 -0800 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-05 18:19:10 -0800 |
| commit | 4bd03ca62ba3a97ec0d8dca33ce1993b577b153e (patch) | |
| tree | ebc35e54315f9f456642683f0f79a5b332cd9cf4 /Test/dafny1/ExtensibleArrayAuto.dfy | |
| parent | 6ad022644a490a0019993325324782ccd58cff01 (diff) | |
Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic specifications
Diffstat (limited to 'Test/dafny1/ExtensibleArrayAuto.dfy')
| -rw-r--r-- | Test/dafny1/ExtensibleArrayAuto.dfy | 113 |
1 files changed, 113 insertions, 0 deletions
diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy new file mode 100644 index 00000000..f7f97deb --- /dev/null +++ b/Test/dafny1/ExtensibleArrayAuto.dfy @@ -0,0 +1,113 @@ +class {:autocontracts} ExtensibleArray<T> {
+ ghost var Contents: seq<T>;
+
+ 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
+ {
+ // shape of data structure
+ elements != null && elements.Length == 256 &&
+ (more != null ==>
+ 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])
+ }
+
+ constructor Init()
+ ensures Contents == [];
+ {
+ elements := new T[256];
+ more := null;
+ length := 0;
+ M := 0;
+
+ Contents := [];
+ }
+
+ method Get(i: int) returns (t: T)
+ requires 0 <= i && i < |Contents|;
+ ensures t == Contents[i];
+ decreases Repr;
+ {
+ if (M <= i) {
+ t := elements[i - M];
+ } else {
+ var arr := more.Get(i / 256);
+ t := arr[i % 256];
+ }
+ }
+
+ method Set(i: int, t: T)
+ requires 0 <= i && i < |Contents|;
+ ensures Contents == old(Contents)[i := t];
+ {
+ if (M <= i) {
+ elements[i - M] := t;
+ } else {
+ var arr := more.Get(i / 256);
+ arr[i % 256] := t;
+ }
+ Contents := Contents[i := t];
+ }
+
+ method Append(t: T)
+ ensures Contents == old(Contents) + [t];
+ decreases Repr;
+ {
+ if (length == 0 || length % 256 != 0) {
+ // there is room in "elements"
+ elements[length - M] := t;
+ } else {
+ if (more == null) {
+ more := new ExtensibleArray<array<T>>.Init();
+ Repr := Repr + {more} + more.Repr;
+ }
+ // "elements" is full, so move it into "more" and allocate a new array
+ more.Append(elements);
+ Repr := Repr + more.Repr;
+ M := M + 256;
+ elements := new T[256];
+ Repr := Repr + {elements};
+ elements[0] := t;
+ }
+ length := length + 1;
+ Contents := Contents + [t];
+ }
+}
+
+method Main() {
+ var a := new ExtensibleArray<int>.Init();
+ var n := 0;
+ while (n < 256*256+600)
+ invariant a.Valid() && fresh(a.Repr);
+ invariant |a.Contents| == n;
+ {
+ a.Append(n);
+ n := n + 1;
+ }
+ var k := a.Get(570); print k, "\n";
+ k := a.Get(0); print k, "\n";
+ k := a.Get(1000); print k, "\n";
+ a.Set(1000, 23);
+ k := a.Get(0); print k, "\n";
+ k := a.Get(1000); print k, "\n";
+ k := a.Get(66000); print k, "\n";
+}
|