summaryrefslogtreecommitdiff
path: root/Test/test2/Quantifiers.bpl
blob: d368fe1f5dad97f5e59c97d818a155080eca7077 (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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
// ----------------------------------------------------------------------- single trigger

function f(int, int) returns (int);

axiom (forall x: int, y: int :: f(x,y) < x+y);
axiom (forall x: int :: { f(x,10) } f(x,10) == 3);

procedure P(a: int, b: int)
  requires a <= 25 && b <= 30;
{
  start:
    assert f(a,b) <= 100;
    return;
}

procedure Q(a: int, b: int)
  requires a + 2 <= b;
{
  start:
    assert f(a,b) == 3;   // not provable with the trigger given above
    return;
}

procedure R(a: int, b: int)
  requires a + 2 <= b;
{
  start:
    assume b <= 10 && 8 <= a;
    assert f(a,b) == 3;   // now, the trigger should fire
    return;
}

// ----------------------------------------------------------------------- multi trigger

function g(int, int) returns (int);

axiom (forall x: int, y: int :: { g(x,10),g(x,y) } g(x,y) == 3);  // multi-trigger

procedure S(a: int, b: int)
  requires a + 2 <= b;
{
  start:
    assert g(a,b) == 3;   // not provable with the trigger given above
    return;
}

procedure T(a: int, b: int)
  requires a + 2 <= b;
{
  start:
    assume b <= 10 && 8 <= a;
    assert g(a,b) == 3;   // this should trigger
    return;
}

// ----------------------------------------------------------------------- several triggers

function h(int, int) returns (int);

axiom (forall y: int :: { g(y,y) } { h(y,h(y,10)) } h(y, h(y,y)) == y);  // several triggers

procedure U0(a: int)
{
  start:
    assert h(a,h(a,a)) == a;   // not provable with the triggers given above
    return;
}

procedure U1(a: int, b: int)
{
  start:
    assume g(a,b) == 5;
    assert h(a,h(a,a)) == a;   // not provable with the triggers given above
    return;
}

procedure V0(a: int, b: int)
  requires a == b;
{
  start:
    assume g(a,b) == 5;
    assert h(a,h(a,a)) == a;   // this should trigger
    return;
}

procedure V1(a: int, b: int)
{
  start:
    assume a == 10;
    assert h(a,h(a,a)) == a;   // this should trigger
    return;
}

procedure V2(a: int, b: int)
{
  start:
    assume 0 <= h(a,h(a,10));
    assume a == 17;
    assert h(a,h(a,a)) == a;   // this should trigger
    return;
}

// ----------------------------------------------------------------------- negated triggers

function ka(ref) returns (int);
function kb(ref) returns (int);
function kbSynonym(ref) returns (int);
function isA(ref, name) returns (bool);
function isB(ref, name) returns (bool);
const $T: name;

axiom (forall o: ref ::
       isA(o, $T) ==> ka(o) < ka(o));  // automatically inferred triggers can be both isA(o,$T) and ka(o)

axiom (forall o: ref ::
       {:nopats isB(o, $T) }
       isB(o, $T) ==> kb(o) < kbSynonym(o));  // prevent isB(o,$T) from being used as a trigger

axiom (forall o: ref :: kb(o) == kbSynonym(o));

procedure W(o: ref, e: int)
  requires isB(o, $T);
{
  start:
    assert e > 20;  // the isB axiom should not trigger, so this cannot be proved
    return;
}

procedure X0(o: ref, e: int)
  requires isA(o, $T);
{
  start:
    assert e > 20;  // this should trigger the isA axiom, so anything is provable
    return;
}

procedure X1(o: ref, e: int, u: int)
  requires isB(o, $T);
{
  start:
    assume f(kb(o), kb(o)) == u;
    assert e > 20;  // this should now trigger the isB axiom, so anything is provable
    return;
}

procedure X2(o: ref, e: int, u: int)
  requires isB(o, $T);
{
  start:
    assert e > 20;  // error is report here, providing evidence that the isB axiom has not been triggered
    return;
}

type name, ref;