Support for copredicates and prefix predicates in comethods.

(Missing from the co support are (prefix) equalities of codatatypes,
various restrictions on the use of co/prefix-predicates, and tactic
support for applying the (prefix-)induction automatically.)

5 files changed, 182 insertions, 12 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 072339b3..97e7c870 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1342,17 +1342,31 @@ CoResolution.dfy(41,9): Error: a call to a prefix predicate/method in this conte
 CoResolution.dfy(42,4): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)

 13 resolution/type errors detected in CoResolution.dfy

 

+-------------------- CoPrefix.dfy --------------------

+CoPrefix.dfy(61,7): Error: failure to decrease termination measure

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+CoPrefix.dfy(74,7): Error: failure to decrease termination measure

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+CoPrefix.dfy(114,1): Error BP5003: A postcondition might not hold on this return path.

+CoPrefix.dfy(113,11): Related location: This is the postcondition that might not hold.

+CoPrefix.dfy(101,17): Related location: Related location

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 17 verified, 3 errors

+

 -------------------- CoinductiveProofs.dfy --------------------

 CoinductiveProofs.dfy(26,12): Error: assertion violation

 CoinductiveProofs.dfy(10,17): Related location: Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-CoinductiveProofs.dfy(33,1): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(32,11): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(10,17): Related location: Related location

-Execution trace:

-    (0,0): anon0

 CoinductiveProofs.dfy(56,1): Error BP5003: A postcondition might not hold on this return path.

 CoinductiveProofs.dfy(55,11): Related location: This is the postcondition that might not hold.

 CoinductiveProofs.dfy(51,3): Related location: Related location

@@ -1380,16 +1394,14 @@ Execution trace:
     (0,0): anon0

 CoinductiveProofs.dfy(147,1): Error BP5003: A postcondition might not hold on this return path.

 CoinductiveProofs.dfy(146,22): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(1,24): Related location: Related location

 Execution trace:

     (0,0): anon0

 CoinductiveProofs.dfy(153,1): Error BP5003: A postcondition might not hold on this return path.

 CoinductiveProofs.dfy(152,22): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(1,24): Related location: Related location

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 31 verified, 9 errors

+Dafny program verifier finished with 32 verified, 8 errors

 

 -------------------- TypeAntecedents.dfy --------------------

 TypeAntecedents.dfy(32,13): Error: assertion violation

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
new file mode 100644
index 00000000..09dd2cc5
--- /dev/null
+++ b/Test/dafny0/CoPrefix.dfy
@@ -0,0 +1,115 @@
+// ----- Stream

+

+codatatype Stream = Nil | Cons(head: int, tail: Stream);

+

+function append(M: Stream, N: Stream): Stream

+{

+  match M

+  case Nil => N

+  case Cons(t, M') => Cons(t, append(M', N))

+}

+

+function zeros(): Stream

+{

+  Cons(0, zeros())

+}

+

+function ones(): Stream

+{

+  Cons(1, ones())

+}

+

+copredicate atmost(a: Stream, b: Stream)

+{

+  match a

+  case Nil => true

+  case Cons(h,t) => b.Cons? && h <= b.head && atmost(t, b.tail)

+}

+

+comethod Theorem0()

+  ensures atmost(zeros(), ones());

+{

+  // the following shows two equivalent ways to getting essentially the

+  // co-inductive hypothesis

+  if (*) {

+    Theorem0#[_k-1]();

+  } else {

+    Theorem0();

+  }

+}

+

+ghost method Theorem0_Manual()

+  ensures atmost(zeros(), ones());

+{

+  parallel (k: nat) {

+    Theorem0_Lemma(k);

+  }

+  assume (forall k: nat :: atmost#[k](zeros(), ones())) ==> atmost(zeros(), ones());

+}

+

+datatype Natural = Zero | Succ(Natural);

+

+comethod Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)

+  ensures atmost(zeros(), ones());

+  decreases y;

+{

+  match (y) {

+    case Succ(x) =>

+      // this is just to show that the decreases clause does kick in

+      Theorem0_TerminationFailure_ExplicitDecreases#[_k](x);

+    case Zero =>

+      Theorem0_TerminationFailure_ExplicitDecreases#[_k](y);  // error: failure to terminate

+  }

+  Theorem0_TerminationFailure_ExplicitDecreases#[_k-1](y);

+}

+

+comethod Theorem0_TerminationFailure_DefaultDecreases(y: Natural)

+  ensures atmost(zeros(), ones());

