001package components.random;
002
003/**
004 * Random component with all its methods. (Note: by package-wide convention, all
005 * references are non-null.) <br/>
006 * <br/>
007 * A Random is modeled by an infinite string of real numbers in the [0..1)
008 * interval that satisfies appropriate statistical tests of randomness. <br/>
009 * <br/>
010 * There is only one no-argument constructor.
011 *
012 * @mathsubtypes {@code
013 * BOUNDED_REAL is real
014 *  exemplar x
015 *  constraint
016 *   0.0 <= x < 1.0
017 * }
018 * @mathmodel type Random is modeled by infinite string of BOUNDED_REAL
019 * @initially <pre>
020 * ():
021 *  ensures
022 *   [this satisfies appropriate statistical tests of randomness]
023 * </pre>
024 */
025public interface Random {
026
027    /**
028     * Returns the first real in {@code this}.
029     *
030     * @return the first real in {@code this}
031     * @updates this
032     * @ensures {@code #this = <nextDouble> * this}
033     */
034    double nextDouble();
035
036    /**
037     * Returns an integer in the [Integer.MIN_VALUE,Integer.MAX_VALUE] interval
038     * computed from the first double in {@code this}.
039     *
040     * @return an integer in the [Integer.MIN_VALUE,Integer.MAX_VALUE] interval
041     *         computed from the first double in {@code this}
042     * @updates this
043     * @ensures {@code
044     * there exists x: real
045     *  (#this = <x> * this and
046     *   nextInt =
047     *    floor((Integer.MAX_VALUE - Integer.MIN_VALUE + 1) * x) + Integer.MIN_VALUE
048     * }
049     */
050    int nextInt();
051
052}