diff options
Diffstat (limited to 'Test/codeexpr/CodeExpr2.bpl')
-rw-r--r-- | Test/codeexpr/CodeExpr2.bpl | 104 |
1 files changed, 52 insertions, 52 deletions
diff --git a/Test/codeexpr/CodeExpr2.bpl b/Test/codeexpr/CodeExpr2.bpl index 9d8beed7..0edaa8f4 100644 --- a/Test/codeexpr/CodeExpr2.bpl +++ b/Test/codeexpr/CodeExpr2.bpl @@ -1,52 +1,52 @@ -// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-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);
-}
+// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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); +} |