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 /Source/Dafny/Dafny.atg | |
| 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 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 9de1421b..fa857aad 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -922,6 +922,7 @@ ParallelStmt<out Statement/*!*/ s> "parallel" (. x = t; .)
"("
QuantifierDomain<out bvars, out attrs, out range>
+ (. if (range == null) { range = new LiteralExpr(x, true); } .)
")"
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
|