blob: df8bbcbbe14b83f9c5e3142ac5a826883b0407fd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
var g: int;
procedure {:checksum "0"} P();
requires g == 0;
modifies g;
implementation {:id "P"} {:checksum "1"} P()
{
call Q();
assert 0 < g;
}
procedure {:checksum "2"} Q();
modifies g;
ensures old(g) < g;
|