sos.koa
Class KiesLijst

java.lang.Object
  sos.koa.KiesLijst

All Implemented Interfaces:

java.lang.Comparable, java.io.Serializable

final class KiesLijst

extends java.lang.Object

implements java.lang.Comparable, java.io.Serializable

A kieslijst in an election.

Version:

$Id: KiesLijst.java,v 1.29 2004/05/16 20:37:39 kiniry Exp $

Author:

Joe Kiniry (kiniry@cs.kun.nl)

Field Summary

(package private) static byte	BLANCO The "Blanco" kieslijst is hard-coded, according to the Ministry, as 99.
(package private) static byte	GROEPERING_NAME_MAX_LENGTH The maximum length in characters of a groepering's name.
(package private) static byte	KIESLIJST_NUMBER_MAX_LENGTH The maximum length, in digits represented by characters, of a kieslijst's number (kieslijstnummer).
(package private) static byte	MAX_CANDIDATES_PER_KIESLIJST The maximum number of candidates per kieslijst, by law.
private static KiesLijst[]	MY_CACHED_KIESLIJSTEN A cache of all kieslijsts ever constructed.
private byte	my_candidate_count The number of candidates in this kieslijst.
(package private) Candidate[]	my_candidates The candidates in this kieslijst.
private byte	my_kieskring_number The number of the kieskring in which this kieslijst resides.
private java.lang.String	my_name The name (kieslijstnaam) of this kieslijst.
private byte	my_number This number (kieslijstnummer) of this kieslijst.
private int	my_vote_count The total number of votes counted in this kieslijst.

Constructor Summary

private

KiesLijst(byte a_kieskring_number, byte a_number, java.lang.String a_name) Construct a new kieslijst object given the specified initialization values.

Method Summary

(package private) void	addCandidate(Candidate a_candidate) Add a candidate to this kieslijst.
(package private) byte	candidateCount()
(package private) Candidate[]	candidates()
(package private) void	clear() Clears all data in this KiesLijst instance.
int	compareTo(java.lang.Object an_object)
boolean	equals(java.lang.Object an_object)
int	hashCode()
(package private) int	incrementVoteCount() Increment the number of votes counted in this kieslijst by one.
(package private) static KiesLijst	make(byte a_kieskring_number, byte a_number, java.lang.String a_name) This is the factory method for obtaining new kieslijst objects, given the specified initialization values.
(package private) java.lang.String	name()
(package private) byte	number()
java.lang.String	toString()
(package private) int	voteCount()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

BLANCO

static final byte BLANCO

The "Blanco" kieslijst is hard-coded, according to the Ministry, as 99.

See Also:

Constant Field Values

KIESLIJST_NUMBER_MAX_LENGTH

static final byte KIESLIJST_NUMBER_MAX_LENGTH

The maximum length, in digits represented by characters, of a kieslijst's number (kieslijstnummer).

See Also:

Constant Field Values

GROEPERING_NAME_MAX_LENGTH

static final byte GROEPERING_NAME_MAX_LENGTH

The maximum length in characters of a groepering's name.

See Also:

Constant Field Values

MAX_CANDIDATES_PER_KIESLIJST

static final byte MAX_CANDIDATES_PER_KIESLIJST

The maximum number of candidates per kieslijst, by law.

See Also:

Constant Field Values

MY_CACHED_KIESLIJSTEN

private static final KiesLijst[] MY_CACHED_KIESLIJSTEN

A cache of all kieslijsts ever constructed. This cache is used by the factory method make().

See Also:

make(byte, byte, java.lang.String)

my_candidates

final Candidate[] my_candidates

The candidates in this kieslijst.

my_number

private byte my_number

This number (kieslijstnummer) of this kieslijst.

my_name

private java.lang.String my_name

The name (kieslijstnaam) of this kieslijst.

my_kieskring_number

private byte my_kieskring_number

The number of the kieskring in which this kieslijst resides.

my_candidate_count

private byte my_candidate_count

The number of candidates in this kieslijst.

my_vote_count

