Dafny: Added heuristic for when to turn on the induction tactic

6 files changed, 268 insertions, 79 deletions

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 6b97b471..0b6d4446 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -168,9 +168,9 @@ namespace Microsoft.Dafny {
       if (a != null) {

         PrintAttributes(a.Prev);

         

-        wr.Write("{ :{0}", a.Name);

+        wr.Write("{{:{0}", a.Name);

         PrintAttributeArgs(a.Args);

-        wr.Write(" } ");

+        wr.Write("} ");

       }

     }

     

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 1ba05262..140c7037 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -4974,71 +4974,67 @@ namespace Microsoft.Dafny {
 

       } else if (expr is ForallExpr) {

         ForallExpr e = (ForallExpr)expr;

-        for (var a = e.Attributes; a != null; a = a.Prev) {

-          if (a.Name == "induction") {

-            if (e.BoundVars.Count == 1) {

-              var n = e.BoundVars[0];

-              // From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation

-              //   (forall n :: (forall k :: k < n ==> P(k)) ==> P(n))

-              BoundVar k = new BoundVar(n.tok, n.Name + "$ih#" + otherTmpVarCount, n.Type);

-              otherTmpVarCount++;

-

-              IdentifierExpr ieK = new IdentifierExpr(k.tok, k.UniqueName);

-              ieK.Var = k; ieK.Type = ieK.Var.Type;  // resolve it here

-              Bpl.Expr boogieK = etran.TrExpr(ieK);

-

-              IdentifierExpr ieN = new IdentifierExpr(n.tok, n.UniqueName);

-              ieN.Var = n; ieN.Type = ieN.Var.Type;  // resolve it here

-              Bpl.Expr boogieN = etran.TrExpr(ieN);

-

-              var substMap = new Dictionary<IVariable, Expression>();

-              substMap.Add(n, ieK);

-              Expression bodyK = Substitute(e.Body, null, substMap);

-

-              Bpl.Expr less;  // says that k is bounded from below and less than n, for each respective type

-              if (n.Type is BoolType) {

-                less = Bpl.Expr.And(Bpl.Expr.Not(boogieK), boogieN);

-              } else if (n.Type is IntType) {

-                less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), boogieK), Bpl.Expr.Lt(boogieK, boogieN));

-              } else if (n.Type is SetType) {

-                less = etran.ProperSubset(e.tok, boogieK, boogieN);

-              } else if (n.Type is SeqType) {

-                Bpl.Expr b0 = FunctionCall(e.tok, BuiltinFunction.SeqLength, null, boogieK);

-                Bpl.Expr b1 = FunctionCall(e.tok, BuiltinFunction.SeqLength, null, boogieN);

-                less = Bpl.Expr.Lt(b0, b1);

-              } else if (n.Type.IsDatatype) {

-                Bpl.Expr b0 = FunctionCall(e.tok, BuiltinFunction.DtRank, null, boogieK);

-                Bpl.Expr b1 = FunctionCall(e.tok, BuiltinFunction.DtRank, null, boogieN);

-                less = Bpl.Expr.Lt(b0, b1);

-              } else {

-                // reference type

-                Bpl.Expr b0 = Bpl.Expr.Neq(boogieK, predef.Null);

-                Bpl.Expr b1 = Bpl.Expr.Neq(boogieN, predef.Null);

-                less = Bpl.Expr.And(Bpl.Expr.Not(b0), b1);

-              }

-

-              Bpl.Expr ihBody = Bpl.Expr.Imp(less, etran.TrExpr(bodyK));

-              Bpl.VariableSeq bvars = new Bpl.VariableSeq();

-              Bpl.Expr typeAntecedent = etran.TrBoundVariables(new List<BoundVar>() { k }, bvars);

-              Bpl.Expr ih = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, ihBody));

-

-              // More precisely now:

-              //   (forall n :: n-has-expected-type && (forall k :: k < n ==> P(k)) && case0(n)   ==> P(n))

-              //   (forall n :: n-has-expected-type && (forall k :: k < n ==> P(k)) && case...(n) ==> P(n))

-              bvars = new Bpl.VariableSeq();

-              typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);

-              foreach (var kase in InductionCases(expr.tok, n.Type, boogieN, etran)) {

-                var ante = BplAnd(BplAnd(typeAntecedent, ih), kase);

-                var bdy = etran.LayerOffset(1).TrExpr(e.Body);

-                Bpl.Expr q = new Bpl.ForallExpr(kase.tok, bvars, Bpl.Expr.Imp(ante, bdy));

-                splits.Add(new SplitExprInfo(false, q));

-              }

