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

@ contract guarantees OK;

23

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
