|
1
|
types
|
|
2
|
MyInt = int [2..100];
|
|
3
|
LengthInt = int [0..40];
|
|
4
|
Primes = autocons system
|
|
5
|
|[
|
|
6
|
var
|
|
7
|
initialized : bool = false ;
|
|
8
|
primes : list [ 40 ] of MyInt = [3]
|
|
9
|
actions
|
|
10
|
obs init = requires initialized = false :
|
|
11
|
primes := [ x | var x: MyInt & (forall tmp : MyInt :
|
|
12
|
(tmp < x => (x mod tmp <> 0 ))) ] ;
|
|
13
|
initialized := true end;
|
|
14
|
|
|
15
|
obs Prime(a: MyInt) =
|
|
16
|
requires (exists i : LengthInt : (primes[i] = a)) :
|
|
17
|
skip
|
|
18
|
end
|
|
19
|
|
|
20
|
do
|
|
21
|
init() // var A : MyInt : Prime(A)
|
|
22
|
od
|
|
23
|
]|
|
|
24
|
system
|
|
25
|
Primes
|
|
26
|
|