Overview | Package | Class | Tree | Deprecated | Index | Help
| SOA © 2004 SoS Group All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## 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;

Overview | Package | Class | Tree | Deprecated | Index | Help
| SOA © 2004 SoS Group All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD