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, 3 insertions, 7 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 9938d30a..61b0398f 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -959,13 +959,9 @@ namespace Microsoft.Dafny {
         //   ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));

         // }

         Indent(indent + n * IndentAmount);

-        wr.Write("if (");

-        if (s.Range == null) {

-          wr.Write("true");

-        } else {

-          TrExpr(s.Range);

-        }

-        wr.WriteLine(") {");

+        wr.Write("if ");

+        TrParenExpr(s.Range);

+        wr.WriteLine(" {");

 

         Indent(indent + (n + 1) * IndentAmount);

         wr.Write("{0}.Add(new System.Tuple<{1}>(", ingredients, tupleTypeArgs);