private int my_vote_count

The total number of votes counted in this kieslijst.

Constructor Detail

KiesLijst

private KiesLijst(byte a_kieskring_number,
                  byte a_number,
                  java.lang.String a_name)

Construct a new kieslijst object given the specified initialization values.

See Also:

 private normal_behavior
   requires 0 <= a_kieskring_number;
   requires a_kieskring_number <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;
   requires 0 <= a_number && a_number <= KiesKring.MAX_KIESLIJSTEN_PER_KIESKRING;
   requires a_name.length() <= GROEPERING_NAME_MAX_LENGTH;
   modifies objectState;
   ensures number() == a_number;
   ensures name().equals(a_name);
   ensures candidateCount() == 0;
   ensures my_kieskring_number == a_kieskring_number;
 

Method Detail

make

static KiesLijst make(byte a_kieskring_number,
                      byte a_number,
                      java.lang.String a_name)

This is the factory method for obtaining new kieslijst objects, given the specified initialization values.

Parameters:

a_kieskring_number - the number of the kieskring in which this kieslijst resides.

a_number - the number of the new kieslijst.

a_name - the name of the new kieslijst.

Returns:

the kieslijst that represents the specified values.

number

byte number()

Returns:

the number of this kieslijst.

 normal_behavior
   ensures 0 <= \result && \result <= KiesKring.MAX_KIESLIJSTEN_PER_KIESKRING;
   ensures \result == my_number;
 

name

java.lang.String name()

Returns:

the name of this kieslijst.

 normal_behavior
   ensures \result.length() <= GROEPERING_NAME_MAX_LENGTH;
   ensures \result == my_name;
 

addCandidate

void addCandidate(Candidate a_candidate)

Add a candidate to this kieslijst.

Parameters:

a_candidate - the candidate to add.

 normal_behavior
   requires candidateCount() < KiesLijst.MAX_CANDIDATES_PER_KIESLIJST;
   modifies \everything;
   ensures candidates()[\old(a_candidate.position_number())] == a_candidate;
   ensures candidateCount() == \old(candidateCount() + 1);
   ensures candidateCount() <= KiesLijst.MAX_CANDIDATES_PER_KIESLIJST;
 

candidates

Candidate[] candidates()

Returns:

the candidates of this kieslijst.

 normal_behavior
   ensures \result == my_candidates;
 

candidateCount

byte candidateCount()

Returns:

the number of candidates in this kieslijst.

 normal_behavior
   ensures 0 <= \result && \result <= KiesLijst.MAX_CANDIDATES_PER_KIESLIJST;
   ensures \result == my_candidate_count;
 

incrementVoteCount

int incrementVoteCount()

Increment the number of votes counted in this kieslijst by one.

Returns:

the total number of votes, including the one just added.

 normal_behavior
   modifies my_vote_count;
   ensures my_vote_count == \old(my_vote_count + 1);
 

voteCount

int voteCount()

Returns:

the number of votes counted in this kieslijst.

 normal_behavior
   ensures \result == my_vote_count;
 

clear

void clear()

Clears all data in this KiesLijst instance. In particular, all candidate references are cleared.

 normal_behavior
   modifies objectState;

   ensures my_number == 0;
   ensures my_name.equals("");
   ensures my_kieskring_number == 0;
   ensures my_candidate_count == 0;
   ensures my_vote_count == 0;

   ensures (\forall int i; i < my_candidates.length; my_candidates[i] == null);
   ensures (\forall int i; i < MY_CACHED_KIESLIJSTEN.length;
                           MY_CACHED_KIESLIJSTEN[i] == null);

   ensures_redundantly number() == 0;
   ensures_redundantly name().equals("");
   ensures_redundantly voteCount() == 0;
   ensures_redundantly candidateCount() == 0;
 

equals

public boolean equals(java.lang.Object an_object)

hashCode

public int hashCode()

toString

public java.lang.String toString()

compareTo

public int compareTo(java.lang.Object an_object)

Specified by:

compareTo in interface java.lang.Comparable