CristalCaveGem » LustreC » Lustrec-Tests

node count (in: bool) returns (cpt: int) ;

let

  cpt = (if in then 1 else 0) + (0 -> pre cpt) ;

tel

node sub (in: bool) returns (cpt: int) ;

  mode begin (

    require count(true) <= 10 ;

    ensure  cpt >= 0 ;

  ) ;

  mode and_then (

  ) ;

*)

let

  cpt = count(in) ;

tel

node top (in: bool) returns (cpt: int) ;

  -- guarantees "sub" (count(true) > 15) => false ;

  guarantee (count(true) > 15) => false ;

let

  cpt = sub(in) ;