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 | 6027c65707f6098bec2e373b738d80b96cbc0a15 (patch) | |
| tree | c0b103dfdf79df2322f1b95102b179f8c9b28697 /Jennisys | |
| parent | 095c4e6d7c81374ea41cdf9526c0b68655ffc01e (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 'Jennisys')
0 files changed, 0 insertions, 0 deletions