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)

Class Specifications

invariant (* MAX_CANDIDATES_PER_KIESLIJST == 80 by law *); invariant 0 <= candidateCount()&&candidateCount() <= MAX_CANDIDATES_PER_KIESLIJST; invariant ( \forall int i; 0 <= i&&i < MY_CACHED_KIESLIJSTEN.length; MY_CACHED_KIESLIJSTEN[i].owner == MY_CACHED_KIESLIJSTEN); invariant my_candidates.length == MAX_CANDIDATES_PER_KIESLIJST+1; invariant ( \forall int i; 0 <= i&&i < my_candidates.length; my_candidates[i].owner == this); invariant 0 <= my_number&&my_number <= KiesKring.MAX_KIESLIJSTEN_PER_KIESKRING; invariant my_name.length() <= GROEPERING_NAME_MAX_LENGTH; invariant my_name.owner == this; invariant 0 <= my_kieskring_number; invariant my_kieskring_number <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST; invariant 0 <= my_candidate_count; invariant my_candidate_count <= MAX_CANDIDATES_PER_KIESLIJST; invariant my_vote_count >= 0;

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
[spec_public] private static KiesLijst[]	MY_CACHED_KIESLIJSTEN           A cache of all kieslijsts ever constructed.
[spec_public] private  byte	my_candidate_count           The number of candidates in this kieslijst.
[spec_public] (package private)  Candidate[]	my_candidates           The candidates in this kieslijst.
[spec_public] private  byte	my_kieskring_number           The number of the kieskring in which this kieslijst resides.
[spec_public] private  java.lang.String	my_name           The name (kieslijstnaam) of this kieslijst.
[spec_public] private  byte	my_number           This number (kieslijstnummer) of this kieslijst.
[spec_public] 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, non_null java.lang.String a_name)           Construct a new kieslijst object given the specified initialization values.

 

Method Summary
(package private)  void	addCandidate(non_null 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)           {@inheritDoc}
int	hashCode()           {@inheritDoc}
(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, non_null 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()           {@inheritDoc}
(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.

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).

GROEPERING_NAME_MAX_LENGTH

static final byte GROEPERING_NAME_MAX_LENGTH

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

MAX_CANDIDATES_PER_KIESLIJST

static final byte MAX_CANDIDATES_PER_KIESLIJST

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)

Specifications: spec_public non_null

my_candidates

final Candidate[] my_candidates

The candidates in this kieslijst.

Specifications: spec_public non_null

my_number

private byte my_number

This number (kieslijstnummer) of this kieslijst.

Specifications: spec_public

my_name

private java.lang.String my_name

The name (kieslijstnaam) of this kieslijst.

Specifications: spec_public non_null

my_kieskring_number

private byte my_kieskring_number

The number of the kieskring in which this kieslijst resides.

Specifications: spec_public

my_candidate_count

private byte my_candidate_count

The number of candidates in this kieslijst.

Specifications: spec_public

my_vote_count

private int my_vote_count

The total number of votes counted in this kieslijst.

Specifications: spec_public

KiesLijst

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

Construct a new kieslijst object given the specified initialization values.

See Also:

Specifications:

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;
assignable objectState;
ensures number() == a_number;
ensures name().equals(a_name);
ensures candidateCount() == 0;
ensures my_kieskring_number == a_kieskring_number;

make

static KiesLijst make(byte a_kieskring_number,
                      byte a_number,
                      non_null 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.

Specifications: pure

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;
ensures \result .number() == a_number;
ensures \result .name().equals(a_name);
ensures \result .candidateCount() >= 0;
ensures MY_CACHED_KIESLIJSTEN[a_kieskring_number*KiesKring.MAX_KIESLIJSTEN_PER_KIESKRING+a_number] != null;

number

byte number()

Returns:

the number of this kieslijst.

Specifications: pure

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.

Specifications: pure non_null

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

addCandidate

void addCandidate(non_null Candidate a_candidate)

Add a candidate to this kieslijst.

Parameters:

a_candidate - the candidate to add.

Specifications:

normal_behavior
requires candidateCount() < KiesLijst.MAX_CANDIDATES_PER_KIESLIJST;
assignable \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.

Specifications: pure non_null

normal_behavior
ensures \result == my_candidates;

candidateCount

byte candidateCount()

Returns:

the number of candidates in this kieslijst.

Specifications: pure

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.

Specifications:

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

voteCount

int voteCount()

Returns:

the number of votes counted in this kieslijst.

Specifications: pure

normal_behavior
ensures \result == my_vote_count;

clear

void clear()

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

Specifications:

normal_behavior
assignable 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)

{@inheritDoc}

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

{@inheritDoc}

Overrides:

hashCode in class java.lang.Object

toString

public java.lang.String toString()

{@inheritDoc}

Overrides:

toString in class java.lang.Object

compareTo

public int compareTo(java.lang.Object an_object)

Specified by:

compareTo in interface java.lang.Comparable