1 
b8dc00eb

bourbouh


2 


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

3 


let

4 


Sofar = X > X and pre Sofar;

5 


tel

6 


node Age (p: bool) returns (age_of_p: int);

7 


let

8 


age_of_p = 0 > if pre(p) then pre(age_of_p) +1+ 1 else 0;

9 


tel

10 


node top (ik, im: int; p, q, r : bool) returns (OK: bool);

11 
2d37a1e1

ploc

@ contract guarantees OK;

12 
b8dc00eb

bourbouh

var k,m : int;

13 


env : bool;

14 


let

15 


k = ik > pre k;

16 


m = im > pre m;

17 


env = Sofar((k>=1 and m>=1) and (Age(p)>=k => q) and (Age(q)>=m => r));

18 


OK = env => (true > ( (Age(p)>=k+m) => r ));

19 


%MAIN;

20 


%PROPERTY OK=true;

21 


tel
