Dafny induction:

* implemented induction tactic for result-less, non-mutating ghost methods
* refine heuristics for determining if a variables is usefully passed to a recursive function
* disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy)
* added command-line flags /induction and /inductionHeuristic (everything is on by default)

1 files changed, 23 insertions, 6 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 591b7383..006c178c 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -137,6 +137,8 @@ namespace Microsoft.Boogie {
     public bool OverlookBoogieTypeErrors = false;

     public bool Verify = true;

     public bool DisallowSoundnessCheating = false;

+    public int DafnyInduction = 3;

+    public int DafnyInductionHeuristic = 3;

     public bool TraceVerify = false;

     public int /*(0:3)*/ ErrorTrace = 1;

     public bool IntraproceduralInfer = true;

@@ -201,12 +203,6 @@ namespace Microsoft.Boogie {
       Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);

       Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC <= 1);

       Contract.Invariant(cce.NonNullElements(ProverOptions));

-

-

-

-

-

-

     }

 

     public int CheckingLevel = 2;

@@ -725,6 +721,16 @@ namespace Microsoft.Boogie {
               break;

             }

 

+          case "-induction":

+          case "/induction":

+            ps.GetNumericArgument(ref DafnyInduction, 4);

+            break;

+

+          case "-inductionHeuristic":

+          case "/inductionHeuristic":

+            ps.GetNumericArgument(ref DafnyInductionHeuristic, 4);

+            break;

+

           case "-contracts":

           case "/contracts":

           case "-c":

@@ -2094,6 +2100,17 @@ namespace Microsoft.Boogie {
                        out.cs, regardless of verification outcome

   /noCheating:<n> : 0 (default) - allow assume statements and free invariants

                     1 - treat all assumptions as asserts, and drop free.

+  /induction:<n> : 0 - never do induction, not even when attributes request it

+                   1 - only apply induction when attributes request it

+                   2 - apply induction as requested (by attributes) and also

+                       for heuristically chosen quantifiers

+                   3 (default) - apply induction as requested, and for

+                       heuristically chosen quantifiers and ghost methods

+  /inductionHeuristic: 0 - least discriminating induction heuristic (that is,

+                           lean toward applying induction more often)

+                       1 - more discriminating

+                       2 - even more discriminating

+                       3 (default) - most discriminating

 

   ---- Boogie options --------------------------------------------------------