sos.koa
Class CandidateList

java.lang.Object
  sos.koa.CandidateList

All Implemented Interfaces:

java.io.Serializable

class CandidateList

extends java.lang.Object

implements java.io.Serializable

The CandidateList stores all of the information embodied in the XML-based candidate list files provided by the KOA application.

Version:

$Id: CandidateList.java,v 1.36 2004/05/18 12:44:54 hubbers Exp $

Author:

Joe Kiniry (kiniry@cs.kun.nl)

Field Summary

(package private) static byte	MAX_KIESKRINGEN_PER_CANDIDATE_LIST The maximum number of kieskringen that can exist in a candidate list.
private byte	my_blanco_count The number of "blanco" candidates contained in this candidate list.
private java.util.Map	my_candidate_codes The candidate codes of this candidate list.
(package private) java.util.SortedMap	my_kieskringen The kieskringen contained in this candidate list.
(package private) CandidateListMetadata	my_metadata The metadata associated with this candidate list.

Constructor Summary

(package private)

CandidateList(java.lang.String a_request_reference, java.lang.String a_response_reference, java.lang.String a_creation_time, java.lang.String a_kieskring_count, java.lang.String a_district_count, java.lang.String a_kieslijst_count, java.lang.String a_positie_count, java.lang.String a_code_count) Construct a new candidate list object given the specified initialization values.

Method Summary

(package private) Candidate	addCandidate(KiesKring a_kieskring, KiesLijst a_kieslijst, java.lang.String a_position_number, java.lang.String a_lastname, java.lang.String some_initials, java.lang.String a_firstname, java.lang.String a_gender, java.lang.String a_city_of_residence) Add the specified candidate to this candidate list.
(package private) boolean	addCandidateCode(Candidate a_candidate, java.lang.String a_candidate_code) Adds the specified candidiate code, bound to the specified candidate, to this candidate list.
(package private) District	addDistrict(KiesKring a_kieskring, int a_district_number, java.lang.String a_name) Add the specified district, contained in a specific kieskring, to this candidate list.
(package private) KiesKring	addKiesKring(byte a_kieskring_number, java.lang.String a_name) Add the specified kieskring to this candidate list.
(package private) KiesLijst	addKiesLijst(KiesKring a_kieskring, byte a_kieslijst_number, java.lang.String a_groepering_name) Add the specified kieslijst, contained in a specific kieskring, to this candidate list.
(package private) byte	blancoCount()
(package private) byte	candidatesPerParty(KiesLijst a_kieslijst)
(package private) void	clear() Clears all data in this CandidateList instance.
(package private) Candidate	getCandidate(int a_candidate_code)
(package private) Candidate	getCandidate(java.lang.String a_candidate_code)
(package private) CandidateListMetadata	metadata()
(package private) byte	totalPartyCount()
(package private) boolean	validCandidate(int a_candidate_code)
(package private) boolean	validCandidate(java.lang.String a_candidate_code)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

MAX_KIESKRINGEN_PER_CANDIDATE_LIST

static final byte MAX_KIESKRINGEN_PER_CANDIDATE_LIST

The maximum number of kieskringen that can exist in a candidate list. This maximum is implicit in the fact that a kieskring's number is at most two digits and non-negative.

See Also:

Constant Field Values

my_kieskringen

java.util.SortedMap my_kieskringen

The kieskringen contained in this candidate list. These kieskringen are arranged in a sorted map so that they can be interated over by number.

my_metadata

CandidateListMetadata my_metadata

The metadata associated with this candidate list.

my_candidate_codes

private java.util.Map my_candidate_codes

The candidate codes of this candidate list. Each candidate has one or more unique codes in the candidate list. Typically each candidate will have 1000 codes.

my_blanco_count

private byte my_blanco_count

The number of "blanco" candidates contained in this candidate list.

Constructor Detail

CandidateList

CandidateList(java.lang.String a_request_reference,
              java.lang.String a_response_reference,
              java.lang.String a_creation_time,
              java.lang.String a_kieskring_count,
              java.lang.String a_district_count,
              java.lang.String a_kieslijst_count,
              java.lang.String a_positie_count,
              java.lang.String a_code_count)

Construct a new candidate list object given the specified initialization values.

Parameters:

a_request_reference - the request reference of the associated candidate list.

a_response_reference - the response reference of the associated candidate list.

a_creation_time - the creation time of the associated candidate list.

a_kieskring_count - the number of kieskringen in the associated candidate list.

a_district_count - the number of districts in the associated candidate list.

a_kieslijst_count - the number of kieslijsten in the associated candidate list.

a_positie_count - the total number of candidates in the associated candidate list.

a_code_count - the number of candidate codes contained in the associated candidate list.

