diff options
| author |  rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
| commit | 554fb3a6780c412b81dc935835c2760e4cbe0b4d (patch) | |
| tree | b50aa3dbbb369a52751bfcb9f142c9c928e591ae /Test/codeexpr/CodeExpr1.bpl | |
| parent | c2aa0b56fce36a101c3bef7ce901b8f26dcb5f08 (diff) | |
Boogie: Added boolean code expressions (sans well-formedness checks on the input).
Diffstat (limited to 'Test/codeexpr/CodeExpr1.bpl')
| -rw-r--r-- | Test/codeexpr/CodeExpr1.bpl | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/Test/codeexpr/CodeExpr1.bpl b/Test/codeexpr/CodeExpr1.bpl new file mode 100644 index 00000000..3cc92333 --- /dev/null +++ b/Test/codeexpr/CodeExpr1.bpl @@ -0,0 +1,67 @@ +// ------ the good ------
+
+procedure F(x: int, y: int) returns (z: bool)
+ requires x < y;
+ ensures z == (x < 3);
+{
+ start:
+ z := |{ var a : bool, b : bool; B: a := x < 3; return a; }|;
+ return;
+}
+
+function r(int): bool;
+
+procedure F'(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: x < 3 + t ==> r(t));
+ assert r(y);
+}
+
+procedure F''(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: |{ var a: bool;
+ Start:
+ a := x < 3 + t;
+ goto X, Y;
+ X: assume a; return r(t);
+ Y: assume !a; return true;
+ }|);
+ assert r(y);
+}
+
+// ------ the bad ------
+
+procedure G(x: int, y: int) returns (z: bool)
+ requires x < y;
+ ensures z == (x < 3);
+{
+ start:
+ z := |{ var a : bool, b : bool; B: a := x < 3; return !a; }|;
+ return; // error: postcondition violation
+}
+
+procedure G'(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: x + 3 < t ==> r(t));
+ assert r(y); // error
+}
+
+procedure G''(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: |{ var a: bool;
+ Start:
+ a := x + 3 < t;
+ goto X, Y;
+ X: assume a; return r(t);
+ Y: assume !a; return true;
+ }|);
+ assert r(y); // error
+}
|