+        if (ApplyInduction(e)) {

+          var n = e.BoundVars[0];

+          // From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation

+          //   (forall n :: (forall k :: k < n ==> P(k)) ==> P(n))

+          BoundVar k = new BoundVar(n.tok, n.Name + "$ih#" + otherTmpVarCount, n.Type);

+          otherTmpVarCount++;

+

+          IdentifierExpr ieK = new IdentifierExpr(k.tok, k.UniqueName);

+          ieK.Var = k; ieK.Type = ieK.Var.Type;  // resolve it here

+          Bpl.Expr boogieK = etran.TrExpr(ieK);

+

+          IdentifierExpr ieN = new IdentifierExpr(n.tok, n.UniqueName);

+          ieN.Var = n; ieN.Type = ieN.Var.Type;  // resolve it here

+          Bpl.Expr boogieN = etran.TrExpr(ieN);

+

+          var substMap = new Dictionary<IVariable, Expression>();

+          substMap.Add(n, ieK);

+          Expression bodyK = Substitute(e.Body, null, substMap);

+

+          Bpl.Expr less;  // says that k is bounded from below and less than n, for each respective type

+          if (n.Type is BoolType) {

+            less = Bpl.Expr.And(Bpl.Expr.Not(boogieK), boogieN);

+          } else if (n.Type is IntType) {

+            less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), boogieK), Bpl.Expr.Lt(boogieK, boogieN));

+          } else if (n.Type is SetType) {

+            less = etran.ProperSubset(e.tok, boogieK, boogieN);

+          } else if (n.Type is SeqType) {

+            Bpl.Expr b0 = FunctionCall(e.tok, BuiltinFunction.SeqLength, null, boogieK);

+            Bpl.Expr b1 = FunctionCall(e.tok, BuiltinFunction.SeqLength, null, boogieN);

+            less = Bpl.Expr.Lt(b0, b1);

+          } else if (n.Type.IsDatatype) {

+            Bpl.Expr b0 = FunctionCall(e.tok, BuiltinFunction.DtRank, null, boogieK);

+            Bpl.Expr b1 = FunctionCall(e.tok, BuiltinFunction.DtRank, null, boogieN);

+            less = Bpl.Expr.Lt(b0, b1);

+          } else {

+            // reference type

+            Bpl.Expr b0 = Bpl.Expr.Neq(boogieK, predef.Null);

+            Bpl.Expr b1 = Bpl.Expr.Neq(boogieN, predef.Null);

+            less = Bpl.Expr.And(Bpl.Expr.Not(b0), b1);

+          }

 

-              // Finally, assume the original quantifier (forall n :: P(n))

-              splits.Add(new SplitExprInfo(true, etran.TrExpr(expr)));

-              return true;

-            }

+          Bpl.Expr ihBody = Bpl.Expr.Imp(less, etran.TrExpr(bodyK));

+          Bpl.VariableSeq bvars = new Bpl.VariableSeq();

+          Bpl.Expr typeAntecedent = etran.TrBoundVariables(new List<BoundVar>() { k }, bvars);

+          Bpl.Expr ih = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, ihBody));

+

+          // More precisely now:

+          //   (forall n :: n-has-expected-type && (forall k :: k < n ==> P(k)) && case0(n)   ==> P(n))

+          //   (forall n :: n-has-expected-type && (forall k :: k < n ==> P(k)) && case...(n) ==> P(n))

+          bvars = new Bpl.VariableSeq();

+          typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);

+          foreach (var kase in InductionCases(expr.tok, n.Type, boogieN, etran)) {

+            var ante = BplAnd(BplAnd(typeAntecedent, ih), kase);

+            var bdy = etran.LayerOffset(1).TrExpr(e.Body);

+            Bpl.Expr q = new Bpl.ForallExpr(kase.tok, bvars, Bpl.Expr.Imp(ante, bdy));

+            splits.Add(new SplitExprInfo(false, q));

           }

+

+          // Finally, assume the original quantifier (forall n :: P(n))

+          splits.Add(new SplitExprInfo(true, etran.TrExpr(expr)));

+          return true;

         }

       }

 

@@ -5052,6 +5048,158 @@ namespace Microsoft.Dafny {
       }

     }

 

+    bool ApplyInduction(ForallExpr e)