See Also:

 normal_behavior
   requires Byte.parseByte(a_kieskring_count) >= 0;
   requires Integer.parseInt(a_district_count) >= 0;
   requires Integer.parseInt(a_kieslijst_count) >= 0;
   requires Integer.parseInt(a_positie_count) >= 0;
   requires Integer.parseInt(a_code_count) >= 0;
   modifies objectState;
   ensures metadata().requestReference().equals(a_request_reference);
   ensures metadata().responseReference().equals(a_response_reference);
   ensures metadata().creationTime().equals(a_creation_time);
   ensures metadata().kiesKringCount() == Byte.parseByte(a_kieskring_count);
   ensures metadata().districtCount() == Integer.parseInt(a_district_count);
   ensures metadata().positieCount() == Integer.parseInt(a_positie_count);
   ensures metadata().codeCount() == Integer.parseInt(a_code_count);
 

Method Detail

addKiesKring

final KiesKring addKiesKring(byte a_kieskring_number,
                             java.lang.String a_name)

Add the specified kieskring to this candidate list.

Parameters:

a_kieskring_number - the number of the kieskring to add.

a_name - the name of the kieskring to add.

Returns:

the newly added kieskring.

See Also:

 normal_behavior
   requires (* all parameters must be of the proper length *);
   requires 0 <= a_kieskring_number;
   requires a_kieskring_number <= MAX_KIESKRINGEN_PER_CANDIDATE_LIST;
   requires a_name.length() <= KiesKring.KIESKRING_NAME_MAX_LENGTH;
   modifies \everything;
   ensures (* all fields are properly initialized *);
   ensures \result.number() == a_kieskring_number;
   ensures \result.name().equals(a_name);
 

addDistrict

final District addDistrict(KiesKring a_kieskring,
                           int a_district_number,
                           java.lang.String a_name)

Add the specified district, contained in a specific kieskring, to this candidate list.

Parameters:

a_kieskring - the kieskring in which the district being added resides.

a_district_number - the number of the district to add.

a_name - the name of the district to add.

Returns:

the newly added district.

See Also:

sos.koa.District#District(sos.koa.KiesKring, int, java.lang.String)

addKiesLijst

final KiesLijst addKiesLijst(KiesKring a_kieskring,
                             byte a_kieslijst_number,
                             java.lang.String a_groepering_name)

Add the specified kieslijst, contained in a specific kieskring, to this candidate list.

Parameters:

a_kieskring - the kieskring in which the district being added resides.

a_kieslijst_number - the number of the kieslijst to add.

a_groepering_name - the name of the groupering to add.

Returns:

the newly added kieslijst.

See Also:

 normal_behavior
   requires 0 <= a_kieslijst_number;
   requires a_kieslijst_number <= KiesKring.MAX_KIESLIJSTEN_PER_KIESKRING;
   requires a_groepering_name.length() <= KiesLijst.GROEPERING_NAME_MAX_LENGTH;
   requires a_kieskring.hasKiesLijst(KiesLijst.make(a_kieskring.number(), a_kieslijst_number, a_groepering_name));
   modifies \nothing;
   ensures \result.equals(KiesLijst.make(a_kieskring.number(), a_kieslijst_number, a_groepering_name));
 also
 normal_behavior
   requires !a_kieskring.hasKiesLijst(KiesLijst.make(a_kieskring.number(), a_kieslijst_number, a_groepering_name));
   modifies a_kieskring.my_kiesLijsten[a_kieslijst_number];
   ensures a_kieskring.hasKiesLijst(KiesLijst.make(a_kieskring.number(), a_kieslijst_number, a_groepering_name));
   ensures a_kieskring.kieslijstCount() == \old(a_kieskring.kieslijstCount() + 1);
   ensures \result.equals(KiesLijst.make(a_kieskring.number(), a_kieslijst_number, a_groepering_name));
 

addCandidate

final Candidate addCandidate(KiesKring a_kieskring,
                             KiesLijst a_kieslijst,
                             java.lang.String a_position_number,
                             java.lang.String a_lastname,
                             java.lang.String some_initials,
                             java.lang.String a_firstname,
                             java.lang.String a_gender,
                             java.lang.String a_city_of_residence)

Add the specified candidate to this candidate list.

Parameters:

a_kieskring - the kieskring to which the candidate belongs.

a_kieslijst - the kieslijst to which the candidate belongs.

a_position_number - the position number of the candidate.

a_lastname - the lastname of the new candidate.

a_firstname - the firstname of the new candidate.

some_initials - the initial of the new candidate.

a_gender - the gender of the new candidate.

a_city_of_residence - the city of residence of the new candidate.

Returns:

