diff options
| author |  Jason Koenig <unknown> | 2012-06-27 18:33:13 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-06-27 18:33:13 -0700 |
| commit | 4cf0bf6e03980c121d308727284a4ab8be3e362f (patch) | |
| tree | d23e027243adef3d85bf1e96fc449c9e6a9ab45f /Test/dafny1 | |
| parent | 9ef369da500431d5bc742c2d5dcf3fbaa16246dd (diff) | |
| parent | 25c81e8393f0f9d643c223cd3e7f6a734ec65ff5 (diff) | |
Dafny: Merge
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
|