root/branches/compiler/cSharp/ooasCompiler/doc/examples/Primes.ooas
| 3 | krennw | types
|
|
MyInt = int [2..100];
|
|||
LengthInt = int [0..40];
|
|||
Primes = autocons system
|
|||
|[
|
|||
var
|
|||
initialized : bool = false ;
|
|||
primes : list [ 40 ] of MyInt = [3]
|
|||
actions
|
|||
obs init = requires initialized = false :
|
|||
primes := [ x | var x: MyInt & (forall tmp : MyInt :
|
|||
(tmp < x => (x mod tmp <> 0 ))) ] ;
|
|||
initialized := true end;
|
|||
obs Prime(a: MyInt) =
|
|||
requires (exists i : LengthInt : (primes[i] = a)) :
|
|||
skip
|
|||
end
|
|||
do
|
|||
init() // var A : MyInt : Prime(A)
|
|||
od
|
|||
]|
|
|||
system
|
|||
Primes
|