From 572b11dddba3bfbdc4e90beb4d7f2e076878f717 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 21 May 2010 18:38:47 +0000 Subject: 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 --- Test/vacid0/Answer | 12 ++++ Test/vacid0/Composite.dfy | 160 ++++++++++++++++++++++++++++++++++++++++++ Test/vacid0/LazyInitArray.dfy | 105 +++++++++++++++++++++++++++ Test/vacid0/SparseArray.dfy | 120 +++++++++++++++++++++++++++++++ Test/vacid0/runtest.bat | 12 ++++ 5 files changed, 409 insertions(+) create mode 100644 Test/vacid0/Answer create mode 100644 Test/vacid0/Composite.dfy create mode 100644 Test/vacid0/LazyInitArray.dfy create mode 100644 Test/vacid0/SparseArray.dfy create mode 100644 Test/vacid0/runtest.bat (limited to 'Test/vacid0') 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): 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): 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) + 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, child: Composite, ghost U: set) + 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) + 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, ghost S: set) + 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 { + ghost var Contents: seq; + var Zero: T; + /*private*/ var a: array; + /*private*/ var b: array; + /*private*/ var c: array; + /*private*/ var n: int; + /*private*/ ghost var d: seq; + /*private*/ ghost var e: seq; + 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 { + ghost var Contents: seq; + var zero: T; + /*private*/ var a: seq; // should really be an array + /*private*/ var b: seq; // should really be an array + /*private*/ var c: seq; // should really be an array + /*private*/ var n: int; + /*private*/ ghost var d: seq; // would be better as an array + /*private*/ ghost var e: seq; // 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(n: int) returns (arr: seq) + 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 +) -- cgit v1.2.3