+    {

+      Contract.Requires(e != null);

+      Contract.Ensures(!Contract.Result<bool>() || e.BoundVars.Count == 1);

+

+      if (e.BoundVars.Count != 1) {

+        return false;

+      }

+      for (var a = e.Attributes; a != null; a = a.Prev) {

+        if (a.Name == "induction") {

+          // return 'true', except if there is one argument and it is 'false'

+          if (a.Args.Count == 1) {

+            var arg = a.Args[0].E as LiteralExpr;

+            if (arg != null && arg.Value is bool && !(bool)arg.Value) {

+              if (CommandLineOptions.Clo.Trace) {

+                Console.Write("Suppressing automatic induction on: ");

+                new Printer(Console.Out).PrintExpression(e);

+                Console.WriteLine();

+              }

+              return false;

+            }

+          }

+          if (CommandLineOptions.Clo.Trace) {

+            Console.Write("Applying requested induction on: ");

+            new Printer(Console.Out).PrintExpression(e);

+            Console.WriteLine();

+          }

+          return true;

+        }

+      }

+

+      // consider automatically applying induction

+      var n = e.BoundVars[0];

+      if (VarOccursInArgumentToRecursiveFunction(e.Body, n, null)) {

+        if (CommandLineOptions.Clo.Trace) {

+          Console.Write("Applying automatic induction on: ");

+          new Printer(Console.Out).PrintExpression(e);

+          Console.WriteLine();

+        }

+        return true;

+      }

+

+      return false;

+    }

+

+    /// <summary>

+    /// Returns 'true' iff

+    ///    there is a subexpression of 'expr' of the form 'F(...n...)' where 'F' is a recursive function

+    ///    and 'n' appears in an "elevated" subexpression of some argument to 'F',

+    ///    or

+    ///    'p' is non-null and 'p' appears in an "elevated" subexpression of 'expr'.

+    /// Requires that 'p' is either 'null' of 'n'.

+    /// </summary>

+    static bool VarOccursInArgumentToRecursiveFunction(Expression expr, BoundVar n, BoundVar p) {

+      Contract.Requires(expr != null);

+      Contract.Requires(n != null);

+

+      if (expr is LiteralExpr || expr is WildcardExpr || expr is ThisExpr) {

+        return false;

+      } else if (expr is IdentifierExpr) {

+        var e = (IdentifierExpr)expr;

+        return p != null && e.Var == p;

+      } else if (expr is DisplayExpression) {

+        var e = (DisplayExpression)expr;

+        return e.Elements.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, null));  // subexpressions are not "elevated"

+      } else if (expr is FieldSelectExpr) {

+        var e = (FieldSelectExpr)expr;

+        return VarOccursInArgumentToRecursiveFunction(e.Obj, n, null);  // subexpressions are not "elevated"

+      } else if (expr is SeqSelectExpr) {

+        var e = (SeqSelectExpr)expr;

+        p = e.SelectOne ? null : p;

+        return VarOccursInArgumentToRecursiveFunction(e.Seq, n, null) ||  // this subexpression is not "elevated"

+          (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, p)) ||  // this one is, if the SeqSelectExpr denotes a range

+          (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, p));    // ditto

+      } else if (expr is SeqUpdateExpr) {

+        var e = (SeqUpdateExpr)expr;

+        return VarOccursInArgumentToRecursiveFunction(e.Seq, n, p) ||  // this subexpression is "elevated"

+          VarOccursInArgumentToRecursiveFunction(e.Index, n, null) ||  // but this one

+          VarOccursInArgumentToRecursiveFunction(e.Value, n, null);    // and this one are not

+      } else if (expr is MultiSelectExpr) {

+        var e = (MultiSelectExpr)expr;

+        // subexpressions are not "elevated"

+        return VarOccursInArgumentToRecursiveFunction(e.Array, n, null) ||

+          e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, null));

+      } else if (expr is FunctionCallExpr) {

+        var e = (FunctionCallExpr)expr;

+        // For recursive functions:  arguments are "elevated"

+        // For non-recursive function:  arguments are "elevated" if the call is

+        if (e.Function.IsRecursive) {

+          p = n;

+        }

+        return VarOccursInArgumentToRecursiveFunction(e.Receiver, n, p) ||

+          e.Args.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, p));

+      } else if (expr is DatatypeValue) {

+        var e = (DatatypeValue)expr;

+        if (!n.Type.IsDatatype) {

+          p = null;

+        }

+        return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, p));

