blob: e1c505f86fbddc6f625f99a487b7daefca9a3473 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
procedure {:checksum "-1"} Foo(b: bool);
implementation {:id "Foo"} {:checksum "2"} Foo(b: bool)
{
var r: int;
assert b;
call r := Sum(42);
assert r != 0;
assert r == (42 * 43) div 2;
}
procedure {:checksum "1"} Sum(n: int) returns (r: int);
requires 0 <= n;
ensures n <= r;
|