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/SparseArray.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/SparseArray.dfy')
| -rw-r--r-- | Test/vacid0/SparseArray.dfy | 120 |
1 files changed, 120 insertions, 0 deletions
diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy new file mode 100644 index 00000000..da1f63bb --- /dev/null +++ b/Test/vacid0/SparseArray.dfy @@ -0,0 +1,120 @@ +class SparseArray<T> {
+ ghost var Contents: seq<T>;
+ var zero: T;
+ /*private*/ var a: seq<T>; // should really be an array
+ /*private*/ var b: seq<int>; // should really be an array
+ /*private*/ var c: seq<int>; // should really be an array
+ /*private*/ var n: int;
+ /*private*/ ghost var d: seq<int>; // would be better as an array
+ /*private*/ ghost var e: seq<int>; // would be better as an array
+ function Valid(): bool
+ reads this;
+ {
+ |a| == |Contents| &&
+ |b| == |Contents| &&
+ |c| == |Contents| &&
+ 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| ==>
+ (i in c[..n] <==> 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;
+ ensures Valid();
+ ensures |Contents| == N && this.zero == zero;
+ ensures (forall x :: x in Contents ==> x == zero);
+ {
+ var aa;
+ var ii;
+ call aa := AllocateArray(N); this.a := aa;
+ call ii := AllocateArray(N); this.b := ii;
+ call ii := AllocateArray(N); this.c := ii;
+ this.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;
+ // TODO: why doesn't this work instead of the next line? invariant (forall x :: x in s ==> x == zero);
+ invariant (forall i :: 0 <= i && i < |s| ==> s[i] == zero);
+ invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);
+ decreases N - k;
+ {
+ s := s + [zero];
+ id := id + [k];
+ k := k + 1;
+ }
+
+ this.zero := zero;
+ this.Contents := s;
+ this.d := id;
+ this.e := id;
+ }
+ 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;
+ 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 := b[i := n];
+ c := 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 := a[i := x];
+ Contents := Contents[i := x];
+ }
+
+ /* The following method is here only to simulate support of arrays in Dafny */
+ /*private*/ static method AllocateArray<G>(n: int) returns (arr: seq<G>)
+ requires 0 <= n;
+ ensures |arr| == n;
+ {
+ arr := [];
+ var i := 0;
+ while (i < n)
+ invariant i <= n && |arr| == i;
+ decreases n - i;
+ {
+ var g: G;
+ arr := arr + [g];
+ i := i + 1;
+ }
+ }
+}
|