summaryrefslogtreecommitdiff
path: root/Test/vacid0
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-05-21 18:38:47 +0000
committerGravatar rustanleino <unknown>2010-05-21 18:38:47 +0000
commit2fc9a47b200589fae14f698e7546553a0b31aec2 (patch)
treeae0fd61bcd66c4f92833c33f82de518a718bfb7c /Test/vacid0
parent9657b7042a5a55fe96bc9b7560c473876d7efa60 (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')
-rw-r--r--Test/vacid0/Answer12
-rw-r--r--Test/vacid0/Composite.dfy160
-rw-r--r--Test/vacid0/LazyInitArray.dfy105
-rw-r--r--Test/vacid0/SparseArray.dfy120
-rw-r--r--Test/vacid0/runtest.bat12
5 files changed, 409 insertions, 0 deletions
diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer
new file mode 100644
index 00000000..6f270f92
--- /dev/null
+++ b/Test/vacid0/Answer
@@ -0,0 +1,12 @@
+
+-------------------- LazyInitArray.dfy --------------------
+
+Dafny program verifier finished with 7 verified, 0 errors
+
+-------------------- SparseArray.dfy --------------------
+
+Dafny program verifier finished with 9 verified, 0 errors
+
+-------------------- Composite.dfy --------------------
+
+Dafny program verifier finished with 14 verified, 0 errors
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
new file mode 100644
index 00000000..28074c7b
--- /dev/null
+++ b/Test/vacid0/Composite.dfy
@@ -0,0 +1,160 @@
+class Composite {
+ var left: Composite;
+ var right: Composite;
+ var parent: Composite;
+ var val: int;
+ var sum: int;
+
+ function Valid(S: set<Composite>): bool
+ reads this, parent, left, right;
+ {
+ this in S &&
+ (parent != null ==> parent in S && (parent.left == this || parent.right == this)) &&
+ (left != null ==> left in S && left.parent == this && left != right) &&
+ (right != null ==> right in S && right.parent == this && left != right) &&
+ sum == val + (if left == null then 0 else left.sum) + (if right == null then 0 else right.sum)
+ }
+
+ function Acyclic(S: set<Composite>): bool
+ reads S;
+ {
+ this in S &&
+ (parent != null ==> parent.Acyclic(S - {this}))
+ }
+
+ method Init(x: int)
+ modifies this;
+ ensures Valid({this}) && Acyclic({this}) && val == x && parent == null;
+ {
+ parent := null;
+ left := null;
+ right := null;
+ val := x;
+ sum := val;
+ }
+
+ method Update(x: int, ghost S: set<Composite>)
+ requires this in S && Acyclic(S);
+ requires (forall c :: c in S ==> c != null && c.Valid(S));
+ modifies S;
+ ensures (forall c :: c in S ==> c.Valid(S));
+ ensures (forall c :: c in S ==> c.left == old(c.left) && c.right == old(c.right) && c.parent == old(c.parent));
+ ensures (forall c :: c in S && c != this ==> c.val == old(c.val));
+ ensures val == x;
+ {
+ var delta := x - val;
+ val := x;
+ call Adjust(delta, S, S);
+ }
+
+ method Add(ghost S: set<Composite>, child: Composite, ghost U: set<Composite>)
+ requires this in S && Acyclic(S);
+ requires (forall c :: c in S ==> c != null && c.Valid(S));
+ requires child != null && child in U;
+ requires (forall c :: c in U ==> c != null && c.Valid(U));
+ requires S !! U;
+ requires left == null || right == null;
+ requires child.parent == null;
+ // modifies only one of this.left and this.right, and child.parent, and various sum fields:
+ modifies S, child;
+ ensures child.left == old(child.left) && child.right == old(child.right) && child.val == old(child.val);
+ ensures (forall c :: c in S && c != this ==> c.left == old(c.left) && c.right == old(c.right));
+ ensures old(left) != null ==> left == old(left);
+ ensures old(right) != null ==> right == old(right);
+ ensures (forall c :: c in S ==> c.parent == old(c.parent) && c.val == old(c.val));
+ // sets child.parent to this:
+ ensures child.parent == this;
+ // leaves everything in S+U valid:
+ ensures (forall c :: c in S+U ==> c.Valid(S+U));
+ {
+ if (left == null) {
+ left := child;
+ } else {
+ right := child;
+ }
+ child.parent := this;
+ call Adjust(child.sum, S, S+U);
+ }
+
+ method Dislodge(ghost S: set<Composite>)
+ requires this in S && Acyclic(S);
+ requires (forall c :: c in S ==> c != null && c.Valid(S));
+ modifies S;
+ ensures (forall c :: c in S ==> c.Valid(S));
+ ensures (forall c :: c in S ==> c.val == old(c.val));
+ ensures (forall c :: c in S && c != this ==> c.parent == old(c.parent));
+ ensures (forall c :: c in S ==> c.left == old(c.left) || (old(c.left) == this && c.left == null));
+ ensures (forall c :: c in S ==> c.right == old(c.right) || (old(c.right) == this && c.right == null));
+ ensures Acyclic({this});
+ {
+ var p := parent;
+ parent := null;
+ if (p != null) {
+ assert (p.left == this) != (p.right == this);
+ if (p.left == this) {
+ p.left := null;
+ } else {
+ p.right := null;
+ }
+ var delta := -sum;
+ call p.Adjust(delta, S - {this}, S);
+ }
+ }
+
+ /*private*/ method Adjust(delta: int, ghost U: set<Composite>, ghost S: set<Composite>)
+ requires U <= S && Acyclic(U);
+ // everything else is valid:
+ requires (forall c :: c in S && c != this ==> c != null && c.Valid(S));
+ // this is almost valid:
+ requires parent != null ==> parent in S && (parent.left == this || parent.right == this);
+ requires left != null ==> left in S && left.parent == this && left != right;
+ requires right != null ==> right in S && right.parent == this && left != right;
+ // ... except that sum needs to be adjusted by delta:
+ requires sum + delta == val + (if left == null then 0 else left.sum) + (if right == null then 0 else right.sum);
+ // modifies sum fields in U:
+ modifies U`sum;
+ // everything is valid, including this:
+ ensures (forall c :: c in S ==> c.Valid(S));
+ {
+ var p := this;
+ ghost var T := U;
+ while (p != null)
+ invariant T <= U;
+ invariant p == null || p.Acyclic(T);
+ invariant (forall c :: c in S && c != p ==> c.Valid(S));
+ invariant p != null ==> p.sum + delta == p.val + (if p.left == null then 0 else p.left.sum) + (if p.right == null then 0 else p.right.sum);
+ invariant (forall c :: c in S ==> c.left == old(c.left) && c.right == old(c.right) && c.parent == old(c.parent) && c.val == old(c.val));
+ decreases T;
+ {
+ p.sum := p.sum + delta;
+ T := T - {p};
+ p := p.parent;
+ }
+ }
+}
+
+method Main()
+{
+ var c0 := new Composite;
+ call c0.Init(57);
+
+ var c1 := new Composite;
+ call c1.Init(12);
+ call c0.Add({c0}, c1, {c1});
+
+ var c2 := new Composite;
+ call c2.Init(48);
+
+ var c3 := new Composite;
+ call c3.Init(48);
+ call c2.Add({c2}, c3, {c3});
+ call c0.Add({c0,c1}, c2, {c2,c3});
+
+ ghost var S := {c0, c1, c2, c3};
+ call c1.Update(100, S);
+ call c2.Update(102, S);
+
+ call c2.Dislodge(S);
+ call c2.Update(496, S);
+ call c0.Update(0, S);
+}
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];
+ }
+}
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;
+ }
+ }
+}
diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
new file mode 100644
index 00000000..d6af7b71
--- /dev/null
+++ b/Test/vacid0/runtest.bat
@@ -0,0 +1,12 @@
+@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /compile:0 %* %%f
+)