summaryrefslogtreecommitdiff
path: root/Test/codeexpr/CodeExpr2.bpl
blob: 61758d5a547b9b5b93a53f15d8b0ee622fa4d027 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
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);
}