diff options
| author |  Rustan Leino <leino@microsoft.com> | 2013-01-20 15:36:14 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2013-01-20 15:36:14 -0800 |
| commit | 65de14b01e968fadbb011e28c25b7ea80c823639 (patch) | |
| tree | a7567a055f6c95b8c9b8719910729e6b1e175e7f /Test/dafny3 | |
| parent | 724cd08bb69546967483e13fdd1a7c7b9797f59b (diff) | |
More automatic co-induction for comethods
Diffstat (limited to 'Test/dafny3')
| -rw-r--r-- | Test/dafny3/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny3/SimpleCoinduction.dfy | 12 |
2 files changed, 11 insertions, 3 deletions
diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer index c4e75986..418ca164 100644 --- a/Test/dafny3/Answer +++ b/Test/dafny3/Answer @@ -17,7 +17,7 @@ Dafny program verifier finished with 47 verified, 0 errors -------------------- SimpleCoinduction.dfy --------------------
-Dafny program verifier finished with 28 verified, 0 errors
+Dafny program verifier finished with 31 verified, 0 errors
-------------------- CalcExample.dfy --------------------
diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy index 5a8ab288..cc92a6f1 100644 --- a/Test/dafny3/SimpleCoinduction.dfy +++ b/Test/dafny3/SimpleCoinduction.dfy @@ -64,7 +64,6 @@ copredicate True(s: Stream) comethod AlwaysTrue(s: Stream)
ensures True(s);
{
- AlwaysTrue(s.tail); // WHY does this not happen automatically? (Because 's' is not quantified over)
}
copredicate AlsoTrue(s: Stream)
@@ -75,7 +74,16 @@ copredicate AlsoTrue(s: Stream) comethod AlsoAlwaysTrue(s: Stream)
ensures AlsoTrue(s);
{
- // AlsoAlwaysTrue(s); // here, the recursive call is not needed, because it uses the same 's', so 's' does not need to be quantified over
+}
+
+copredicate TT(y: int)
+{
+ TT(y+1)
+}
+
+comethod AlwaysTT(y: int)
+ ensures TT(y);
+{
}
// -----------------------------------------------------------------------
|