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 else 0;

9 


tel

10 


node top (k0: int; p, q, r, t : bool) returns (OK: bool);

11 
2d37a1e1

ploc

@ contract guarantees OK;

12 
b8dc00eb

bourbouh

var k: int;

13 


env : bool;

14 


let

15 


k = k0> pre(k);

16 


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

17 


OK = env => ((Age(p and r)>=k) => (q and t));

18 


%MAIN;

19 


%PROPERTY OK=true;

20 


tel
