Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / tests / cocospec / refinement.lus @ 6ccfcb12

History | View | Annotate | Download (639 Bytes)

1 c3af3032 Bourbouh
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 5dfe059d ploc
(*@ --contract
8 c3af3032 Bourbouh
  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 5dfe059d ploc
(*@ --contract
24 c3af3032 Bourbouh
  assume true -> in = not pre in ;
25 5dfe059d ploc
  -- guarantees "sub" cpt >= 0 ;
26
  -- guarantees "sub" (count(true) > 15) => false ;
27 bd3f748f ploc
  guarantee cpt >= 0 ;
28
  guarantee (count(true) > 15) => false ;
29 c3af3032 Bourbouh
*)
30
let
31
  cpt = sub(in) ;
32 bd3f748f ploc
tel