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/CodeExpr2.bpl | |
| parent | c2aa0b56fce36a101c3bef7ce901b8f26dcb5f08 (diff) | |
Boogie: Added boolean code expressions (sans well-formedness checks on the input).
Diffstat (limited to 'Test/codeexpr/CodeExpr2.bpl')
| -rw-r--r-- | Test/codeexpr/CodeExpr2.bpl | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/Test/codeexpr/CodeExpr2.bpl b/Test/codeexpr/CodeExpr2.bpl new file mode 100644 index 00000000..61758d5a --- /dev/null +++ b/Test/codeexpr/CodeExpr2.bpl @@ -0,0 +1,50 @@ +type T;
+const zero: T;
+
+function IsProperIndex(i: int, size: int): bool;
+
+procedure P(a: [int]T, n: int)
+ requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+{
+ call Q(a, n);
+}
+
+procedure Q(a: [int]T, n: int)
+ requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+{
+ call P(a, n);
+}
+
+procedure A(a: [int]T, n: int)
+{
+ assert
+ (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)
+ ==>
+ (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure B(a: [int]T, n: int)
+{
+ assert
+ (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)
+ ==>
+ (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}
+
+procedure C(a: [int]T, n: int)
+{
+ Start:
+ assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+ goto Next;
+ Next:
+ assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure D(a: [int]T, n: int)
+{
+ Start:
+ assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+ goto Next;
+ Next:
+ assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}
|