From 2fc9a47b200589fae14f698e7546553a0b31aec2 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/VSI-Benchmarks/Answer | 2 +- Test/VSI-Benchmarks/b2.dfy | 74 +++++-------------- Test/VSI-Benchmarks/b3.dfy | 3 - Test/VSI-Benchmarks/b4.dfy | 1 - Test/VSI-Benchmarks/b7.dfy | 1 - Test/VSI-Benchmarks/b8.dfy | 2 - Test/alltests.txt | 1 + Test/dafny0/Answer | 49 ++++++++++++- Test/dafny0/Array.dfy | 156 ++++++++++++++++++++++++++++++++++++++++ Test/dafny0/SmallTests.dfy | 10 +++ Test/dafny0/TypeTests.dfy | 10 +++ Test/dafny0/runtest.bat | 2 +- Test/vacid0/Answer | 12 ++++ Test/vacid0/Composite.dfy | 160 ++++++++++++++++++++++++++++++++++++++++++ Test/vacid0/LazyInitArray.dfy | 105 +++++++++++++++++++++++++++ Test/vacid0/SparseArray.dfy | 120 +++++++++++++++++++++++++++++++ Test/vacid0/runtest.bat | 12 ++++ 17 files changed, 653 insertions(+), 67 deletions(-) create mode 100644 Test/dafny0/Array.dfy 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') diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer index 1efeba04..2a4587f4 100644 --- a/Test/VSI-Benchmarks/Answer +++ b/Test/VSI-Benchmarks/Answer @@ -5,7 +5,7 @@ Dafny program verifier finished with 10 verified, 0 errors -------------------- b2.dfy -------------------- -Dafny program verifier finished with 12 verified, 0 errors +Dafny program verifier finished with 6 verified, 0 errors -------------------- b3.dfy -------------------- diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index ec255ed1..fd20a72b 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -1,27 +1,23 @@ -// Note:Implemented arrays as Dafny does not provide them - class Benchmark2 { - method BinarySearch(a: Array, key: int) returns (result: int) + method BinarySearch(a: array, key: int) returns (result: int) requires a != null; - requires (forall i, j :: - 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j)); - ensures -1 <= result && result < a.Length(); - ensures 0 <= result ==> a.Get(result) == key; - ensures result == -1 ==> - (forall i :: 0 <= i && i < a.Length() ==> a.Get(i) != key); + requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]); + ensures -1 <= result && result < |a|; + ensures 0 <= result ==> a[result] == key; + ensures result == -1 ==> (forall i :: 0 <= i && i < |a| ==> a[i] != key); { var low := 0; - var high := a.Length(); + var high := |a|; while (low < high) - invariant 0 <= low && low <= high && high <= a.Length(); - invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key); - invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i)); + invariant 0 <= low && low <= high && high <= |a|; + invariant (forall i :: 0 <= i && i < low ==> a[i] < key); + invariant (forall i :: high <= i && i < |a| ==> key < a[i]); decreases high - low; { var mid := low + (high - low) / 2; - var midVal := a.Get(mid); + var midVal := a[mid]; if (midVal < key) { low := mid + 1; @@ -36,47 +32,13 @@ class Benchmark2 { } } -class Array { - var contents: seq; - method Init(n: int) - requires 0 <= n; - modifies this; - ensures |contents| == n; - { - var i := 0; - contents := []; - while (i < n) - invariant i <= n && i == |contents|; - decreases n - i; - { - contents := contents + [0]; - i := i + 1; - } - } - function method Length(): int - reads this; - { |contents| } - function method Get(i: int): int - requires 0 <= i && i < |contents|; - reads this; - { contents[i] } - method Set(i: int, x: int) - requires 0 <= i && i < |contents|; - modifies this; - ensures contents == old(contents)[i := x]; - { - contents := contents[i := x]; - } -} - method Main() { - var a := new Array; - call a.Init(5); - call a.Set(0, -4); - call a.Set(1, -2); - call a.Set(2, -2); - call a.Set(3, 0); - call a.Set(4, 25); + var a := new int[5]; + a[0] := -4; + a[1] := -2; + a[2] := -2; + a[3] := 0; + a[4] := 25; call TestSearch(a, 4); call TestSearch(a, -8); call TestSearch(a, -2); @@ -86,9 +48,9 @@ method Main() { call TestSearch(a, 27); } -method TestSearch(a: Array, key: int) +method TestSearch(a: array, key: int) requires a != null; - requires (forall i, j :: 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j)); + requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]); { var b := new Benchmark2; call r := b.BinarySearch(a, key); diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 37b73cba..6d9c3ddd 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -64,7 +64,6 @@ class Benchmark3 { invariant n <= |q.contents|; invariant n == |p|; invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i); - decreases |q.contents| - n; { p := p + [n]; n := n + 1; @@ -121,7 +120,6 @@ class Benchmark3 { invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated invariant 0 <= k && k < |old(q.contents)| && old(q.contents)[k] == m; invariant (forall i ::0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far - decreases n-j; { call x:= q.Dequeue(); call q.Enqueue(x); @@ -134,7 +132,6 @@ class Benchmark3 { while (j < k) invariant j <= k; invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; - decreases k-j; { call x := q.Dequeue(); call q.Enqueue(x); diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index ab1285f6..d2fca9bc 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -95,7 +95,6 @@ class Map { while (j < |keys|) invariant j <= |keys|; invariant key !in keys[..j]; - decreases |keys| -j; { if (keys[j] == key) { idx := j; diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index e5af6357..2304e602 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -142,7 +142,6 @@ class Client { call wr.Create(); while (0 < |q.contents|) invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint; - decreases |q.contents|; { call ch := q.Dequeue(); call wr.PutChar(ch); diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index d8ee2013..34e0cfef 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -104,7 +104,6 @@ class Glossary { invariant q !in wr.footprint; invariant qcon == q.contents; invariant (forall k :: k in q.contents ==> k in glossary.keys); - decreases |definition| -i; { var w := definition[i]; call present, d := glossary.Find(w); @@ -342,7 +341,6 @@ class Map { while (j < |keys|) invariant j <= |keys|; invariant key !in keys[..j]; - decreases |keys| -j; { if (keys[j] == key) { idx := j; diff --git a/Test/alltests.txt b/Test/alltests.txt index 2648581c..6d44550e 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -21,4 +21,5 @@ houdini Postponed Test for Houdini decision procedure dafny0 Use Dafny programs havoc0 Use HAVOC-generated bpl files VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges +vacid0 Use Dafny attempts to VACID Edition 0 benchmarks livevars Use STORM benchmarks for testing correctness of live variable analysis diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 726a6c13..59582de8 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -78,7 +78,8 @@ TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected i TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int) TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed -9 resolution/type errors detected in TypeTests.dfy +TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +10 resolution/type errors detected in TypeTests.dfy -------------------- SmallTests.dfy -------------------- SmallTests.dfy(30,7): Error: RHS expression must be well defined @@ -123,7 +124,7 @@ Execution trace: (0,0): anon4_Else (0,0): anon3 -Dafny program verifier finished with 22 verified, 9 errors +Dafny program verifier finished with 24 verified, 9 errors -------------------- Definedness.dfy -------------------- Definedness.dfy(8,7): Error: possible division by zero @@ -265,6 +266,50 @@ Execution trace: Dafny program verifier finished with 21 verified, 29 errors +-------------------- Array.dfy -------------------- +Array.dfy(10,12): Error: assignment may update an array not in the enclosing method's modifies clause +Execution trace: + (0,0): anon0 + (0,0): anon3_Then +Array.dfy(17,9): Error: RHS expression must be well defined +Execution trace: + (0,0): anon0 +Array.dfy(24,10): Error: LHS expression must be well defined +Execution trace: + (0,0): anon0 +Array.dfy(48,20): Error: assertion violation +Execution trace: + (0,0): anon0 +Array.dfy(56,12): Error: assignment may update an array not in the enclosing method's modifies clause +Execution trace: + (0,0): anon0 + (0,0): anon3_Then +Array.dfy(63,12): Error: assignment may update an array not in the enclosing method's modifies clause +Execution trace: + (0,0): anon0 + (0,0): anon3_Then +Array.dfy(95,18): Error: assertion violation +Execution trace: + (0,0): anon0 +Array.dfy(107,6): Error: insufficient reads clause to read array element +Execution trace: + (0,0): anon0 + (0,0): anon4_Then + (0,0): anon5_Then +Array.dfy(115,6): Error: insufficient reads clause to read array element +Execution trace: + (0,0): anon0 + (0,0): anon4_Then + (0,0): anon5_Then +Array.dfy(131,10): Error: assignment may update an array not in the enclosing method's modifies clause +Execution trace: + (0,0): anon0 +Array.dfy(138,10): Error: assignment may update an array not in the enclosing method's modifies clause +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 22 verified, 11 errors + -------------------- Modules0.dfy -------------------- Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T Modules0.dfy(13,7): Error: module T named among imports does not exist diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy new file mode 100644 index 00000000..928f2bc5 --- /dev/null +++ b/Test/dafny0/Array.dfy @@ -0,0 +1,156 @@ +class A { + method M() { + var y := new A[100]; + y[5] := null; + } + + method N0() { + var a; + if (a != null && 5 < |a|) { + a[5] := 12; // error: violates modifies clause + } + } + + method N1(a: array) + modifies a; + { + var b := |a|; // error: a may be null + } + + method N2(a: array) + requires a != null; + modifies a; + { + a[5] := 12; // error: index may be outside bounds + } + + method N3(a: array) + requires a != null && 5 < |a|; + modifies a; + ensures (forall i :: 0 <= i && i < |a| ==> a[i] == old(a[i]) || (i == 5 && a[i] == 12)); + { + a[5] := 12; // all is good + } + + var zz0: array; + var zz1: array; + method O() { + var zz2 := new A[25]; + assert zz2 != zz0; // holds because zz2 is newly allocated + /****** These would be good things to be able to verify, but the current encoding is not up to the task + var o: object := zz0; + assert this != o; // holds because zz0 has a different type + if (zz0 != null && zz1 != null && 2 <= |zz0| && |zz0| == |zz1|) { + o := zz1[1]; + assert zz0[1] == o ==> o == null; // holds because zz0 and zz1 have different element types + } + ******/ + assert zz2[20] == null; // error: no reason that this must hold + } + + var x: array; + method P0() + modifies this; + { + if (x != null && 100 <= |x|) { + x[5] := 12; // error: violates modifies clause + } + } + method P1() + modifies this`x; + { + if (x != null && 100 <= |x|) { + x[5] := 12; // error: violates modifies clause + } + } + method P2() + modifies x; + { + if (x != null && 100 <= |x|) { + x[5] := 12; // fine + } + } + + method Q() { + var y := new object[100]; + y[5] := null; + y[0..] := null; + y[..83] := null; + y[0..|y|] := null; + } + + method R() { + var y := new int[100]; + y[55] := 80; + y[10..] := 25; + y[..83] := 30; + y[50..60] := 35; + y[55] := 90; + + assert y[54] == 35; + assert y[55] == 90; + assert y[83] == 25; + assert y[8] == 30; + assert y[90] + y[91] + y[0] + 20 == |y|; + assert y[93] == 24; // error (it's 25) + } +} + +class B { } + +// ------------------------------- + +class ArrayTests { + function F0(a: array): bool + { + a != null && 10 <= |a| && + a[7] == 13 // error: reads on something outside reads clause + } + + var b: array; + function F1(): bool + reads this; + { + b != null && 10 <= |b| && + b[7] == 13 // error: reads on something outside reads clause + } + + function F2(a: array): bool + reads this, b, a; + { + a != null && 10 <= |a| && + a[7] == 13 // good + && + b != null && 10 <= |b| && + b[7] == 13 // good + } + + method M0(a: array) + requires a != null && 10 <= |a|; + { + a[7] := 13; // error: updates location not in modifies clause + } + + method M1() + requires b != null && 10 <= |b|; + modifies this; + { + b[7] := 13; // error: updates location not in modifies clause + } + + method M2() + modifies this; + { + var bb := new int[75]; + b := bb; // fine + } + + method M3(a: array) + requires a != null && 10 <= |a|; + requires b != null && 10 <= |b|; + modifies this, b, a; + { + a[7] := 13; // good + b[7] := 13; // good + } +} diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index ba6c8e0c..4e3fab69 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -150,4 +150,14 @@ class Modifies { m.x := m.x + 1; // error: may violate modifies clause } } + + method SetConstruction() { + var s := {1}; + assert s != {}; + if (*) { + assert s != {0,1}; + } else { + assert s != {1,0}; + } + } } diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 1616234e..fe8644be 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -45,3 +45,13 @@ datatype ReverseOrder_TheCounterpart { More(ReverseOrder_MutuallyRecursiveDataType); } +// --------------------- + +class ArrayTests { + ghost method G(a: array) + requires a != null && 10 <= |a|; + modifies a; + { + a[7] := 13; // error: array elements are not ghost locations + } +} diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index fd90e479..c43ea782 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -17,7 +17,7 @@ for %%f in (BQueue.bpl) do ( %BPLEXE% %* %%f ) -for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy +for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy Modules0.dfy Modules1.dfy BadFunction.dfy Queue.dfy ListCopy.dfy BinaryTree.dfy ListReverse.dfy ListContents.dfy SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy 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