diff options
| author |  rustanleino <unknown> | 2010-05-21 18:38:47 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-05-21 18:38:47 +0000 |
| commit | 572b11dddba3bfbdc4e90beb4d7f2e076878f717 (patch) | |
| tree | 421f92d259589f7711ee1a13b58529dd59d066c6 /Test/vacid0/LazyInitArray.dfy | |
| parent | 425a4c8ff53eb2196e684b6843016baadfe60835 (diff) | |
Dafny:
* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks
Diffstat (limited to 'Test/vacid0/LazyInitArray.dfy')
| -rw-r--r-- | Test/vacid0/LazyInitArray.dfy | 105 |
1 files changed, 105 insertions, 0 deletions
diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy new file mode 100644 index 00000000..6ae00e24 --- /dev/null +++ b/Test/vacid0/LazyInitArray.dfy @@ -0,0 +1,105 @@ +class LazyInitArray<T> {
+ ghost var Contents: seq<T>;
+ var Zero: T;
+ /*private*/ var a: array<T>;
+ /*private*/ var b: array<int>;
+ /*private*/ var c: array<int>;
+ /*private*/ var n: int;
+ /*private*/ ghost var d: seq<int>;
+ /*private*/ ghost var e: seq<int>;
+ function Valid(): bool
+ reads this, a, b, c;
+ {
+ a != null && b != null && c != null &&
+ |a| == |Contents| + 1 && // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'
+ |b| == |Contents| &&
+ |c| == |Contents| &&
+ b != c &&
+ 0 <= n && n <= |c| &&
+ (forall i :: 0 <= i && i < |Contents| ==>
+ Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&
+ (forall i :: 0 <= i && i < |Contents| ==>
+ ((exists j :: 0 <= j && j < n && c[j] == i)
+ <==>
+ 0 <= b[i] && b[i] < n && c[b[i]] == i)) &&
+ // The idea behind d and e is the following:
+ // * d is a permutation of the first |Contents| natural numbers
+ // * e describes which permutation d is
+ // * c[..n] == d[..n]
+ |d| == |Contents| &&
+ |e| == |Contents| &&
+ (forall i :: 0 <= i && i < n ==> c[i] == d[i]) &&
+ (forall i :: 0 <= i && i < |d| ==> 0 <= d[i] && d[i] < |d|) &&
+ (forall i :: 0 <= i && i < |e| ==> 0 <= e[i] && e[i] < |e|) &&
+ (forall i :: 0 <= i && i < |e| ==> d[e[i]] == i)
+ }
+
+ method Init(N: int, zero: T)
+ requires 0 <= N;
+ modifies this, a, b, c;
+ ensures Valid();
+ ensures |Contents| == N && Zero == zero;
+ ensures (forall x :: x in Contents ==> x == zero);
+ {
+ var aa := new T[N+1]; a := aa;
+ var ii := new int[N]; b := ii;
+ ii := new int[N]; c := ii;
+ n := 0;
+
+ // initialize ghost variable Contents to a sequence of length N containing only zero's,
+ // and ghost variables d and e to be the identity sequences of length N
+ ghost var s := [];
+ ghost var id := [];
+ ghost var k := 0;
+ while (k < N)
+ invariant k <= N;
+ invariant |s| == k && (forall i :: 0 <= i && i < |s| ==> s[i] == zero);
+ invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);
+ {
+ s := s + [zero];
+ id := id + [k];
+ k := k + 1;
+ }
+
+ d := id;
+ e := id;
+ Zero := zero;
+ Contents := s;
+ }
+
+ method Get(i: int) returns (x: T)
+ requires Valid();
+ requires 0 <= i && i < |Contents|;
+ ensures x == Contents[i];
+ {
+ if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
+ x := a[i];
+ } else {
+ x := Zero;
+ }
+ }
+
+ method Set(i: int, x: T)
+ requires Valid();
+ requires 0 <= i && i < |Contents|;
+ modifies this, a, b, c;
+ ensures Valid();
+ ensures |Contents| == |old(Contents)| && Contents == Contents[i := x];
+ ensures Zero == old(Zero);
+ {
+ if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
+ } else {
+ assert n <= e[i];
+ b[i] := n;
+ c[n] := i;
+ ghost var t := d[n];
+ ghost var k := e[i];
+ d := d[n := i][k := t];
+ e := e[i := n][t := k];
+ n := n + 1;
+ }
+
+ a[i] := x;
+ Contents := Contents[i := x];
+ }
+}
|