1



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

18

 (p k> q and r k> t) => (p and r) k> (q and t)

19


20

 Not provable in luke*

21

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

22

@ contract guarantees OK;

23

var k: int;

24

env : bool;

25

let

26

k = k0> pre(k);

27

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

28

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

29

%PROPERTY OK=true;

30

%MAIN;

31

tel
