Fixed the problem with the previous check-in.

6 files changed, 96 insertions, 66 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index bb7cbe23..fa72c6e4 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -596,9 +596,12 @@ namespace Microsoft.Dafny
   /// </summary>

   class CoMethodBodyCloner : Cloner

   {

+    readonly CoMethod context;

     readonly Expression k;

-    public CoMethodBodyCloner(Expression k) {

+    public CoMethodBodyCloner(CoMethod context, Expression k) {

+      Contract.Requires(context != null);

       Contract.Requires(k != null);

+      this.context = context;

       this.k = k;

     }

     public override Statement CloneStmt(Statement stmt) {

@@ -613,19 +616,26 @@ namespace Microsoft.Dafny
         }

       } else if (stmt is CallStmt) {

         var s = (CallStmt)stmt;

-        var lhs = s.Lhs.ConvertAll(CloneExpr);

-        var receiver = CloneExpr(s.Receiver);

-        var args = new List<Expression>();

-        args.Add(k);

-        foreach (var arg in s.Args) {

-          args.Add(CloneExpr(arg));

+        if (s.Method is CoMethod) {

+          var moduleCaller = context.EnclosingClass.Module;

+          var moduleCallee = s.Method.EnclosingClass.Module;

+          if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) {

+            // we're looking at a recursive call to a comethod

+            var lhs = s.Lhs.ConvertAll(CloneExpr);

+            var receiver = CloneExpr(s.Receiver);

+            var args = new List<Expression>();

+            args.Add(k);

+            foreach (var arg in s.Args) {

+              args.Add(CloneExpr(arg));

+            }

+            var r = new CallStmt(Tok(s.Tok), lhs, receiver, s.MethodName + "#", args);

+

+            // don't forget to add labels to the cloned statement

+            AddStmtLabels(r, stmt.Labels);

+            r.Attributes = CloneAttributes(stmt.Attributes);

+            return r;

+          }

         }

-        var r = new CallStmt(Tok(s.Tok), lhs, receiver, s.MethodName + "#", args);

-

-        // don't forget to add labels to the cloned statement

-        AddStmtLabels(r, stmt.Labels);

-        r.Attributes = CloneAttributes(stmt.Attributes);

-        return r;

       }

       return base.CloneStmt(stmt);

     }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6c9e136e..a3749372 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -666,10 +666,6 @@ namespace Microsoft.Dafny
                   var com = (CoMethod)m;

                   // _k has already been added to 'formals', so append the original formals

                   formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal));

-                  // prepend "free requires 0 < _k;", since the postcondition of a comethod holds trivially if _k is 0

-                  var req = new List<MaybeFreeExpression>();

-                  req.Add(new MaybeFreeExpression(new BinaryExpr(k.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(k.tok, 0), new IdentifierExpr(k.tok, k.Name)), true));

-                  req.AddRange(com.Req.ConvertAll(cloner.CloneMayBeFreeExpr));

                   // prepend _k to the given decreases clause

                   var decr = new List<Expression>();

                   decr.Add(new IdentifierExpr(com.tok, k.Name));

@@ -677,10 +673,11 @@ namespace Microsoft.Dafny
                   // Create prefix method.  Note that the body is not cloned, but simply shared.

                   com.PrefixMethod = new PrefixMethod(com.tok, extraName, com.IsStatic,

                     com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal),

-                    req, cloner.CloneSpecFrameExpr(com.Mod), new List<MaybeFreeExpression>(),  // Note, the postconditions are filled in after the comethod's postconditions have been resolved

+                    com.Req.ConvertAll(cloner.CloneMayBeFreeExpr), cloner.CloneSpecFrameExpr(com.Mod),

+                    new List<MaybeFreeExpression>(),  // Note, the postconditions are filled in after the comethod's postconditions have been resolved

                     new Specification<Expression>(decr, null),

                     null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the comethod is known

-                    null, com);

+                    cloner.CloneAttributes(com.Attributes), com);

                   extraMember = com.PrefixMethod;

                   // In the call graph, add an edge from M# to M, since this will have the desired effect of detecting unwanted cycles.

                   moduleDef.CallGraph.AddEdge(com.PrefixMethod, com);