+      } else if (expr is OldExpr) {

+        var e = (OldExpr)expr;

+        return VarOccursInArgumentToRecursiveFunction(e.E, n, p);

+      } else if (expr is FreshExpr) {

+        var e = (FreshExpr)expr;

+        return VarOccursInArgumentToRecursiveFunction(e.E, n, null);

+      } else if (expr is AllocatedExpr) {

+        var e = (AllocatedExpr)expr;

+        return VarOccursInArgumentToRecursiveFunction(e.E, n, null);

+      } else if (expr is UnaryExpr) {

+        var e = (UnaryExpr)expr;

+        // arguments to both Not and SeqLength are "elevated"

+        return VarOccursInArgumentToRecursiveFunction(e.E, n, p);

+      } else if (expr is BinaryExpr) {

+        var e = (BinaryExpr)expr;

+        switch (e.ResolvedOp) {

+          case BinaryExpr.ResolvedOpcode.Add:

+          case BinaryExpr.ResolvedOpcode.Sub:

+          case BinaryExpr.ResolvedOpcode.Mul:

+          case BinaryExpr.ResolvedOpcode.Div:

+          case BinaryExpr.ResolvedOpcode.Mod:

+          case BinaryExpr.ResolvedOpcode.Union:

+          case BinaryExpr.ResolvedOpcode.Intersection:

+          case BinaryExpr.ResolvedOpcode.SetDifference:

+          case BinaryExpr.ResolvedOpcode.Concat:

+            // these operators have "elevated" arguments

+            break;

+          default:

+            // whereas all other binary operators do not

+            p = null;

+            break;

+        }

+        return VarOccursInArgumentToRecursiveFunction(e.E0, n, p) ||

+          VarOccursInArgumentToRecursiveFunction(e.E1, n, p);

+      } else if (expr is QuantifierExpr) {

+        var e = (QuantifierExpr)expr;

+        return VarOccursInArgumentToRecursiveFunction(e.Body, n, null);

+      } else if (expr is ITEExpr) {

+        var e = (ITEExpr)expr;

+        return VarOccursInArgumentToRecursiveFunction(e.Test, n, null) ||  // test is not "elevated"

+          VarOccursInArgumentToRecursiveFunction(e.Thn, n, p) ||           // but the two branches are

+          VarOccursInArgumentToRecursiveFunction(e.Els, n, p);

+      } else if (expr is BoxingCastExpr) {

+        var e = (BoxingCastExpr)expr;

+        return VarOccursInArgumentToRecursiveFunction(e.E, n, p);

+      } else if (expr is UnboxingCastExpr) {

+        var e = (UnboxingCastExpr)expr;

+        return VarOccursInArgumentToRecursiveFunction(e.E, n, p);

+      } else {

+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member

+      }

+    }

