diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-26 23:40:33 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-26 23:40:33 -0700 |
| commit | 8fba5ba566b28bd012ac5d4485df65308dc338a1 (patch) | |
| tree | 23287b3b10cb9c70ac9ee1f6256075a425759020 /Test/dafny0/ControlStructures.dfy | |
| parent | b649899e20acf38aa8bcf041a55fbd3613b809bf (diff) | |
Dafny:
* fixed ghost/non-ghost story for breaks and returns
* changed compilation/translation to always use goto's to implement Dafny's breaks
* introduced "break break" statements
Diffstat (limited to 'Test/dafny0/ControlStructures.dfy')
| -rw-r--r-- | Test/dafny0/ControlStructures.dfy | 105 |
1 files changed, 105 insertions, 0 deletions
diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy index 2c9b3a35..5012e003 100644 --- a/Test/dafny0/ControlStructures.dfy +++ b/Test/dafny0/ControlStructures.dfy @@ -135,3 +135,108 @@ method B(x: int) returns (r: int) r := r - 1;
}
}
+
+// --------------- breaks ---------------
+
+method TheBreaker_AllGood(M: int, N: int, O: int)
+{
+ var a, b, c, d, e;
+ var i := 0;
+ while (i < M)
+ {
+ var j := 0;
+ label InnerHasLabel:
+ while (j < N)
+ {
+ var u := 2000;
+ label MyLabelBlock:
+ label MyLabelBlockAgain:
+ if (*) {
+ a := 15; break;
+ } else if (*) {
+ b := 12; break break;
+ } else if (*) {
+ c := 21; break InnerHasLabel;
+ } else if (*) {
+ while (u < 10000) {
+ u := u + 3;
+ if (*) { u := 1998; break MyLabelBlock; }
+ if (*) { u := 1998; break MyLabelBlockAgain; }
+ }
+ assert 10000 <= u;
+ u := 1998;
+ } else {
+ u := u - 2;
+ }
+ assert u == 1998;
+ var k := 0;
+ while
+ decreases O - k;
+ {
+ case k < O && k % 2 == 0 =>
+ d := 187; break;
+ case k < O =>
+ if (*) { e := 4; break InnerHasLabel; }
+ if (*) { e := 7; break; }
+ if (*) { e := 37; break break break; }
+ k := k + 1;
+ }
+ assert O <= k || d == 187 || e == 7;
+ j := j + 1;
+ }
+ assert N <= j || a == 15 || c == 21 || e == 4;
+ i := i + 1;
+ }
+ assert M <= i || b == 12 || e == 37;
+}
+
+method TheBreaker_SomeBad(M: int, N: int, O: int)
+{
+ var a, b, c, d, e;
+ var i := 0;
+ while (i < M)
+ {
+ var j := 0;
+ label InnerHasLabel:
+ while (j < N)
+ {
+ var u := 2000;
+ label MyLabelBlock:
+ label MyLabelBlockAgain:
+ if (*) {
+ a := 15; break;
+ } else if (*) {
+ b := 12; break break;
+ } else if (*) {
+ c := 21; break InnerHasLabel;
+ } else if (*) {
+ while (u < 10000) {
+ u := u + 3;
+ if (*) { u := 1998; break MyLabelBlock; }
+ if (*) { u := 1998; break MyLabelBlockAgain; }
+ }
+ assert u < 2000; // error (and no way to get past this assert statement)
+ } else {
+ u := u - 2;
+ }
+ assert u == 1998;
+ var k := 0;
+ while
+ decreases O - k;
+ {
+ case k < O && k % 2 == 0 =>
+ d := 187; break;
+ case k < O =>
+ if (*) { e := 4; break InnerHasLabel; }
+ if (*) { e := 7; break; }
+ if (*) { e := 37; break break break; }
+ k := k + 1;
+ }
+ assert O <= k || e == 7; // error: d == 187
+ j := j + 1;
+ }
+ assert N <= j || c == 21 || e == 4; // error: a == 15
+ i := i + 1;
+ }
+ assert M <= i || b == 12; // error: e == 37
+}
|