the newly added candidate.

 normal_behavior
   requires (* all parameters must be of the proper length *);
   requires a_lastname.length() <= Candidate.LASTNAME_MAX_LENGTH;
   requires a_firstname.length() <= Candidate.FIRSTNAME_MAX_LENGTH;
   requires some_initials.length() <= Candidate.INITIALS_MAX_LENGTH;
   requires a_gender.length() == 1;
   requires a_gender.charAt(0) == Candidate.MALE || a_gender.charAt(0) == Candidate.FEMALE || a_gender.charAt(0) == Candidate.UNKNOWN;
   requires 0 <= Byte.parseByte(a_position_number);
   requires Byte.parseByte(a_position_number) <= KiesLijst.MAX_CANDIDATES_PER_KIESLIJST;
   modifies \nothing;
   ensures (* all fields are properly initialized *);
   ensures \result.lastname().equals(a_lastname);
   ensures \result.firstname().equals(a_firstname);
   ensures \result.initials().equals(some_initials);
   ensures \result.gender() == a_gender.charAt(0);
   ensures \result.position_number() == Byte.parseByte(a_position_number);
   ensures \result.cityOfResidence().equals(a_city_of_residence);
   ensures \result.kiesKring().equals(a_kieskring);
   ensures \result.kiesLijst().equals(a_kieslijst);
 also
 normal_behavior
   requires (* Is the position of 1 REQUIRED? -JRK *);
   requires a_kieslijst.number() == KiesLijst.BLANCO;
   requires Byte.parseByte(a_position_number) == 1;
   modifies my_blanco_count;
   ensures my_blanco_count == \old(my_blanco_count + 1);
 

addCandidateCode

final boolean addCandidateCode(Candidate a_candidate,
                               java.lang.String a_candidate_code)

Adds the specified candidiate code, bound to the specified candidate, to this candidate list.

Parameters:

a_candidate - the candidate to which we bind the candidate code.

a_candidate_code - the candidate code to bind to the candidate.

Returns:

a flag indicating if the specified candidate code previously had a candidate associated with it.

 normal_behavior
   requires 0 <= Integer.parseInt(a_candidate_code);
   modifies my_candidate_codes.objectState;
   ensures \result <==> (\old(getCandidate(a_candidate_code) == null));
 

getCandidate

final Candidate getCandidate(java.lang.String a_candidate_code)

Parameters:

a_candidate_code - the candidate code we are interested in.

Returns:

the candidate in this candidate list associated with the specified candidate code.

 normal_behavior
   requires 0 <= Integer.parseInt(a_candidate_code);
   requires validCandidate(a_candidate_code);
   ensures \result == my_candidate_codes.get(a_candidate_code);
 

validCandidate

final boolean validCandidate(java.lang.String a_candidate_code)

Parameters:

a_candidate_code - the candidate code we are interested in.

Returns:

a flag indicating if the specified candidate code is a valid candidate code for this candidate list. That is to say, the specified code is associated with a candidate in this candidate list.

 normal_behavior
   requires 0 <= Integer.parseInt(a_candidate_code);
   ensures \result == my_candidate_codes.containsKey(a_candidate_code);
 

getCandidate

final Candidate getCandidate(int a_candidate_code)

Parameters:

a_candidate_code - the candidate code we are interested in.

Returns:

the candidate in this candidate list associated with the specified candidate code.

 normal_behavior
   requires 0 <= a_candidate_code;
   requires validCandidate(a_candidate_code);
   ensures \result == my_candidate_codes.get(new Integer(a_candidate_code));
 

validCandidate

final boolean validCandidate(int a_candidate_code)

Parameters:

a_candidate_code - the candidate code we are interested in.

Returns:

a flag indicating if the specified candidate code is a valid candidate code for this candidate list. That is to say, the specified code is associated with a candidate in this candidate list.

 normal_behavior
   requires 0 <= a_candidate_code;
   ensures \result == my_candidate_codes.containsKey(new Integer(a_candidate_code));
 

metadata

final CandidateListMetadata metadata()

Returns:

the metadata associated with this candidate list.

 normal_behavior
   ensures \result == my_metadata;
 

candidatesPerParty

final byte candidatesPerParty(KiesLijst a_kieslijst)

Parameters:

a_kieslijst - the kieslijst (party) that we are interested in.

Returns:

the number of candidates in the specified kieslijst (party).

 normal_behavior
   ensures 0 <= \result;
 

totalPartyCount

final byte totalPartyCount()

Returns:

the total number of kieslijsten (parties) contained in this candidate list.

 normal_behavior
   ensures 0 <= \result && \result <= KiesKring.MAX_KIESLIJSTEN_PER_KIESKRING;
 also
 normal_behavior
   requires (* if there are more than MAX_KIESLIJSTEN_PER_KIESKRING kieslijsten in any kieskring *);
   ensures (* false *);
 

blancoCount

final byte blancoCount()

Returns:

the total number of "blanco" kieslijsten contained in this candidate list.

See Also:

 normal_behavior
   ensures 0 <= \result;
   ensures \result == my_blanco_count;
 

clear

final void clear()

Clears all data in this CandidateList instance. In particular, all kieskring references are cleared.

 normal_behavior
   modifies objectState;

   ensures my_kieskringen == null;
   ensures my_candidate_codes == null;
   ensures my_metadata == null;
   ensures my_blanco_count == 0;

   ensures_redundantly (\forall int i; getCandidate(i) == null);
   ensures_redundantly (\forall int i; !validCandidate(i));
   ensures_redundantly (\forall KiesLijst kl; candidatesPerParty(kl) == 0);
   ensures_redundantly (* totalPartyCount() == 0; *);
   ensures_redundantly metadata() == null;
   ensures_redundantly blancoCount() == 0;