@@ -1183,8 +1180,11 @@ namespace Microsoft.Dafny
           // Compute the statement body of the prefix method

           if (com.Body != null) {

             var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1));

-            var subst = new CoMethodBodyCloner(kMinusOne);

-            prefixMethod.Body = subst.CloneBlockStmt(com.Body);

+            var subst = new CoMethodBodyCloner(com, kMinusOne);

+            var mainBody = subst.CloneBlockStmt(com.Body);

+            var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name));

+            var condBody = new IfStmt(com.BodyStartTok, kPositive, mainBody, null);

+            prefixMethod.Body = new BlockStmt(com.tok, new List<Statement>() { condBody });

           }

           // The prefix method now has all its components, so it's finally time we resolve it

           currentClass = (ClassDecl)prefixMethod.EnclosingClass;

@@ -2673,9 +2673,6 @@ namespace Microsoft.Dafny
         scope.Push(p.Name, p);

       }

 

-      // attributes are allowed to mention both in- and out-parameters

-      ResolveAttributes(m.Attributes, false);

-

       // ... continue resolving specification

       foreach (MaybeFreeExpression e in m.Ens) {

         ResolveExpression(e.E, true);

@@ -2697,6 +2694,9 @@ namespace Microsoft.Dafny
         ResolveBlockStatement(m.Body, m.IsGhost, codeContext);

       }

 

+      // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for comethods)

+      ResolveAttributes(m.Attributes, false);

+

       scope.PopMarker();  // for the out-parameters and outermost-level locals

       scope.PopMarker();  // for the in-parameters

     }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index a8e2ba1c..760e6880 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1310,11 +1310,7 @@ Coinductive.dfy(90,8): Error: a recursive copredicate call can only be done in p
 Coinductive.dfy(91,8): Error: a recursive copredicate call can only be done in positive positions

 Coinductive.dfy(92,8): Error: a recursive copredicate call can only be done in positive positions and cannot sit inside an existential quantifier

 Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in positive positions and cannot sit inside an existential quantifier

-Coinductive.dfy(117,12): Error: only copredicates and equalities of codatatypes are allowed as conclusions of comethods

-Coinductive.dfy(126,19): Error: only copredicates and equalities of codatatypes are allowed as conclusions of comethods

-Coinductive.dfy(128,35): Error: only copredicates and equalities of codatatypes are allowed as conclusions of comethods

-Coinductive.dfy(131,14): Error: only copredicates and equalities of codatatypes are allowed as conclusions of comethods

-12 resolution/type errors detected in Coinductive.dfy

+8 resolution/type errors detected in Coinductive.dfy

 

 -------------------- Corecursion.dfy --------------------

 Corecursion.dfy(15,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can called co-recursively)

@@ -1343,68 +1339,86 @@ CoResolution.dfy(92,4): Error: a recursive call from a comethod can go only to o
 CoPrefix.dfy(60,7): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon7_Then

+    (0,0): anon8_Else

+    (0,0): anon9_Then

 CoPrefix.dfy(73,7): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon7_Then

+    (0,0): anon8_Else

+    (0,0): anon9_Then

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

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

 CoPrefix.dfy(98,17): Related location: Related location

 Execution trace:

     (0,0): anon0

+    (0,0): anon3_Then

 CoPrefix.dfy(135,25): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Then

+    (0,0): anon9_Then

+    (0,0): anon10_Then

 CoPrefix.dfy(139,25): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon9_Then

+    (0,0): anon12_Then

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

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

 

-Dafny program verifier finished with 23 verified, 5 errors

+Dafny program verifier finished with 24 verified, 6 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

+    (0,0): anon5_Then

+    (0,0): anon6_Then

 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

 Execution trace:

     (0,0): anon0

+    (0,0): anon3_Then

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

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Then

+    (0,0): anon5_Then

+    (0,0): anon6_Then

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

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

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

 Execution trace:

     (0,0): anon0

+    (0,0): anon3_Then

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

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Then

+    (0,0): anon5_Then

