diff options
-rw-r--r-- | Source/Provers/Simplify/ProverInterface.ssc | 18 | ||||
-rw-r--r-- | Test/alltests.txt | 3 | ||||
-rw-r--r-- | Test/dafny0/Answer | 52 | ||||
-rw-r--r-- | Test/dafny0/BinaryTree.dfy | 244 | ||||
-rw-r--r-- | Test/dafny0/runtest.bat | 15 | ||||
-rw-r--r-- | Test/dafny1/Answer | 56 | ||||
-rw-r--r-- | Test/dafny1/BQueue.bpl (renamed from Test/dafny0/BQueue.bpl) | 0 | ||||
-rw-r--r-- | Test/dafny1/BinaryTree.dfy | 244 | ||||
-rw-r--r-- | Test/dafny1/Celebrity.dfy (renamed from Test/dafny0/Celebrity.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/ListContents.dfy (renamed from Test/dafny0/ListContents.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/ListCopy.dfy (renamed from Test/dafny0/ListCopy.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/ListReverse.dfy (renamed from Test/dafny0/ListReverse.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/Queue.dfy (renamed from Test/dafny0/Queue.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/SchorrWaite.dfy (renamed from Test/dafny0/SchorrWaite.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/Substitution.dfy (renamed from Test/dafny0/Substitution.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/SumOfCubes.dfy (renamed from Test/dafny0/SumOfCubes.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/TerminationDemos.dfy (renamed from Test/dafny0/TerminationDemos.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/TreeDatatype.dfy (renamed from Test/dafny0/Tree.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/UltraFilter.dfy | 108 | ||||
-rw-r--r-- | Test/dafny1/UnboundedStack.dfy (renamed from Test/dafny0/UnboundedStack.dfy) | 0 | ||||
-rw-r--r-- | Test/dafny1/runtest.bat | 26 |
21 files changed, 454 insertions, 312 deletions
diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc index c885f84e..bd618c24 100644 --- a/Source/Provers/Simplify/ProverInterface.ssc +++ b/Source/Provers/Simplify/ProverInterface.ssc @@ -207,22 +207,34 @@ namespace Microsoft.Boogie.Simplify programFiles = Environment.GetEnvironmentVariable("ProgramW6432");
}
- for (int minorVersion = 7; true; minorVersion--) {
+ List<string!> attempts = new List<string!>();
+ for (int minorVersion = 15; true; minorVersion--) {
if (File.Exists(_proverPath)) {
- return; // all seems good
+ break; // all seems good
}
+ attempts.Add(_proverPath);
if (minorVersion < 0) {
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Failed to find prover. Looked in these places:");
+ foreach (string a in attempts) {
+ Console.WriteLine(" {0}", a);
+ }
+ }
throw new ProverException("Cannot find executable: " + firstTry);
}
_proverPath = Path.Combine(programFiles + @"\Microsoft Research\Z3-2." + minorVersion + @"\bin", proverExe);
if (File.Exists(_proverPath)) {
- return; // all seems good
+ break; // all seems good
}
+ attempts.Add(_proverPath);
if (programFilesX86 != null) {
_proverPath = Path.Combine(programFilesX86 + @"\Microsoft Research\Z3-2." + minorVersion + @"\bin", proverExe);
}
}
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Using prover: " + _proverPath);
+ }
}
}
diff --git a/Test/alltests.txt b/Test/alltests.txt index a8ad52f2..e5f91e61 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -18,7 +18,8 @@ test16 Use Tests methodology of visible-state semantics and loop un test17 Postponed Tests inference of parameterized contracts
z3api Postponed Test for Z3 Managed .NET API prover
houdini Postponed Test for Houdini decision procedure
-dafny0 Use Dafny programs
+dafny0 Use Dafny functionality tests
+dafny1 Use Various Dafny examples
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
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index e1b83c87..0c152d6e 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -64,10 +64,6 @@ class C { Dafny program verifier finished with 0 verified, 0 errors
--------------------- BQueue.bpl --------------------
-
-Boogie program verifier finished with 8 verified, 0 errors
-
-------------------- TypeTests.dfy --------------------
TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
@@ -338,30 +334,6 @@ Execution trace: Dafny program verifier finished with 2 verified, 1 error
--------------------- Queue.dfy --------------------
-
-Dafny program verifier finished with 22 verified, 0 errors
-
--------------------- ListCopy.dfy --------------------
-
-Dafny program verifier finished with 4 verified, 0 errors
-
--------------------- BinaryTree.dfy --------------------
-
-Dafny program verifier finished with 24 verified, 0 errors
-
--------------------- ListReverse.dfy --------------------
-
-Dafny program verifier finished with 2 verified, 0 errors
-
--------------------- ListContents.dfy --------------------
-
-Dafny program verifier finished with 9 verified, 0 errors
-
--------------------- SchorrWaite.dfy --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
-
-------------------- Termination.dfy --------------------
Dafny program verifier finished with 13 verified, 0 errors
@@ -423,27 +395,3 @@ Dafny program verifier finished with 24 verified, 2 errors -------------------- Datatypes.dfy --------------------
Dafny program verifier finished with 10 verified, 0 errors
-
--------------------- UnboundedStack.dfy --------------------
-
-Dafny program verifier finished with 12 verified, 0 errors
-
--------------------- SumOfCubes.dfy --------------------
-
-Dafny program verifier finished with 17 verified, 0 errors
-
--------------------- TerminationDemos.dfy --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
-
--------------------- Substitution.dfy --------------------
-
-Dafny program verifier finished with 12 verified, 0 errors
-
--------------------- Tree.dfy --------------------
-
-Dafny program verifier finished with 6 verified, 0 errors
-
--------------------- Celebrity.dfy --------------------
-
-Dafny program verifier finished with 11 verified, 0 errors
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy deleted file mode 100644 index 8b4892dd..00000000 --- a/Test/dafny0/BinaryTree.dfy +++ /dev/null @@ -1,244 +0,0 @@ -class IntSet {
- ghost var contents: set<int>;
- ghost var footprint: set<object>;
-
- var root: Node;
-
- function Valid(): bool
- reads this, footprint;
- {
- this in footprint &&
- (root == null ==> contents == {}) &&
- (root != null ==>
- root in footprint && root.footprint <= footprint && this !in root.footprint &&
- root.Valid() &&
- contents == root.contents)
- }
-
- method Init()
- modifies this;
- ensures Valid() && fresh(footprint - {this});
- ensures contents == {};
- {
- root := null;
- footprint := {this};
- contents := {};
- }
-
- method Find(x: int) returns (present: bool)
- requires Valid();
- ensures present <==> x in contents;
- {
- if (root == null) {
- present := false;
- } else {
- call present := root.Find(x);
- }
- }
-
- method Insert(x: int)
- requires Valid();
- modifies footprint;
- ensures Valid() && fresh(footprint - old(footprint));
- ensures contents == old(contents) + {x};
- {
- call t := InsertHelper(x, root);
- root := t;
- contents := root.contents;
- footprint := root.footprint + {this};
- }
-
- static method InsertHelper(x: int, n: Node) returns (m: Node)
- requires n == null || n.Valid();
- modifies n.footprint;
- ensures m != null && m.Valid();
- ensures n == null ==> fresh(m.footprint) && m.contents == {x};
- ensures n != null ==> m == n && n.contents == old(n.contents) + {x};
- ensures n != null ==> fresh(n.footprint - old(n.footprint));
- decreases if n == null then {} else n.footprint;
- {
- if (n == null) {
- m := new Node;
- call m.Init(x);
- } else if (x == n.data) {
- m := n;
- } else {
- if (x < n.data) {
- assert n.right == null || n.right.Valid();
- call t := InsertHelper(x, n.left);
- n.left := t;
- n.footprint := n.footprint + n.left.footprint;
- } else {
- assert n.left == null || n.left.Valid();
- call t := InsertHelper(x, n.right);
- n.right := t;
- n.footprint := n.footprint + n.right.footprint;
- }
- n.contents := n.contents + {x};
- m := n;
- }
- }
-
- method Remove(x: int)
- requires Valid();
- modifies footprint;
- ensures Valid() && fresh(footprint - old(footprint));
- ensures contents == old(contents) - {x};
- {
- if (root != null) {
- call newRoot := root.Remove(x);
- root := newRoot;
- if (root == null) {
- contents := {};
- footprint := {this};
- } else {
- contents := root.contents;
- footprint := root.footprint + {this};
- }
- }
- }
-}
-
-class Node {
- ghost var contents: set<int>;
- ghost var footprint: set<object>;
-
- var data: int;
- var left: Node;
- var right: Node;
-
- function Valid(): bool
- reads this, footprint;
- {
- this in footprint &&
- null !in footprint &&
- (left != null ==>
- left in footprint &&
- left.footprint <= footprint && this !in left.footprint &&
- left.Valid() &&
- (forall y :: y in left.contents ==> y < data)) &&
- (right != null ==>
- right in footprint &&
- right.footprint <= footprint && this !in right.footprint &&
- right.Valid() &&
- (forall y :: y in right.contents ==> data < y)) &&
- (left == null && right == null ==>
- contents == {data}) &&
- (left != null && right == null ==>
- contents == left.contents + {data}) &&
- (left == null && right != null ==>
- contents == {data} + right.contents) &&
- (left != null && right != null ==>
- left.footprint !! right.footprint &&
- contents == left.contents + {data} + right.contents)
- }
-
- method Init(x: int)
- modifies this;
- ensures Valid() && fresh(footprint - {this});
- ensures contents == {x};
- {
- data := x;
- left := null;
- right := null;
- contents := {x};
- footprint := {this};
- }
-
- method Find(x: int) returns (present: bool)
- requires Valid();
- ensures present <==> x in contents;
- decreases footprint;
- {
- if (x == data) {
- present := true;
- } else if (left != null && x < data) {
- call present := left.Find(x);
- } else if (right != null && data < x) {
- call present := right.Find(x);
- } else {
- present := false;
- }
- }
-
- method Remove(x: int) returns (node: Node)
- requires Valid();
- modifies footprint;
- ensures fresh(footprint - old(footprint));
- ensures node != null ==> node.Valid();
- ensures node == null ==> old(contents) <= {x};
- ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {x};
- decreases footprint;
- {
- node := this;
- if (left != null && x < data) {
- call t := left.Remove(x);
- left := t;
- contents := contents - {x};
- if (left != null) { footprint := footprint + left.footprint; }
- } else if (right != null && data < x) {
- call t := right.Remove(x);
- right := t;
- contents := contents - {x};
- if (right != null) { footprint := footprint + right.footprint; }
- } else if (x == data) {
- if (left == null && right == null) {
- node := null;
- } else if (left == null) {
- node := right;
- } else if (right == null) {
- node := left;
- } else {
- // rotate
- call min, r := right.RemoveMin();
- data := min; right := r;
- contents := contents - {x};
- if (right != null) { footprint := footprint + right.footprint; }
- }
- }
- }
-
- method RemoveMin() returns (min: int, node: Node)
- requires Valid();
- modifies footprint;
- ensures fresh(footprint - old(footprint));
- ensures node != null ==> node.Valid();
- ensures node == null ==> old(contents) == {min};
- ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {min};
- ensures min in old(contents) && (forall x :: x in old(contents) ==> min <= x);
- decreases footprint;
- {
- if (left == null) {
- min := data;
- node := right;
- } else {
- call min, t := left.RemoveMin();
- left := t;
- node := this;
- contents := contents - {min};
- if (left != null) { footprint := footprint + left.footprint; }
- }
- }
-}
-
-class Main {
- method Client0(x: int)
- {
- var s := new IntSet;
- call s.Init();
-
- call s.Insert(12);
- call s.Insert(24);
- call present := s.Find(x);
- assert present <==> x == 12 || x == 24;
- }
-
- method Client1(s: IntSet, x: int)
- requires s != null && s.Valid();
- modifies s.footprint;
- {
- call s.Insert(x);
- call s.Insert(24);
- assert old(s.contents) - {x,24} == s.contents - {x,24};
- }
-}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index eb7ea4f7..aa45ca05 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -11,19 +11,10 @@ for %%f in (Simple.dfy) do ( %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f
)
-for %%f in (BQueue.bpl) do (
- echo.
- echo -------------------- %%f --------------------
- %BPLEXE% %* %%f
-)
-
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
- TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy
- SumOfCubes.dfy TerminationDemos.dfy Substitution.dfy
- Tree.dfy Celebrity.dfy) do (
+ Modules0.dfy Modules1.dfy BadFunction.dfy
+ Termination.dfy Use.dfy DTypes.dfy
+ TypeParameters.dfy Datatypes.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 %* %%f
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer new file mode 100644 index 00000000..cf593abf --- /dev/null +++ b/Test/dafny1/Answer @@ -0,0 +1,56 @@ +
+-------------------- BQueue.bpl --------------------
+
+Boogie program verifier finished with 8 verified, 0 errors
+
+-------------------- Queue.dfy --------------------
+
+Dafny program verifier finished with 22 verified, 0 errors
+
+-------------------- BinaryTree.dfy --------------------
+
+Dafny program verifier finished with 24 verified, 0 errors
+
+-------------------- UnboundedStack.dfy --------------------
+
+Dafny program verifier finished with 12 verified, 0 errors
+
+-------------------- ListCopy.dfy --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+
+-------------------- ListReverse.dfy --------------------
+
+Dafny program verifier finished with 2 verified, 0 errors
+
+-------------------- ListContents.dfy --------------------
+
+Dafny program verifier finished with 9 verified, 0 errors
+
+-------------------- SchorrWaite.dfy --------------------
+
+Dafny program verifier finished with 10 verified, 0 errors
+
+-------------------- SumOfCubes.dfy --------------------
+
+Dafny program verifier finished with 17 verified, 0 errors
+
+-------------------- TerminationDemos.dfy --------------------
+
+Dafny program verifier finished with 10 verified, 0 errors
+
+-------------------- Substitution.dfy --------------------
+
+Dafny program verifier finished with 12 verified, 0 errors
+
+-------------------- TreeDatatype.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
+
+-------------------- Celebrity.dfy --------------------
+
+Dafny program verifier finished with 11 verified, 0 errors
+
+-------------------- UltraFilter.dfy --------------------
+
+Dafny program verifier finished with 19 verified, 0 errors
diff --git a/Test/dafny0/BQueue.bpl b/Test/dafny1/BQueue.bpl index 77f1efb3..77f1efb3 100644 --- a/Test/dafny0/BQueue.bpl +++ b/Test/dafny1/BQueue.bpl diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy new file mode 100644 index 00000000..fbda3ecb --- /dev/null +++ b/Test/dafny1/BinaryTree.dfy @@ -0,0 +1,244 @@ +class IntSet {
+ ghost var Contents: set<int>;
+ ghost var Repr: set<object>;
+
+ var root: Node;
+
+ function Valid(): bool
+ reads this, Repr;
+ {
+ this in Repr &&
+ (root == null ==> Contents == {}) &&
+ (root != null ==>
+ root in Repr && root.Repr <= Repr && this !in root.Repr &&
+ root.Valid() &&
+ Contents == root.Contents)
+ }
+
+ method Init()
+ modifies this;
+ ensures Valid() && fresh(Repr - {this});
+ ensures Contents == {};
+ {
+ root := null;
+ Repr := {this};
+ Contents := {};
+ }
+
+ method Find(x: int) returns (present: bool)
+ requires Valid();
+ ensures present <==> x in Contents;
+ {
+ if (root == null) {
+ present := false;
+ } else {
+ call present := root.Find(x);
+ }
+ }
+
+ method Insert(x: int)
+ requires Valid();
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures Contents == old(Contents) + {x};
+ {
+ call t := InsertHelper(x, root);
+ root := t;
+ Contents := root.Contents;
+ Repr := root.Repr + {this};
+ }
+
+ static method InsertHelper(x: int, n: Node) returns (m: Node)
+ requires n == null || n.Valid();
+ modifies n.Repr;
+ ensures m != null && m.Valid();
+ ensures n == null ==> fresh(m.Repr) && m.Contents == {x};
+ ensures n != null ==> m == n && n.Contents == old(n.Contents) + {x};
+ ensures n != null ==> fresh(n.Repr - old(n.Repr));
+ decreases if n == null then {} else n.Repr;
+ {
+ if (n == null) {
+ m := new Node;
+ call m.Init(x);
+ } else if (x == n.data) {
+ m := n;
+ } else {
+ if (x < n.data) {
+ assert n.right == null || n.right.Valid();
+ call t := InsertHelper(x, n.left);
+ n.left := t;
+ n.Repr := n.Repr + n.left.Repr;
+ } else {
+ assert n.left == null || n.left.Valid();
+ call t := InsertHelper(x, n.right);
+ n.right := t;
+ n.Repr := n.Repr + n.right.Repr;
+ }
+ n.Contents := n.Contents + {x};
+ m := n;
+ }
+ }
+
+ method Remove(x: int)
+ requires Valid();
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures Contents == old(Contents) - {x};
+ {
+ if (root != null) {
+ call newRoot := root.Remove(x);
+ root := newRoot;
+ if (root == null) {
+ Contents := {};
+ Repr := {this};
+ } else {
+ Contents := root.Contents;
+ Repr := root.Repr + {this};
+ }
+ }
+ }
+}
+
+class Node {
+ ghost var Contents: set<int>;
+ ghost var Repr: set<object>;
+
+ var data: int;
+ var left: Node;
+ var right: Node;
+
+ function Valid(): bool
+ reads this, Repr;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (left != null ==>
+ left in Repr &&
+ left.Repr <= Repr && this !in left.Repr &&
+ left.Valid() &&
+ (forall y :: y in left.Contents ==> y < data)) &&
+ (right != null ==>
+ right in Repr &&
+ right.Repr <= Repr && this !in right.Repr &&
+ right.Valid() &&
+ (forall y :: y in right.Contents ==> data < y)) &&
+ (left == null && right == null ==>
+ Contents == {data}) &&
+ (left != null && right == null ==>
+ Contents == left.Contents + {data}) &&
+ (left == null && right != null ==>
+ Contents == {data} + right.Contents) &&
+ (left != null && right != null ==>
+ left.Repr !! right.Repr &&
+ Contents == left.Contents + {data} + right.Contents)
+ }
+
+ method Init(x: int)
+ modifies this;
+ ensures Valid() && fresh(Repr - {this});
+ ensures Contents == {x};
+ {
+ data := x;
+ left := null;
+ right := null;
+ Contents := {x};
+ Repr := {this};
+ }
+
+ method Find(x: int) returns (present: bool)
+ requires Valid();
+ ensures present <==> x in Contents;
+ decreases Repr;
+ {
+ if (x == data) {
+ present := true;
+ } else if (left != null && x < data) {
+ call present := left.Find(x);
+ } else if (right != null && data < x) {
+ call present := right.Find(x);
+ } else {
+ present := false;
+ }
+ }
+
+ method Remove(x: int) returns (node: Node)
+ requires Valid();
+ modifies Repr;
+ ensures fresh(Repr - old(Repr));
+ ensures node != null ==> node.Valid();
+ ensures node == null ==> old(Contents) <= {x};
+ ensures node != null ==> node.Repr <= Repr && node.Contents == old(Contents) - {x};
+ decreases Repr;
+ {
+ node := this;
+ if (left != null && x < data) {
+ call t := left.Remove(x);
+ left := t;
+ Contents := Contents - {x};
+ if (left != null) { Repr := Repr + left.Repr; }
+ } else if (right != null && data < x) {
+ call t := right.Remove(x);
+ right := t;
+ Contents := Contents - {x};
+ if (right != null) { Repr := Repr + right.Repr; }
+ } else if (x == data) {
+ if (left == null && right == null) {
+ node := null;
+ } else if (left == null) {
+ node := right;
+ } else if (right == null) {
+ node := left;
+ } else {
+ // rotate
+ call min, r := right.RemoveMin();
+ data := min; right := r;
+ Contents := Contents - {x};
+ if (right != null) { Repr := Repr + right.Repr; }
+ }
+ }
+ }
+
+ method RemoveMin() returns (min: int, node: Node)
+ requires Valid();
+ modifies Repr;
+ ensures fresh(Repr - old(Repr));
+ ensures node != null ==> node.Valid();
+ ensures node == null ==> old(Contents) == {min};
+ ensures node != null ==> node.Repr <= Repr && node.Contents == old(Contents) - {min};
+ ensures min in old(Contents) && (forall x :: x in old(Contents) ==> min <= x);
+ decreases Repr;
+ {
+ if (left == null) {
+ min := data;
+ node := right;
+ } else {
+ call min, t := left.RemoveMin();
+ left := t;
+ node := this;
+ Contents := Contents - {min};
+ if (left != null) { Repr := Repr + left.Repr; }
+ }
+ }
+}
+
+class Main {
+ method Client0(x: int)
+ {
+ var s := new IntSet;
+ call s.Init();
+
+ call s.Insert(12);
+ call s.Insert(24);
+ call present := s.Find(x);
+ assert present <==> x == 12 || x == 24;
+ }
+
+ method Client1(s: IntSet, x: int)
+ requires s != null && s.Valid();
+ modifies s.Repr;
+ {
+ call s.Insert(x);
+ call s.Insert(24);
+ assert old(s.Contents) - {x,24} == s.Contents - {x,24};
+ }
+}
diff --git a/Test/dafny0/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index fd267c71..fd267c71 100644 --- a/Test/dafny0/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny1/ListContents.dfy index 62636ce5..62636ce5 100644 --- a/Test/dafny0/ListContents.dfy +++ b/Test/dafny1/ListContents.dfy diff --git a/Test/dafny0/ListCopy.dfy b/Test/dafny1/ListCopy.dfy index 52f5cf76..52f5cf76 100644 --- a/Test/dafny0/ListCopy.dfy +++ b/Test/dafny1/ListCopy.dfy diff --git a/Test/dafny0/ListReverse.dfy b/Test/dafny1/ListReverse.dfy index ef029b88..ef029b88 100644 --- a/Test/dafny0/ListReverse.dfy +++ b/Test/dafny1/ListReverse.dfy diff --git a/Test/dafny0/Queue.dfy b/Test/dafny1/Queue.dfy index 42b7dd64..42b7dd64 100644 --- a/Test/dafny0/Queue.dfy +++ b/Test/dafny1/Queue.dfy diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index a46e83a3..a46e83a3 100644 --- a/Test/dafny0/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy diff --git a/Test/dafny0/Substitution.dfy b/Test/dafny1/Substitution.dfy index 72415fea..72415fea 100644 --- a/Test/dafny0/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy index b4fab490..b4fab490 100644 --- a/Test/dafny0/SumOfCubes.dfy +++ b/Test/dafny1/SumOfCubes.dfy diff --git a/Test/dafny0/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy index 6b63bfec..6b63bfec 100644 --- a/Test/dafny0/TerminationDemos.dfy +++ b/Test/dafny1/TerminationDemos.dfy diff --git a/Test/dafny0/Tree.dfy b/Test/dafny1/TreeDatatype.dfy index 58124171..58124171 100644 --- a/Test/dafny0/Tree.dfy +++ b/Test/dafny1/TreeDatatype.dfy diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy new file mode 100644 index 00000000..61e86836 --- /dev/null +++ b/Test/dafny1/UltraFilter.dfy @@ -0,0 +1,108 @@ +// ultra filter
+
+class UltraFilter<G> {
+ static function IsFilter(f: set<set<G>>, S: set<G>): bool
+ {
+ (forall A, B :: A in f && A <= B ==> B in f) &&
+ (forall C, D :: C in f && D in f ==> C * D in f) &&
+ S in f &&
+ {} !in f
+ }
+
+ static function IsUltraFilter(f: set<set<G>>, S: set<G>): bool
+ {
+ IsFilter(f, S) &&
+ (forall g :: IsFilter(g, S) && f <= g ==> f == g)
+ }
+
+ method Theorem(f: set<set<G>>, S: set<G>, M: set<G>, N: set<G>)
+ requires IsUltraFilter(f, S);
+ requires M + N in f;
+ ensures M in f || N in f;
+ {
+ if (M !in f) {
+ // instantiate 'g' with the following 'h'
+ call h := H(f, S, M);
+ call Lemma_HIsFilter(h, f, S, M);
+ call Lemma_FHOrdering0(h, f, S, M);
+ }
+ }
+
+ // Dafny currently does not have a set comprehension expression, so this method stub will have to do
+ method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>);
+ ensures (forall X :: X in h <==> M + X in f);
+
+ method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ requires M !in f;
+ ensures IsFilter(h, S);
+ {
+ // call Lemma_H0(h, f, S, M, *, *);
+ assume (forall A, B :: A in h && A <= B ==> B in h);
+
+ // call Lemma_H1(h, f, S, M, *, *);
+ assume (forall C, D :: C in h && D in h ==> C * D in h);
+
+ call Lemma_H2(h, f, S, M);
+
+ call Lemma_H3(h, f, S, M);
+ }
+
+ method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ requires A in h && A <= B;
+ ensures B in h;
+ {
+ assert M + A <= M + B;
+ }
+
+ method Lemma_H1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, C: set<G>, D: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ requires C in h && D in h;
+ ensures C * D in h;
+ {
+ assert (M + C) * (M + D) == M + (C * D);
+ }
+
+ method Lemma_H2(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ ensures S in h;
+ {
+ // S is intended to stand for the universal set, but this is the only place where that plays a role
+ assume M <= S;
+
+ assert M + S == S;
+ }
+
+ method Lemma_H3(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ requires M !in f;
+ ensures {} !in h;
+ {
+ assert M + {} == M;
+ }
+
+ method Lemma_FHOrdering0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ requires IsFilter(h, S);
+ ensures f <= h;
+ {
+ // call Lemma_FHOrdering1(h, f, S, M, *);
+ assume (forall Y :: Y in f ==> Y in h);
+ assume f <= h; // hickup in boxing
+ }
+
+ method Lemma_FHOrdering1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, Y: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ ensures Y in f ==> Y in h;
+ {
+ assert Y <= M + Y;
+ }
+}
diff --git a/Test/dafny0/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy index 4c3b095a..4c3b095a 100644 --- a/Test/dafny0/UnboundedStack.dfy +++ b/Test/dafny1/UnboundedStack.dfy diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat new file mode 100644 index 00000000..aab76ff9 --- /dev/null +++ b/Test/dafny1/runtest.bat @@ -0,0 +1,26 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (BQueue.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BPLEXE% %* %%f
+)
+
+for %%f in (Queue.dfy
+ BinaryTree.dfy
+ UnboundedStack.dfy
+ ListCopy.dfy ListReverse.dfy ListContents.dfy
+ SchorrWaite.dfy
+ SumOfCubes.dfy
+ TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy
+ Celebrity.dfy
+ UltraFilter.dfy) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /compile:0 %* %%f
+)
|