CristalCaveGem » LustreC » Lustrec-Tests

node Sofar( X : bool ) returns ( Y : bool );

let

  Y = (true -> pre Y) or X;

tel

node Store( Delta : int ) returns ( Total : int );

var Prev : int;

let

  Prev  = 0 -> pre Total;

  Total = if Delta < 0 or Prev > 0  then Prev+Delta

     else if Delta > 0 and Prev < 10 then Prev+Delta

     else Prev;

tel

--@ ensures OK;

node top( Delta : int ) returns ( OK : bool );

var Total : int;

let

  Total = Store( Delta );

  OK = Sofar( -1 <= Delta and Delta <= 1 ) => 0 <= Total and Total <= 20; 

  --%MAIN;

  --%PROPERTY  OK=true;

tel