1 
b8dc00eb

bourbouh



2 


 Source: Bertrand Jeannet

3 




4 



5 


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

6 


let

7 


Sofar = X > X and pre Sofar;

8 


tel

9 



10 



11 


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

12 


 how long has p been maintained true in the strict past

13 


let

14 


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

15 


tel

16 



17 


 Theorem 1:

18 


 (p k> q and q m> r) => p k+m> r

19 



20 


 Not provable in luke*

21 


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

22 
2d37a1e1

ploc

@ contract guarantees OK;

23 
b8dc00eb

bourbouh

var k,m : int;

24 


env : bool;

25 


let

26 


k = ik > pre k;

27 


m = im > pre m;

28 


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

29 


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

30 


%PROPERTY OK=true;

31 


%MAIN;

32 


tel
