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

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

Method Summary
`(package private) void` | `addCandidate(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)`
`int` | `hashCode()`
`(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, 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()`
`(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.

  See Also:
    Constant Field Values

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

  See Also:
    Constant Field Values

### GROEPERING_NAME_MAX_LENGTH

    static final byte GROEPERING_NAME_MAX_LENGTH

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

  See Also:
    Constant Field Values

### MAX_CANDIDATES_PER_KIESLIJST

    static final byte MAX_CANDIDATES_PER_KIESLIJST

  The maximum number of candidates per kieslijst, by law.

  See Also:
    Constant Field Values

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

### my_candidates

    final Candidate[] my_candidates

  The candidates in this kieslijst.

### my_number

    private byte my_number

  This number (kieslijstnummer) of this kieslijst.

### my_name

    private java.lang.String my_name

  The name (kieslijstnaam) of this kieslijst.

### my_kieskring_number

    private byte my_kieskring_number

  The number of the kieskring in which this kieslijst resides.

### my_candidate_count

    private byte my_candidate_count

  The number of candidates in this kieslijst.

### my_vote_count

    private int my_vote_count

  The total number of votes counted in this kieslijst.

Constructor Detail

### KiesLijst

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

  Construct a new kieslijst object given the specified initialization values.

See Also:
  `

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

  `

Method Detail

### make

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

### number

    byte number()

  Returns:
    the number of this kieslijst.

         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.

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

### addCandidate

    void addCandidate(Candidate a_candidate)

  Add a candidate to this kieslijst.

  Parameters:
    `a_candidate` - the candidate to add.

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

         normal_behavior
           ensures \result == my_candidates;

### candidateCount

    byte candidateCount()

  Returns:
    the number of candidates in this kieslijst.

         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.

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

### voteCount

    int voteCount()

  Returns:
    the number of votes counted in this kieslijst.

         normal_behavior
           ensures \result == my_vote_count;

### clear

    void clear()

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

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

### hashCode

    public int hashCode()

### toString

    public java.lang.String toString()

### compareTo

    public int compareTo(java.lang.Object an_object)

  Specified by:
    `compareTo` in interface `java.lang.Comparable`

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