1
|
node count (in: bool) returns (cpt: int) ;
|
2
|
let
|
3
|
cpt = (if in then 1 else 0) + (0 -> pre cpt) ;
|
4
|
tel
|
5
|
|
6
|
node sub (in: bool) returns (cpt: int) ;
|
7
|
(*@ --contract
|
8
|
assume true -> in = not pre in ;
|
9
|
mode begin (
|
10
|
require count(true) <= 10 ;
|
11
|
ensure cpt >= 0 ;
|
12
|
) ;
|
13
|
mode and_then (
|
14
|
require not ::begin ;
|
15
|
ensure true ;
|
16
|
) ;
|
17
|
*)
|
18
|
let
|
19
|
cpt = count(in) ;
|
20
|
tel
|
21
|
|
22
|
node top (in: bool) returns (cpt: int) ;
|
23
|
(*@ --contract
|
24
|
assume true -> in = not pre in ;
|
25
|
-- guarantees "sub" cpt >= 0 ;
|
26
|
-- guarantees "sub" (count(true) > 15) => false ;
|
27
|
guarantees cpt >= 0 ;
|
28
|
guarantees (count(true) > 15) => false ;
|
29
|
*)
|
30
|
let
|
31
|
cpt = sub(in) ;
|
32
|
tel
|