blob: 89634552b211d361176c74b01911f5dcc3ec0e4b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
procedure {:checksum "0"} M(n: int);
implementation {:id "M"} {:checksum "1"} M(n: int)
{
var x: int;
call x := N(n);
assert 0 <= x;
}
procedure {:checksum "2"} N(n: int) returns (r: int);
requires 0 < n;
ensures 0 < r;
|