class interface P_RANDOM
creation
make (seed: INTEGER)
-- Initialise pseudo-random machine from seed.
feature(s) from P_RANDOM
-- Initialisation
make (seed: INTEGER)
-- Initialise pseudo-random machine from seed.
feature(s) from P_RANDOM
-- Initialisation
reset (seed: INTEGER)
-- Initialise pseudo-random machine from seed.
feature(s) from P_RANDOM
-- Random number
get_number (min_range, max_range: INTEGER)
-- Get a new random integer inside specified range.
require
positive: min_range >= 0;
in_order: min_range < max_range
ensure
inside: last_number >= min_range and last_number <= max_range; -- last_number set
done:
last_number: INTEGER
-- Last result.
end of P_RANDOM