diff options
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 8 | ||||
| -rw-r--r-- | Test/dafny0/CoPredicates.dfy | 10 |
2 files changed, 14 insertions, 4 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 6b7a1079..258f67e0 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1290,13 +1290,13 @@ Execution trace: Dafny program verifier finished with 5 verified, 2 errors
-------------------- CoPredicates.dfy --------------------
-CoPredicates.dfy(35,1): Error BP5003: A postcondition might not hold on this return path.
-CoPredicates.dfy(34,11): Related location: This is the postcondition that might not hold.
-CoPredicates.dfy(20,22): Related location: Related location
+CoPredicates.dfy(45,1): Error BP5003: A postcondition might not hold on this return path.
+CoPredicates.dfy(44,11): Related location: This is the postcondition that might not hold.
+CoPredicates.dfy(30,22): Related location: Related location
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 11 verified, 1 error
+Dafny program verifier finished with 14 verified, 1 error
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy index b4da4792..67dff91b 100644 --- a/Test/dafny0/CoPredicates.dfy +++ b/Test/dafny0/CoPredicates.dfy @@ -10,6 +10,16 @@ copredicate Pos(s: Stream<int>) 0 < s.head && Pos(s.tail)
}
+copredicate X(s: Stream)
+{
+ X(s)
+}
+
+ghost method AlwaysLemma(s: Stream)
+ ensures X(s);
+{
+}
+
function Doubles(n: int): Stream<int>
{
Cons(2*n, Doubles(n + 1))
|