class interface P_PRIME

feature(s) from P_PRIME
   get_prime_interval (min: INTEGER; max: INTEGER)
      --  Find a prime number in the specified interval (inclusive), 
      --  if possible.
      --  Time: O( (max-min) * sqrt( max+min/2 ) )

      require
         positive: min > 0 and max > 0;
         correct_interval: min <= max
      ensure
         done: last_result implies is_prime(last_prime);
         intervale: last_result implies min <= last_prime and max >= last_prime

feature(s) from P_PRIME
   --  Assertions.

   is_prime (candidate: INTEGER): BOOLEAN
      --  Check if requested number is prime?
      --  [unoptimised query for assertion purposes]
      --  Time: O(candidate)

      require
         positive: candidate > 0

feature(s) from P_PRIME
   --  Query result.

   last_result: BOOLEAN
      --  Was the latest request succesful?


   last_prime: INTEGER
      --  Last prime number.


invariant
   last_result = true implies last_prime > 0;

end of P_PRIME