diff options
Diffstat (limited to 'Test/test2/Structured.bpl')
| -rw-r--r-- | Test/test2/Structured.bpl | 327 |
1 files changed, 327 insertions, 0 deletions
diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl new file mode 100644 index 00000000..ce97b145 --- /dev/null +++ b/Test/test2/Structured.bpl @@ -0,0 +1,327 @@ +
+const K: int;
+
+function f(int) returns (int);
+
+axiom (exists k: int :: f(k) == K);
+
+procedure Find(a: int, b: int) returns (k: int);
+ requires a <= b && (forall j: int :: a < j && j < b ==> f(j) != K);
+ ensures f(k) == K;
+
+// nondeterministic, unstructured, recursive version
+implementation Find(a: int, b: int) returns (k: int)
+{
+ entry:
+ goto A, B, C;
+
+ A:
+ assume f(a) == K;
+ k := a;
+ return;
+
+ B:
+ assume f(b) == K;
+ k := b;
+ return;
+
+ C:
+ assume f(a) != K && f(b) != K;
+ call k := Find(a-1, b+1);
+ return;
+}
+
+// nondeterministic, recursive version
+implementation Find(a: int, b: int) returns (k: int)
+{
+ if (*) {
+ assume f(a) == K;
+ k := a;
+ } else if (*) {
+ assume f(b) == K;
+ k := b;
+ } else {
+ assume f(a) != K && f(b) != K;
+ call k := Find(a-1, b+1);
+ }
+}
+
+// deterministic, structured, recursive version
+implementation Find(a: int, b: int) returns (k: int)
+{
+ if (f(a) == K) {
+ k := a;
+ } else if (f(b) == K) {
+ k := b;
+ } else {
+ call k := Find(a-1, b+1);
+ }
+}
+
+// deterministic, structured, iterative version
+implementation Find(a: int, b: int) returns (k: int)
+{
+ var x: int, y: int;
+
+ x := a;
+ y := b;
+
+ while (f(x) != K && f(y) != K)
+ invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
+ {
+ x := x-1;
+ y := y+1;
+ }
+
+ if (f(x) == K) {
+ k := x;
+ } else {
+ k := y;
+ }
+}
+
+// deterministic, structured, iterative version with breaks
+implementation Find(a: int, b: int) returns (k: int)
+{
+ var x: int, y: int;
+
+ x := a;
+ y := b;
+
+ while (true)
+ invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
+ {
+ if (f(x) == K) {
+ k := x;
+ break;
+ } else if (f(y) == K) {
+ k := y;
+ break;
+ }
+ x := x-1;
+ y := y+1;
+ }
+}
+
+// deterministic, somewhat structured, iterative version
+implementation Find(a: int, b: int) returns (k: int)
+{
+ var x: int, y: int;
+
+ x := a;
+ y := b;
+
+ while (true)
+ invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
+ {
+ if (f(x) == K) {
+ goto FoundX;
+ } else if (f(y) == K) {
+ goto FoundY;
+ }
+ x := x-1;
+ y := y+1;
+ }
+
+ FoundX:
+ k := x;
+ return;
+
+ FoundY:
+ k := y;
+ return;
+}
+
+// deterministic, structured, iterative version with breaks
+implementation Find(a: int, b: int) returns (k: int)
+{
+ var x: int, y: int;
+
+ x := a;
+ y := b;
+
+ outer:
+ if (true) {
+ inner:
+ while (true)
+ invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K);
+ {
+ if (f(x) == K) {
+ break inner;
+ } else if (f(y) == K) {
+ break outer;
+ }
+ x := x-1;
+ y := y+1;
+ }
+
+ k := x;
+ return;
+ }
+ k := y;
+}
+
+// ----- free invariant -----
+
+function Teal(int) returns (bool);
+function ShadeOfGreen(int) returns (bool);
+axiom (forall w: int :: Teal(w) ==> ShadeOfGreen(w));
+
+procedure P(x: int) returns (y: int)
+ requires Teal(x);
+ ensures ShadeOfGreen(y);
+{
+ y := x;
+ while (y < 100)
+ free invariant Teal(y);
+ {
+ y := y + 5;
+ }
+}
+
+// ----- run off the end of the BigBlock -----
+
+procedure RunOffEnd0() returns (x: int)
+ ensures x == 3;
+{
+ x := 0;
+ Label0:
+ x := x + 1;
+ Label1:
+ x := x + 1;
+ Label2:
+ Label3:
+ Label4:
+ x := x + 1;
+}
+
+procedure RunOffEnd1() returns (x: int)
+ ensures x == 4;
+{
+ x := 0;
+ Label0:
+ x := x + 1;
+ Label1:
+ if (*) {
+ Label2:
+ x := x + 2;
+ } else if (*) {
+ Label3:
+ x := 2;
+ x := x + 2;
+ Label4:
+ Label5:
+ x := x - 1;
+ } else {
+ if (*) {
+ x := 0;
+ while (x < 3)
+ invariant x <= 3;
+ { x := x + 1; }
+ } else {
+ x := x + 2;
+ }
+ }
+ x := x + 1;
+}
+
+procedure RunOffEnd2() returns (x: int)
+ ensures x == 10;
+{
+ while (true) {
+ while (true) {
+ if (*) {
+ x := 10;
+ break;
+ }
+ }
+ if (*) { break; }
+ }
+}
+
+procedure RunOffEnd3() returns (x: int)
+ ensures x == 9;
+{
+ while (true) {
+ while (true) {
+ if (*) {
+ x := 10;
+ break;
+ }
+ }
+ if (*) { break; }
+ } // error: violated postcondition
+}
+
+procedure RunOffEnd4() returns (x: int)
+{
+ var y: int;
+ var bad: bool;
+
+ while (true) {
+ y := x;
+ bad := false;
+ if (*) {
+ x := x + 1;
+ bad := true;
+ }
+ if (x == y) { break; }
+ }
+ assert !bad;
+}
+
+procedure RunOffEnd5() returns (x: int)
+{
+ while (true) {
+ if (x == 5) { }
+ }
+ assert false;
+}
+
+procedure RunOffEnd6() returns (x: int)
+{
+ x := 7;
+ while (true)
+ invariant x == 7;
+ {
+ x := 5;
+ MyLabel:
+ x := 7;
+ }
+}
+
+// ----- jump optimizations -----
+
+procedure Q0()
+{
+ var x: int;
+
+ x := 0;
+ if (*) {
+ x := 1;
+ }
+ assert x == 1; // error
+}
+
+procedure Q1() returns (x: int)
+{
+ if (x == 0) {
+ A:
+ x := x + 0;
+ assert x == 0; // error
+ B:
+ x := x + 1;
+ goto A;
+ }
+}
+
+procedure Q2() returns (x: int)
+{
+ if (x == 0) {
+ while (x < 10)
+ invariant x <= 10;
+ {
+ x := x + 1;
+ }
+ }
+}
|