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

3 files changed, 50 insertions, 9 deletions

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));

+}

+