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)

Class Specifications

invariant my_kieskringen.size() <= MAX_KIESKRINGEN_PER_CANDIDATE_LIST; invariant my_kieskringen.owner == this; invariant my_metadata.owner == this; invariant my_candidate_codes.owner == this; invariant 0 <= my_blanco_count; invariant ( \forall int i; ; getCandidate(i) == getCandidate(Integer.toString(i))); invariant ( \forall int i; ; validCandidate(i) == validCandidate(Integer.toString(i)));

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

 

Constructor Summary

(package private)

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

 

Method Summary
(package private)  Candidate	addCandidate(non_null KiesKring a_kieskring, non_null KiesLijst a_kieslijst, non_null java.lang.String a_position_number, non_null java.lang.String a_lastname, non_null java.lang.String some_initials, non_null java.lang.String a_firstname, non_null java.lang.String a_gender, non_null java.lang.String a_city_of_residence)           Add the specified candidate to this candidate list.
(package private)  boolean	addCandidateCode(non_null Candidate a_candidate, non_null java.lang.String a_candidate_code)           Adds the specified candidiate code, bound to the specified candidate, to this candidate list.
(package private)  District	addDistrict(non_null KiesKring a_kieskring, int a_district_number, non_null 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, non_null java.lang.String a_name)           Add the specified kieskring to this candidate list.
(package private)  KiesLijst	addKiesLijst(non_null KiesKring a_kieskring, byte a_kieslijst_number, non_null 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(non_null 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(non_null 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(non_null 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.

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.

Specifications: spec_public non_null

my_metadata

CandidateListMetadata my_metadata

The metadata associated with this candidate list.

Specifications: spec_public non_null

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.

Specifications: spec_public non_null

my_blanco_count

private byte my_blanco_count

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

Specifications: spec_public

CandidateList

CandidateList(non_null java.lang.String a_request_reference,
              non_null java.lang.String a_response_reference,
              non_null java.lang.String a_creation_time,
              non_null java.lang.String a_kieskring_count,
              non_null java.lang.String a_district_count,
              non_null java.lang.String a_kieslijst_count,
              non_null java.lang.String a_positie_count,
              non_null 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:

Specifications: pure

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

addKiesKring

final KiesKring addKiesKring(byte a_kieskring_number,
                             non_null 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:

Specifications: non_null

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;
assignable \everything;
ensures (* all fields are properly initialized *);
ensures \result .number() == a_kieskring_number;
ensures \result .name().equals(a_name);

addDistrict

final District addDistrict(non_null KiesKring a_kieskring,
                           int a_district_number,
                           non_null 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)

Specifications: non_null

normal_behavior
requires 0 <= a_district_number;
requires a_district_number <= KiesKring.MAX_DISTRICTS_PER_KIESKRING;
requires a_name.length() <= District.DISTRICT_NAME_MAX_LENGTH;
assignable a_kieskring.objectState;
ensures a_kieskring.hasDistrict(\result );
ensures \result .number() == a_district_number;
ensures \result .name().equals(a_name);

addKiesLijst

final KiesLijst addKiesLijst(non_null KiesKring a_kieskring,
                             byte a_kieslijst_number,
                             non_null 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:

Specifications: non_null

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));
assignable \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));
assignable 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(non_null KiesKring a_kieskring,
                             non_null KiesLijst a_kieslijst,
                             non_null java.lang.String a_position_number,
                             non_null java.lang.String a_lastname,
                             non_null java.lang.String some_initials,
                             non_null java.lang.String a_firstname,
                             non_null java.lang.String a_gender,
                             non_null 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.

Specifications: non_null

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;
assignable \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;
assignable my_blanco_count;
ensures my_blanco_count == \old(my_blanco_count+1);

addCandidateCode

final boolean addCandidateCode(non_null Candidate a_candidate,
                               non_null 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.

Specifications:

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

getCandidate

final Candidate getCandidate(non_null 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.

Specifications: pure non_null

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(non_null 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.

Specifications: pure

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.

Specifications: pure non_null

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.

Specifications: pure

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.

Specifications: pure non_null

normal_behavior
ensures \result == my_metadata;

candidatesPerParty

final byte candidatesPerParty(non_null KiesLijst a_kieslijst)

Parameters:

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

Returns:

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

Specifications: pure

normal_behavior
ensures 0 <= \result ;

totalPartyCount

final byte totalPartyCount()

Returns:

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

Specifications: pure

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:

Specifications: pure

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.

Specifications:

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