diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 22 | ||||
| -rw-r--r-- | Test/dafny0/ControlStructures.dfy | 34 |
2 files changed, 39 insertions, 17 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 40725691..7186f30f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -864,7 +864,7 @@ Execution trace: (0,0): anon89_Then
(0,0): anon61
-Dafny program verifier finished with 20 verified, 10 errors
+Dafny program verifier finished with 22 verified, 10 errors
-------------------- Termination.dfy --------------------
Termination.dfy(356,47): Error: failure to decrease termination measure
@@ -1672,36 +1672,36 @@ Execution trace: Dafny program verifier finished with 38 verified, 11 errors
-------------------- Superposition.dfy --------------------
- +
Verifying CheckWellformed$$_0_M0.C.M ...
[0 proof obligations] verified
- +
Verifying Impl$$_0_M0.C.M ...
[4 proof obligations] verified
- +
Verifying CheckWellformed$$_0_M0.C.P ...
[4 proof obligations] verified
- +
Verifying CheckWellformed$$_0_M0.C.Q ...
[3 proof obligations] error
Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon5_Else
- +
Verifying CheckWellformed$$_0_M0.C.R ...
[3 proof obligations] error
Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon5_Else
- +
Verifying CheckWellformed$$_1_M1.C.M ...
[0 proof obligations] verified
- +
Verifying Impl$$_1_M1.C.M ...
[1 proof obligation] verified
- +
Verifying CheckWellformed$$_1_M1.C.P ...
[1 proof obligation] error
Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.
@@ -1710,10 +1710,10 @@ Execution trace: (0,0): anon7_Else
(0,0): anon9_Then
(0,0): anon6
- +
Verifying CheckWellformed$$_1_M1.C.Q ...
[0 proof obligations] verified
- +
Verifying CheckWellformed$$_1_M1.C.R ...
[0 proof obligations] verified
diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy index 2136e2f1..95aff80e 100644 --- a/Test/dafny0/ControlStructures.dfy +++ b/Test/dafny0/ControlStructures.dfy @@ -238,28 +238,50 @@ method TheBreaker_SomeBad(M: int, N: int, O: int) assert M <= i || b == 12; // error: e == 37
}
+method BreakStatements(d: D, n: nat)
+{
+ var i := 0;
+ while i < n {
+ if i % 7 == 3 { break; }
+ match d {
+ case Green =>
+ case Blue =>
+ var j := 63;
+ while j < 3000
+ {
+ if j % n == 0 { break; } // in a previous version, this was translated into a malformed Boogie program
+ if j % (n+1) == 0 { break break; }
+ j := j + 1;
+ }
+ case Red =>
+ case Purple =>
+ }
+ i := i + 1;
+ }
+}
+
// --------------- paren-free syntax ---------------
method PF1(d: D)
requires d == D.Green;
{
- if d != D.Green { // guards can be written without parens
+ 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;
+ assert false;
}
while d != D.Green {
- assert false;
+ assert false;
}
while d != D.Green
- decreases 1;
+ decreases 1;
{
- assert false;
+ assert false;
}
while {1, 2, 3} <= {1, 2} {
- assert false;
+ assert false;
}
}
|