diff options
| author |  Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 14:56:35 -0700 |
|---|---|---|
| committer | Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 14:56:35 -0700 |
| commit | 33be652b4db584a8441f7b1006ceed73eb091be6 (patch) | |
| tree | 6050f3143e35fed1b1053e9c9044a516a539d5da /Test/dafny1 | |
| parent | 2e43fe69d087fb75213f67f735a3e85e0278a29f (diff) | |
Dafny: fixed regression tests
Diffstat (limited to 'Test/dafny1')
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/ListContents.dfy | 7 | ||||
| -rw-r--r-- | Test/dafny1/Rippling.dfy | 8 |
3 files changed, 15 insertions, 4 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 023d80df..9ed6d75a 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -115,6 +115,10 @@ Dafny program verifier finished with 15 verified, 4 errors Dafny program verifier finished with 10 verified, 0 errors
+-------------------- BDD.dfy --------------------
+
+Dafny program verifier finished with 5 verified, 0 errors
+
-------------------- UltraFilter.dfy --------------------
Dafny program verifier finished with 19 verified, 0 errors
diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy index 069ffbde..594be748 100644 --- a/Test/dafny1/ListContents.dfy +++ b/Test/dafny1/ListContents.dfy @@ -86,6 +86,13 @@ class Node<T> { reverse := current;
current := nx;
+ // This makes the verification go faster.
+ assert current != null ==>
+ current.Valid() &&
+ current in old(footprint) && current.footprint <= old(footprint) &&
+ current.footprint !! reverse.footprint &&
+ |old(list)| == |reverse.list| + |current.list| &&
+ (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);
}
}
}
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 8bed7545..835c3043 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -157,11 +157,11 @@ function last(xs: List): Nat case Cons(z, zs) => last(ys)
}
-function map(f: FunctionValue, xs: List): List
+function apply(f: FunctionValue, xs: List): List
{
match xs
case Nil => Nil
- case Cons(y, ys) => Cons(Apply(f, y), map(f, ys))
+ case Cons(y, ys) => Cons(Apply(f, y), apply(f, ys))
}
// In the following two functions, parameter "p" stands for a predicate: applying p and
@@ -355,7 +355,7 @@ ghost method P11() }
ghost method P12()
- ensures forall n, xs, f :: drop(n, map(f, xs)) == map(f, drop(n, xs));
+ ensures forall n, xs, f :: drop(n, apply(f, xs)) == apply(f, drop(n, xs));
{
}
@@ -506,7 +506,7 @@ ghost method P40() }
ghost method P41()
- ensures forall n, xs, f :: take(n, map(f, xs)) == map(f, take(n, xs));
+ ensures forall n, xs, f :: take(n, apply(f, xs)) == apply(f, take(n, xs));
{
}
|