diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/ControlStructures.dfy | 26 |
2 files changed, 27 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index f2fccb73..a5c48e9a 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1039,7 +1039,7 @@ Execution trace: (0,0): anon89_Then
(0,0): anon61
-Dafny program verifier finished with 18 verified, 10 errors
+Dafny program verifier finished with 20 verified, 10 errors
-------------------- Termination.dfy --------------------
Termination.dfy(356,47): Error: failure to decrease termination measure
diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy index c46eee3a..2136e2f1 100644 --- a/Test/dafny0/ControlStructures.dfy +++ b/Test/dafny0/ControlStructures.dfy @@ -237,3 +237,29 @@ method TheBreaker_SomeBad(M: int, N: int, O: int) }
assert M <= i || b == 12; // error: e == 37
}
+
+// --------------- paren-free syntax ---------------
+
+method PF1(d: D)
+ requires d == D.Green;
+{
+ if d != D.Green { // guards can be written without parens
+ match d {
+ }
+ }
+ if { case false => assert false; case true => assert true; }
+ if {1, 2, 3} <= {1, 2} { // conflict between display set as guard and alternative statement is resolved
+ assert false;
+ }
+ while d != D.Green {
+ assert false;
+ }
+ while d != D.Green
+ decreases 1;
+ {
+ assert false;
+ }
+ while {1, 2, 3} <= {1, 2} {
+ assert false;
+ }
+}
|