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 (k0, m0: int; p, q : bool) returns (OK: bool);

11 
2d37a1e1

ploc

@ contract guarantees OK;

12 
b8dc00eb

bourbouh

var k,m: int;

13 


env : bool;

14 


let

15 


k = k0> pre(k);

16 


m = m0> pre(m);

17 


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

18 


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

19 


%MAIN;

20 


%PROPERTY OK=true;

21 


tel
