1 
b8dc00eb

bourbouh


2 


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

3 


let

4 


Y = (true > pre Y) or X;

5 


tel

6 


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

7 


var Prev : int;

8 


let

9 


Prev = 0 > pre Total;

10 


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

11 


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

12 


else Prev;

13 


tel

14 


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

15 
2d37a1e1

ploc

@ contract guarantees OK;

16 
b8dc00eb

bourbouh

var Total : int;

17 


let

18 


Total = Store( Delta );

19 


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

20 


%MAIN;

21 


%PROPERTY OK=true;

22 


tel