+{

+  match (y) {

+    case Succ(yy) =>

+      // this is just to show that the decreases clause does kick in

+      Theorem0_TerminationFailure_DefaultDecreases#[_k](yy);

+    case Zero =>

+      Theorem0_TerminationFailure_DefaultDecreases#[_k](y);  // error: failure to terminate

+  }

+  Theorem0_TerminationFailure_DefaultDecreases#[_k-1](y);

+}

+

+ghost method {:induction true} Theorem0_Lemma(k: nat)

+  ensures atmost#[k](zeros(), ones());

+{

+}

+

+/** SOON

+comethod Theorem1()

+  ensures append(zeros(), ones()) == zeros();

+{

+  Theorem1();

+}

+** SOON */

+

+codatatype IList = ICons(head: int, tail: IList);

+

+function UpIList(n: int): IList

+{

+  ICons(n, UpIList(n+1))

+}

+

+copredicate Pos(s: IList)

+{

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

+}

+

+comethod Theorem2(n: int)

+  requires 1 <= n;

+  ensures Pos(UpIList(n));

+{

+  Theorem2(n+1);

+}

+

+comethod Theorem2_NotAProof(n: int)

+  requires 1 <= n;

+  ensures Pos(UpIList(n));

+{  // error: this is not a proof

+}

diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
new file mode 100644
index 00000000..233a818b
--- /dev/null
+++ b/Test/dafny0/CoResolution.dfy
@@ -0,0 +1,43 @@
+copredicate P(b: bool)

+{

+  !b && Q(null)

+}

+

+copredicate Q(a: array<int>)

+{

+  a == null && P(true)

+}

+

+//copredicate A() { B() }

+//predicate B() { A() }  // error: SCC of a copredicate must include only copredicates

+

+copredicate D()

+  reads this;  // error: copredicates are not allowed to have a reads clause -- WHY NOT?

+{

+  true

+}

+

+copredicate S(d: set<int>)

+{

+  this.S#(d) &&  // error: the call to S# must give an explicit depth argument

+  S#(d) &&  // error: the call to S# must give an explicit depth argument

+  this.Undeclared#(d) &&  // error: 'Undeclared#' is undeclared, and depth argument is left implicit

+  this.Undeclared#[5](d) &&  // error: 'Undeclared#' is undeclared

+  Undeclared#(d) &&  // error: 'Undeclared#' is undeclared, and depth argument is left implicit

+  Undeclared#[5](d) &&  // error: 'Undeclared#' is undeclared

+  this.S#[5](d) &&

+  S#[5](d) &&

+  S#(5, d) &&  // error: the '5' here does not give the depth argument

+  S#[_k](d)  // error: _k is not an identifier in scope

+}

+

+comethod CM(d: set<int>)

+{

+  var b;

+  b := this.S#[5](d) && this.S#(d + d);  // error: cannot rely on implicit depth argument here

+  b := S#[5](d) && S#(d + d);  // error: cannot rely on implicit depth argument here

+  this.CM#[5](d);

+  CM#[5](d);

+  this.CM#(d + d);  // error: must give an explicit depth argument

+  CM#(d + d);  // error: must give an explicit depth argument

+}

diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index c56f9b36..ddb23b5b 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -23,18 +23,18 @@ comethod PosLemma1(n: int)
 {

   PosLemma1(n + 1);

   if (*) {

-    assert Pos(Upward(n + 1));  // error: cannot conclude this here, because we only have a certificate

+    assert Pos(Upward(n + 1));  // error: cannot conclude this here, because we only have prefix predicates

   }

 }

 

 comethod Outside_CoMethod_Caller_PosLemma(n: int)

   requires 1 <= n;

   ensures Pos(Upward(n));

-{  // error: this comethod is supposed to produce a certificate, but instead it establishes the real deal

-   // (which currently produces a complaint from Dafny)

+{

   assert Upward(n).tail == Upward(n + 1);  // follows from one unrolling of the definition of Upward

   PosLemma0(n + 1);

   assert Pos(Upward(n+1));  // this follows directly from the previous line, because it isn't a recursive call

+  // ... and it implies the prefix predicate we're supposed to establish

 }

 

 method Outside_Method_Caller_PosLemma(n: int)

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index fd5349f4..82d4bebd 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -18,7 +18,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy

             TypeParameters.dfy Datatypes.dfy

             Coinductive.dfy Corecursion.dfy CoResolution.dfy

-            CoinductiveProofs.dfy

+            CoPrefix.dfy CoinductiveProofs.dfy

             TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy

             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy