Interface RandomWithParity

All Known Implementing Classes:

AlternatingCoin, UnfilteredRandom

public interface RandomWithParity

Generates a new number within specified bounds with every call. The number generated is always non-negative. The parity of the number generated changes with every invocation. That is, the first request for a number results in an even number, the second request results in an odd number, and so on.

Mathematical Model (abstract field):

history is a sequence of natural numbers.

Constraint (abstract invariant):

(forall i : 0 <= i < |history| : history[i] is even <==> i is even)

Initial State (ensured by constructor):

history is empty

Author:

paolo

Method Summary

int	generateNumber(int upperBound) Generates a natural number (ie >=0) within the specified bound.

Method Detail

generateNumber

int generateNumber(int upperBound)

Generates a natural number (ie >=0) within the specified bound. The returned value is guaranteed to be less than or equal to the bound. Since the bound must be >= 1, there are always at least two possible return values (0 and 1). In addition, the method alternates the parity of the generated number. The first time it is called it returns an even number, the next time an odd number, and so on, back and forth.

Parameters:

upperBound - the maximum value that can be generated by this call

Requires (precondition):

upperBound >= 1

Alters (modification frame):

history

Ensures (postcondition):

history = #history + generateNumber
generateNumber is even <==> |#history| is even

Returns:

0 <= generateNumber <= upperBound