diff options
Diffstat (limited to 'Test/dafny1')
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/Celebrity.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/UltraFilter.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 2 |
4 files changed, 7 insertions, 3 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 7c7719ee..06cac03b 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -51,6 +51,10 @@ Dafny program verifier finished with 8 verified, 0 errors Dafny program verifier finished with 10 verified, 0 errors
+-------------------- SchorrWaite-stages.dfy --------------------
+
+Dafny program verifier finished with 16 verified, 0 errors
+
-------------------- Cubes.dfy --------------------
Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index 21b895aa..4c761671 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -10,7 +10,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool }
method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
- requires (exists c :: IsCelebrity(c, people));
+ requires exists c :: IsCelebrity(c, people);
ensures r == c;
{
var cc; assume cc == c; // this line essentially converts ghost c to non-ghost cc
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index c8419890..c78d5e81 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -1,6 +1,6 @@ // ultra filter
-class UltraFilter<G> {
+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) &&
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index d098d753..fa7f7c70 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -11,7 +11,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy SeparationLogicList.dfy
ListCopy.dfy ListReverse.dfy ListContents.dfy
MatrixFun.dfy pow2.dfy
- SchorrWaite.dfy
+ SchorrWaite.dfy SchorrWaite-stages.dfy
Cubes.dfy SumOfCubes.dfy FindZero.dfy
TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
Induction.dfy Rippling.dfy MoreInduction.dfy
|