1 | package(load_event_b_project([event_b_model(none, | |
2 | 'Sieve', | |
3 | [sees(none, | |
4 | ['SieveContext']), | |
5 | variables(none, | |
6 | [identifier(none, | |
7 | cur), | |
8 | identifier(none, | |
9 | numbers)]), | |
10 | invariant(none, | |
11 | [subset(none, | |
12 | identifier(none, | |
13 | numbers), | |
14 | natural_set(none)), | |
15 | member(none, | |
16 | identifier(none, | |
17 | cur), | |
18 | natural1_set(none))]), | |
19 | theorems(none, | |
20 | []), | |
21 | events(none, | |
22 | [event(none, | |
23 | 'INITIALISATION', | |
24 | [], | |
25 | [], | |
26 | [], | |
27 | [assign(none, | |
28 | [identifier(none, | |
29 | numbers)], | |
30 | [interval(none, | |
31 | integer(none, | |
32 | 2), | |
33 | identifier(none, | |
34 | mx))]), | |
35 | assign(none, | |
36 | [identifier(none, | |
37 | cur)], | |
38 | [integer(none, | |
39 | 2)])], | |
40 | []), | |
41 | event(none, | |
42 | treat_prime, | |
43 | [], | |
44 | [], | |
45 | [member(none, | |
46 | identifier(none, | |
47 | cur), | |
48 | identifier(none, | |
49 | numbers)), | |
50 | less_equal(none, | |
51 | multiplication(none, | |
52 | identifier(none, | |
53 | cur), | |
54 | identifier(none, | |
55 | cur)), | |
56 | identifier(none, | |
57 | mx))], | |
58 | [assign(none, | |
59 | [identifier(none, | |
60 | cur)], | |
61 | [add(none, | |
62 | identifier(none, | |
63 | cur), | |
64 | integer(none, | |
65 | 1))]), | |
66 | assign(none, | |
67 | [identifier(none, | |
68 | numbers)], | |
69 | [set_subtraction(none, | |
70 | identifier(none, | |
71 | numbers), | |
72 | range(none, | |
73 | event_b_comprehension_set(none, | |
74 | [identifier(none, | |
75 | n)], | |
76 | couple(none, | |
77 | [identifier(none, | |
78 | n), | |
79 | multiplication(none, | |
80 | identifier(none, | |
81 | n), | |
82 | identifier(none, | |
83 | cur))]), | |
84 | member(none, | |
85 | identifier(none, | |
86 | n), | |
87 | interval(none, | |
88 | integer(none, | |
89 | 2), | |
90 | div(none, | |
91 | identifier(none, | |
92 | mx), | |
93 | identifier(none, | |
94 | cur)))))))])], | |
95 | []), | |
96 | event(none, | |
97 | treat_composite, | |
98 | [], | |
99 | [], | |
100 | [less_equal(none, | |
101 | multiplication(none, | |
102 | identifier(none, | |
103 | cur), | |
104 | identifier(none, | |
105 | cur)), | |
106 | identifier(none, | |
107 | mx)), | |
108 | not_member(none, | |
109 | identifier(none, | |
110 | cur), | |
111 | identifier(none, | |
112 | numbers))], | |
113 | [assign(none, | |
114 | [identifier(none, | |
115 | cur)], | |
116 | [add(none, | |
117 | identifier(none, | |
118 | cur), | |
119 | integer(none, | |
120 | 1))])], | |
121 | []), | |
122 | event(none, | |
123 | finished, | |
124 | [], | |
125 | [identifier(none, | |
126 | npr)], | |
127 | [greater(none, | |
128 | multiplication(none, | |
129 | identifier(none, | |
130 | cur), | |
131 | identifier(none, | |
132 | cur)), | |
133 | identifier(none, | |
134 | mx)), | |
135 | equal(none, | |
136 | identifier(none, | |
137 | npr), | |
138 | card(none, | |
139 | identifier(none, | |
140 | numbers)))], | |
141 | [], | |
142 | [])])])], | |
143 | [event_b_context(none, | |
144 | 'SieveContext', | |
145 | [extends(none, | |
146 | []), | |
147 | constants(none, | |
148 | [identifier(none, | |
149 | mx)]), | |
150 | axioms(none, | |
151 | [equal(none, | |
152 | identifier(none, | |
153 | mx), | |
154 | integer(none, | |
155 | 1000))]), | |
156 | theorems(none, | |
157 | []), | |
158 | sets(none, | |
159 | [])])], | |
160 | _Error)). |