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)

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

Constructor Detail

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

Method Detail

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

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