Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (639 Bytes)

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
  guarantee cpt >= 0 ;
28
  guarantee (count(true) > 15) => false ;
29
*)
30
let
31
  cpt = sub(in) ;
32
tel