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/Parser.cs | |
| 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/Parser.cs')
| -rw-r--r-- | Source/Dafny/Parser.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 57f4c46e..2fc50c37 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1233,6 +1233,7 @@ List<Expression/*!*/>/*!*/ decreases) { x = t;
Expect(33);
QuantifierDomain(out bvars, out attrs, out range);
+ if (range == null) { range = new LiteralExpr(x, true); }
Expect(34);
while (la.kind == 29 || la.kind == 31) {
isFree = false;
|