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