diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-29 16:59:46 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-29 16:59:46 -0700 |
| commit | c8452b274087624140cb7f2424b321de54fcb41a (patch) | |
| tree | 6dd73ee0dc98d9c6997e39b6e109a1d5e4c02a74 /Test/dafny1/Answer | |
| parent | e7bf7ffb17f0c4022c3df81b4fe33df440723c37 (diff) | |
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)
Diffstat (limited to 'Test/dafny1/Answer')
| -rw-r--r-- | Test/dafny1/Answer | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 0a99ca95..d53ae14b 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -81,11 +81,11 @@ Dafny program verifier finished with 6 verified, 0 errors -------------------- Induction.dfy --------------------
-Dafny program verifier finished with 29 verified, 0 errors
+Dafny program verifier finished with 33 verified, 0 errors
-------------------- Rippling.dfy --------------------
-Dafny program verifier finished with 137 verified, 0 errors
+Dafny program verifier finished with 141 verified, 0 errors
-------------------- MoreInduction.dfy --------------------
|