diff options
| author |  Rustan Leino <unknown> | 2013-12-30 17:11:46 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-12-30 17:11:46 -0800 |
| commit | 24603296188f3ebd166a0a89da0edac0ebf76d89 (patch) | |
| tree | de1e41f8c41436730f013ef4d052c542fa917667 /Test/dafny0/StatementExpressions.dfy | |
| parent | 14b738e4e40215ddb2442f2294caf7734e9bed07 (diff) | |
Added proper parsing for StmtExpr's in all contexts.
Adjusted printer accordingly.
Fixed bug in Substituter for CalcStmt in StmtExpr's.
Always show terminating semi-colon in hover-text for default decreases clauses.
Diffstat (limited to 'Test/dafny0/StatementExpressions.dfy')
| -rw-r--r-- | Test/dafny0/StatementExpressions.dfy | 71 |
1 files changed, 71 insertions, 0 deletions
diff --git a/Test/dafny0/StatementExpressions.dfy b/Test/dafny0/StatementExpressions.dfy index 386d030b..99416013 100644 --- a/Test/dafny0/StatementExpressions.dfy +++ b/Test/dafny0/StatementExpressions.dfy @@ -85,3 +85,74 @@ function F_PreconditionViolation(n: int): int L(n); // error: argument might be negative
50 / Fact(n)
}
+
+// --------------------- These had had parsing problems in the past
+
+lemma MyLemma(x: int) {
+ var d: Dtz;
+ if 0 < x {
+ var y: int;
+ match MyLemma(y); d { // error: cannot prove termination
+ case Cons0(_) =>
+ case Cons1(_) =>
+ }
+ }
+}
+
+function Parsing_Regression_test0(): int
+{
+ var x := 12;
+ assert x < 20;
+ MyLemma(x);
+ calc { x; < x+1; }
+ // and again
+ var x := 12;
+ assert x < 20;
+ MyLemma(x);
+ calc { x; < x+1; }
+ 17
+}
+
+datatype Dtz = Cons0(int) | Cons1(bool)
+
+function Parsing_Regression_test1(dtz: Dtz): int
+{
+ match dtz
+ case Cons0(s) =>
+ var x := 12;
+ assert x < 20;
+ MyLemma(x);
+ calc { x; < x+1; }
+ // and again
+ var x := 12;
+ assert x < 20;
+ MyLemma(x);
+ calc { x; < x+1; }
+ 17
+ case Cons1(_) =>
+ var x := 12;
+ assert x < 20;
+ MyLemma(x);
+ calc { x; < x+1; }
+ // and again
+ var x := 12;
+ assert x < 20;
+ MyLemma(x);
+ calc { x; < x+1; }
+ 19
+}
+
+function Parsing_Regression_test2(): int
+{
+ // parentheses should be allowed anywhere
+ var x := 12;
+ ( assert x < 20;
+ ( MyLemma(x);
+ ( calc { x; < x+1; }
+ ( var x := 12;
+ ( assert x < 20;
+ ( MyLemma(x);
+ ( calc { x; < x+1; }
+ 17
+ ) ) ) ) ) ) )
+}
|