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, 11 insertions, 0 deletions

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 817120ce..539974fd 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -187,3 +187,14 @@ method DuplicateUpdate() {
     }

   }

 }

+

+ghost method DontDoMuch(x: int)

+{

+}

+

+method OmittedRange() {

+  parallel (x) { }

+  parallel (x) {

+    DontDoMuch(x);

+  }

+}