Change the encoding of proof certificates to make the two levels explicit

Restrict what conclusions comethods are allowed to have

1 files changed, 28 insertions, 0 deletions

diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index 431d6bb1..cab0637d 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -104,3 +104,31 @@ module CoPredicateResolutionErrors {
 }

 

 // --------------------------------------------------

+

+module InvalidCoMethodConclusions {

+  codatatype Stream<T> = Cons(head: T, tail: Stream);

+

+  copredicate Positive(s: Stream<int>)

+  {

+    s.head > 0 && Positive(s.tail)

+  }

+

+  comethod BadTheorem(s: Stream)

+    ensures false;  // error: invalid comethod conclusion

+  {

+    BadTheorem(s.tail);

+  }

+

+  comethod CM(s: Stream<int>)

+    ensures true && !false;

+    ensures s.head == 8 ==> Positive(s);

+    ensures s.tail == s;

+    ensures s.head < 100;  // error: invalid comethod conclusion

+    ensures Positive(s) ==> s.tail == s;

+    ensures Positive(s) ==> s.head > 88;  // error: bad RHS of implication

+    ensures !Positive(s) ==> s.tail == s;

+    ensures !(true && !false ==> Positive(s) && !Positive(s));

+    ensures !(false && !true ==> Positive(s) && !Positive(s));  // error: bad LHS of implication

+  {

+  }

+}