+

     IEnumerable<Bpl.Expr> InductionCases(IToken tok, Type ty, Bpl.Expr expr, ExpressionTranslator etran) {

       DatatypeDecl dt = ty.AsDatatype;

       if (dt == null) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4bf7e527..c33cf851 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -484,7 +484,7 @@ Execution trace:
     (0,0): anon13_Else

     (0,0): anon8

 

-Dafny program verifier finished with 41 verified, 6 errors

+Dafny program verifier finished with 44 verified, 6 errors

 

 -------------------- Use.dfy --------------------

 Use.dfy(16,18): Error: assertion violation

@@ -543,8 +543,14 @@ DTypes.dfy(134,6): Related location: Related location
 DTypes.dfy(93,3): Related location: Related location

 Execution trace:

     (0,0): anon0

+DTypes.dfy(160,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon6_Then

+    (0,0): anon4

 

-Dafny program verifier finished with 24 verified, 5 errors

+Dafny program verifier finished with 27 verified, 6 errors

 

 -------------------- TypeParameters.dfy --------------------

 TypeParameters.dfy(41,22): Error: assertion violation

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index efd2f6f0..2f59db73 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -105,7 +105,7 @@ class DatatypeInduction<T> {
   method Theorem0(tree: Tree<T>)

     ensures 1 <= LeafCount(tree);

   {

-    assert (forall t: Tree<T> {:induction} :: 1 <= LeafCount(t));

+    assert (forall t: Tree<T> :: 1 <= LeafCount(t));

   }

 

   // also make sure it works for an instantiated generic datatype

@@ -113,29 +113,50 @@ class DatatypeInduction<T> {
     ensures 1 <= LeafCount(bt);

     ensures 1 <= LeafCount(it);

   {

-    assert (forall t: Tree<bool> {:induction} :: 1 <= LeafCount(t));

-    assert (forall t: Tree<int> {:induction} :: 1 <= LeafCount(t));

+    assert (forall t: Tree<bool> :: 1 <= LeafCount(t));

+    assert (forall t: Tree<int> :: 1 <= LeafCount(t));

   }

 

   method NotATheorem0(tree: Tree<T>)

     ensures LeafCount(tree) % 2 == 1;

   {

-    assert (forall t: Tree<T> {:induction} :: LeafCount(t) % 2 == 1);  // error: fails for Branch case

+    assert (forall t: Tree<T> :: LeafCount(t) % 2 == 1);  // error: fails for Branch case

   }

 

   method NotATheorem1(tree: Tree<T>)

     ensures 2 <= LeafCount(tree);

   {

-    assert (forall t: Tree<T> {:induction} :: 2 <= LeafCount(t));  // error: fails for Leaf case

+    assert (forall t: Tree<T> :: 2 <= LeafCount(t));  // error: fails for Leaf case

   }

 

   function Predicate(): bool

   {

-    (forall t: Tree<T> {:induction} :: 2 <= LeafCount(t))

+    (forall t: Tree<T> :: 2 <= LeafCount(t))

   }

 

   method NotATheorem2()

   {

     assert Predicate();  // error (this tests Related Location for induction via a predicate)

   }

+

+  // ----- here is a test for induction over integers

+

+  method IntegerInduction_Succeeds(a: array<int>)

+    requires a != null;

+    requires a.Length == 0 || a[0] == 0;

+    requires (forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1);

+  {

+    // The following assertion can be proved by induction:

+    assert (forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n);

+  }

+

+  method IntegerInduction_Fails(a: array<int>)

+    requires a != null;

+    requires a.Length == 0 || a[0] == 0;

+    requires (forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1);

+  {

+    // ...but the induction heuristics don't recognize the situation as one where

+    // applying induction would be profitable:

+    assert (forall n :: 0 <= n && n < a.Length ==> a[n] == n*n);  // error reported

+  }

 }

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 779c9892..226eadbe 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -310,5 +310,19 @@ function ReachBack(n: int): bool
   requires 0 <= n;

   ensures ReachBack(n);

 {

-  (forall m :: 0 <= m && m < n ==> ReachBack(m))

+  // Turn off induction for this test, since that's not the point of

+  // the test case.

+  (forall m {:induction false} :: 0 <= m && m < n ==> ReachBack(m))

 }

+

+function ReachBack_Alt(n: int): bool

+  requires 0 <= n;

+{

+  n == 0 || ReachBack_Alt(n-1)

+}

+

+ghost method Lemma_ReachBack()

+{

+  assert (forall m :: 0 <= m ==> ReachBack_Alt(m));

+}

+

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index ea447be7..4bd1f35b 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -49,7 +49,7 @@ class IntegerInduction {
     }

   }

 

-  // Here is another proof.  It makes use of Dafny's {:induction} attribute to

+  // Here is another proof.  It makes use of Dafny's induction heuristics to

   // prove the lemma.

 

   ghost method Theorem2(n: int)

@@ -59,7 +59,7 @@ class IntegerInduction {
     if (n != 0) {

       call Theorem0(n-1);

 

-      assert (forall m {:induction} :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));

+      assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));

     }

   }

 

@@ -91,7 +91,7 @@ class IntegerInduction {
   // Finally, with the postcondition of GaussWithPost, one can prove the entire theorem by induction

 

   ghost method Theorem4()

-    ensures (forall n {:induction} :: 0 <= n ==> SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n));

+    ensures (forall n :: 0 <= n ==> SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n));

   {

     // look ma, no hints!

   }

@@ -102,7 +102,7 @@ class IntegerInduction {
   {

     // the postcondition is a simple consequence of these quantified versions of the theorem:

     if (*) {

-      assert (forall m {:induction} :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));

+      assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));

     } else {

       call Theorem4();

     }

@@ -125,7 +125,7 @@ class DatatypeInduction<T> {
   method Theorem0(tree: Tree<T>)

     ensures 1 <= LeafCount(tree);

   {

-    assert (forall t: Tree<T> {:induction} :: 1 <= LeafCount(t));

+    assert (forall t: Tree<T> :: 1 <= LeafCount(t));

   }

 

   // see also Test/dafny0/DTypes.dfy for more variations of this example