blob: da9058679c823906d62813c828d2d560cf884d50 (
plain) (
blame)
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
|
node test(i: int) returns (a, b, probe c: int; exit: bool)
var
la, lb: int;
half: bool;
let
exit = i >= 20;
half = true -> not pre half;
la = 0 -> pre a;
lb = 0 -> pre b;
activate
if half then
let
a = la + 1;
b = lb;
tel
else
let
a = la;
b = lb + 1;
tel
returns a, b;
c = a - b;
guarantee c_bounded: c >= 0 and c <= 1;
guarantee link_c_half: (half and c = 1) or ((not half) and c = 0);
tel
|
