OoasTools

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