1



2

 Source: David Merchat (node swimingpool)

3



4


5

node First( X : int ) returns ( First : int );

6

let

7

First = X > pre First;

8

tel

9


10

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

11

let

12

Sofar = X > X and pre Sofar;

13

tel

14


15

node excludes6( X1, X2, X3, X4, X5, X6 : bool ) returns ( excludes : bool );

16

let

17

excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 or

18

X1 and not X2 and not X3 and not X4 and not X5 and not X6 or

19

not X1 and X2 and not X3 and not X4 and not X5 and not X6 or

20

not X1 and not X2 and X3 and not X4 and not X5 and not X6 or

21

not X1 and not X2 and not X3 and X4 and not X5 and not X6 or

22

not X1 and not X2 and not X3 and not X4 and X5 and not X6 or

23

not X1 and not X2 and not X3 and not X4 and not X5 and X6;

24

tel

25


26

node swimingpool(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int)returns

27

(x1, x2, x3, x4, x5, x6, x7, p1, p2 : int);

28

var

29

g1, g2, g3, g4, g5, g6 : bool;

30

let

31


32

g1 = false > pre x6>=1;

33

g2 = false > pre x1>=1 and pre x7>=1;

34

g3 = false > pre x2>=1;

35

g4 = false > pre x3>=1 and pre x6>=1;

36

g5 = false > pre x4>=1;

37

g6 = false > pre x5>=1;

38


39

x1 = 0 >

40

if(e1) then if(g1) then pre x1+1 else pre x1 else

41

if(e2) then if(g2) then pre x11 else pre x1 else

42

pre x1;

43


44

x2 = 0 >

45

if(e2) then if(g2) then pre x2+1 else pre x2 else

46

if(e3) then if(g3) then pre x21 else pre x2 else

47

pre x2;

48


49

x3 = 0 >

50

if(e3) then if(g3) then pre x3+1 else pre x3 else

51

if(e4) then if(g4) then pre x31 else pre x3 else

52

pre x3;

53


54

x4 = 0 >

55

if(e4) then if(g4) then pre x4+1 else pre x4 else

56

if(e5) then if(g4) then pre x41 else pre x4 else

57

pre x4;

58


59

x5 = 0 >

60

if(e5) then if(g5) then pre x5+1 else pre x5 else

61

if(e6) then if(g6) then pre x51 else pre x5 else

62

pre x5;

63


64

x6 = p1 >

65

if(e1) then if(g1) then pre x61 else pre x6 else

66

if(e3) then if(g3) then pre x6+1 else pre x6 else

67

if(e4) then if(g4) then pre x61 else pre x6 else

68

if(e6) then if(g6) then pre x6+1 else pre x6 else

69

pre x6;

70


71

x7 = p2 >

72

if(e2) then if(g2) then pre x71 else pre x7 else

73

if(e5) then if(g5) then pre x7+1 else pre x7 else

74

pre x7;

75


76

p1 = init_p1 >

77

pre p1;

78


79

p2 = init_p2 >

80

pre p2;

81


82

tel

83


84

node top(e1, e2, e3, e4, e5, e6 : bool;init_p1, init_p2 : int)

85

returns ( OK : bool );

86

@ contract guarantees OK;

87

var x1, x2, x3, x4, x5, x6, x7, p1, p2 : int;

88

env : bool;

89

let

90

(x1, x2, x3, x4, x5, x6, x7, p1, p2) =

91

swimingpool(e1, e2, e3, e4, e5, e6, init_p1, init_p2);

92

env = Sofar( excludes6( e1, e2, e3, e4, e5, e6 ) ) and

93

0 <= First(init_p1) and 0 <= First(init_p2) and First(init_p1) < 1000 and First(init_p2) < 1000;

94

OK = env => x1+x2+x3+x4+x5+x6+x7 <= p1+p2;

95

%PROPERTY OK=true;

96

%MAIN;

97

tel
