blob: cf06e1f92ef4a52d466c096d3d6c9d07af455dbb (
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
|
procedure a, b, c := P(x, y, z)
requires 10
ensures 20
do
if 30 then else end;
if 31 then else end;
while x < z
invariant x <= z
invariant b.valid and 1
do
k := x + 1;
end;
(x+5).head := c.tail;
a := new (17, 18);
assert a != null;
m := k + a + null;
c := m;
call Q(x, y, y);
if x then
call a, c, b := P(a, b, c);
else
call R();
end;
end;
procedure Q(x, y, z)
requires 10
ensures 20
do
if 40 then else end;
end;
procedure R()
requires 10
ensures 20
do
end;
|