1 
0cbf0839

ploc


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 
3e36d4e0

ploc

@ ensures OK;

15 
0cbf0839

ploc

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

16 


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