+    (0,0): anon6_Then

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

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

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

 Execution trace:

     (0,0): anon0

+    (0,0): anon3_Then

 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.

 Execution trace:

     (0,0): anon0

+    (0,0): anon3_Then

 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.

 Execution trace:

     (0,0): anon0

+    (0,0): anon3_Then

 

 Dafny program verifier finished with 35 verified, 8 errors

 

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
index 8cbe5394..991e160f 100644
--- a/Test/dafny0/CoPrefix.dfy
+++ b/Test/dafny0/CoPrefix.dfy
@@ -26,7 +26,7 @@ copredicate atmost(a: Stream, b: Stream)
   case Cons(h,t) => b.Cons? && h <= b.head && atmost(t, b.tail)

 }

 

-comethod Theorem0()

+comethod {:induction false} Theorem0()

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

 {

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

@@ -48,7 +48,7 @@ ghost method Theorem0_Manual()
 

 datatype Natural = Zero | Succ(Natural);

 

-comethod Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)

+comethod {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)

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

   decreases y;

 {

@@ -62,7 +62,7 @@ comethod Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)
   Theorem0_TerminationFailure_ExplicitDecreases#[_k-1](y);

 }

 

-comethod Theorem0_TerminationFailure_DefaultDecreases(y: Natural)

+comethod {:induction false} Theorem0_TerminationFailure_DefaultDecreases(y: Natural)

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

 {

   match (y) {

@@ -80,7 +80,7 @@ ghost method {:induction true} Theorem0_Lemma(k: nat)
 {

 }

 

-comethod Theorem1()

+comethod {:induction false} Theorem1()

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

 {

   Theorem1();

@@ -98,17 +98,17 @@ copredicate Pos(s: IList)
   s.head > 0 && Pos(s.tail)

 }

 

-comethod Theorem2(n: int)

+comethod {:induction false} Theorem2(n: int)

   requires 1 <= n;

   ensures Pos(UpIList(n));

 {

   Theorem2(n+1);

 }

 

-comethod Theorem2_NotAProof(n: int)

+comethod {:induction false} Theorem2_NotAProof(n: int)

   requires 1 <= n;

   ensures Pos(UpIList(n));

-{  // error: this is not a proof

+{  // error: this is not a proof (without automatic induction)

 }

 

 codatatype TList<T> = TCons(head: T, tail: TList);

@@ -125,7 +125,7 @@ function GG<T>(h: T): TList<T>
   TCons(h, GG(Next(h)))

 }

 

-comethod Compare<T>(h: T)

+comethod {:induction false} Compare<T>(h: T)

   ensures FF(h) == GG(h);

 {

   assert FF(h).head == GG(h).head;

@@ -142,3 +142,9 @@ comethod Compare<T>(h: T)
     case true =>

   }

 }

+

+comethod {:induction false} BadTheorem(s: IList)

+  ensures false;

+{  // error: postcondition violation

+  BadTheorem(s.tail);

+}

diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index cab0637d..4d197dd7 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -105,7 +105,7 @@ module CoPredicateResolutionErrors {
 

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

 

-module InvalidCoMethodConclusions {

+module UnfruitfulCoMethodConclusions {

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

 

   copredicate Positive(s: Stream<int>)

@@ -114,7 +114,7 @@ module InvalidCoMethodConclusions {
   }

 

   comethod BadTheorem(s: Stream)

-    ensures false;  // error: invalid comethod conclusion

+    ensures false;

   {

     BadTheorem(s.tail);

   }

@@ -123,12 +123,12 @@ module InvalidCoMethodConclusions {
     ensures true && !false;

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

     ensures s.tail == s;

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

+    ensures s.head < 100;

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

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

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

     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

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

   {

   }

 }

diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index 47c5f262..b7dea89d 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -10,14 +10,14 @@ copredicate Pos(s: Stream<int>)
   0 < s.head && Pos(s.tail)

 }

 

-comethod PosLemma0(n: int)

+comethod {:induction false} PosLemma0(n: int)

   requires 1 <= n;

   ensures Pos(Upward(n));

 {

   PosLemma0(n + 1);  // this completes the proof

 }

 

-comethod PosLemma1(n: int)

+comethod {:induction false} PosLemma1(n: int)

   requires 1 <= n;

   ensures Pos(Upward(n));

 {

@@ -27,7 +27,7 @@ comethod PosLemma1(n: int)
   }

 }

 

-comethod Outside_CoMethod_Caller_PosLemma(n: int)

+comethod {:induction false} Outside_CoMethod_Caller_PosLemma(n: int)

   requires 1 <= n;

   ensures Pos(Upward(n));

 {

@@ -51,19 +51,19 @@ copredicate X(s: Stream)  // this is equivalent to always returning 'true'
   X(s)

 }

 

-comethod AlwaysLemma_X0(s: Stream)

+comethod {:induction false} AlwaysLemma_X0(s: Stream)

   ensures X(s);  // prove that X(s) really is always 'true'

 {  // error: this is not the right proof

   AlwaysLemma_X0(s.tail);

 }

 

-comethod AlwaysLemma_X1(s: Stream)

+comethod {:induction false} AlwaysLemma_X1(s: Stream)

   ensures X(s);  // prove that X(s) really is always 'true'

 {

   AlwaysLemma_X1(s);  // this is the right proof

 }

 

-comethod AlwaysLemma_X2(s: Stream)

+comethod {:induction false} AlwaysLemma_X2(s: Stream)

   ensures X(s);

 {

   AlwaysLemma_X2(s);

@@ -77,19 +77,19 @@ copredicate Y(s: Stream)  // this is equivalent to always returning 'true'
   Y(s.tail)

 }

 

-comethod AlwaysLemma_Y0(s: Stream)

+comethod {:induction false} AlwaysLemma_Y0(s: Stream)

   ensures Y(s);  // prove that Y(s) really is always 'true'

 {

   AlwaysLemma_Y0(s.tail);  // this is a correct proof

 }

 

-comethod AlwaysLemma_Y1(s: Stream)

+comethod {:induction false} AlwaysLemma_Y1(s: Stream)

   ensures Y(s);

 {  // error: this is not the right proof

   AlwaysLemma_Y1(s);

 }

 

-comethod AlwaysLemma_Y2(s: Stream)

+comethod {:induction false} AlwaysLemma_Y2(s: Stream)

   ensures Y(s);

 {

   AlwaysLemma_Y2(s.tail);

@@ -103,7 +103,7 @@ copredicate Z(s: Stream)
   false

 }

 

-comethod AlwaysLemma_Z(s: Stream)

+comethod {:induction false} AlwaysLemma_Z(s: Stream)

   ensures Z(s);  // says, perversely, that Z(s) is always 'true'

 {  // error: this had better not lead to a proof

   AlwaysLemma_Z(s);

@@ -119,7 +119,7 @@ copredicate Even(s: Stream<int>)
   s.head % 2 == 0 && Even(s.tail)

 }

 

-comethod Lemma0(n: int)

+comethod {:induction false} Lemma0(n: int)

   ensures Even(Doubles(n));

 {

   Lemma0(n+1);

@@ -130,25 +130,25 @@ function UpwardBy2(n: int): Stream<int>
   Cons(n, UpwardBy2(n + 2))

 }

 

-comethod Lemma1(n: int)

+comethod {:induction false} Lemma1(n: int)

   ensures Even(UpwardBy2(2*n));

 {

   Lemma1(n+1);

 }

 

-comethod ProveEquality(n: int)

+comethod {:induction false} ProveEquality(n: int)

   ensures Doubles(n) == UpwardBy2(2*n);

 {

   ProveEquality(n+1);

 }

 

-comethod BadEquality0(n: int)

+comethod {:induction false} BadEquality0(n: int)

   ensures Doubles(n) == UpwardBy2(n);

 {  // error: postcondition does not hold

   BadEquality0(n+1);

 }

 

-comethod BadEquality1(n: int)

+comethod {:induction false} BadEquality1(n: int)

   ensures Doubles(n) == UpwardBy2(n+1);

 {  // error: postcondition does not hold

   BadEquality1(n+1);