Package components.random

Interface Random

All Known Implementing Classes:

Random1L

public interface Random

Random component with all its methods. (Note: by package-wide convention, all references are non-null.)

A Random is modeled by an infinite string of real numbers in the [0..1) interval that satisfies appropriate statistical tests of randomness.

There is only one no-argument constructor.

Mathematical Subtypes:

BOUNDED_REAL is real
 exemplar x
 constraint
  0.0 <= x < 1.0

Mathematical Model (abstract value and abstract invariant of this):

type Random is modeled by infinite string of BOUNDED_REAL

Constructor(s) (initial abstract value(s) of this):

():
 ensures
  [this satisfies appropriate statistical tests of randomness]

Method Summary

Modifier and Type	Method	Description
double	nextDouble()	Returns the first real in this.
int	nextInt()	Returns an integer in the [Integer.MIN_VALUE,Integer.MAX_VALUE] interval computed from the first double in this.

Method Details

nextDouble

double nextDouble()

Returns the first real in this.

Returns:

the first real in this

Updates:

this

Ensures:

#this = <nextDouble> * this

nextInt

int nextInt()

Returns an integer in the [Integer.MIN_VALUE,Integer.MAX_VALUE] interval computed from the first double in this.

Returns:

an integer in the [Integer.MIN_VALUE,Integer.MAX_VALUE] interval computed from the first double in this

Updates:

this

Ensures:

there exists x: real
 (#this = <x> * this and
  nextInt =
   floor((Integer.MAX_VALUE - Integer.MIN_VALUE + 1) * x) + Integer.MIN_VALUE