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)

Class Specifications
invariant (* MAX_CANDIDATES_PER_KIESLIJST == 80 by law *); invariant 0 <= candidateCount()&&candidateCount() <= MAX_CANDIDATES_PER_KIESLIJST; invariant ( \forall int i; 0 <= i&&i < MY_CACHED_KIESLIJSTEN.length; MY_CACHED_KIESLIJSTEN[i].owner == MY_CACHED_KIESLIJSTEN); invariant my_candidates.length == MAX_CANDIDATES_PER_KIESLIJST+1; invariant ( \forall int i; 0 <= i&&i < my_candidates.length; my_candidates[i].owner == this); invariant 0 <= my_number&&my_number <= KiesKring.MAX_KIESLIJSTEN_PER_KIESKRING; invariant my_name.length() <= GROEPERING_NAME_MAX_LENGTH; invariant my_name.owner == this; invariant 0 <= my_kieskring_number; invariant my_kieskring_number <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST; invariant 0 <= my_candidate_count; invariant my_candidate_count <= MAX_CANDIDATES_PER_KIESLIJST; invariant my_vote_count >= 0;

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

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

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

### GROEPERING_NAME_MAX_LENGTH

    static final byte GROEPERING_NAME_MAX_LENGTH

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

### MAX_CANDIDATES_PER_KIESLIJST

    static final byte MAX_CANDIDATES_PER_KIESLIJST

### 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)`
  Specifications: spec_public non_null

### my_candidates

    final Candidate[] my_candidates

  The candidates in this kieslijst.

  Specifications: spec_public non_null

### my_number

    private byte my_number

  This number (kieslijstnummer) of this kieslijst.

  Specifications: spec_public

### my_name

    private java.lang.String my_name

  The name (kieslijstnaam) of this kieslijst.

  Specifications: spec_public non_null

### my_kieskring_number

    private byte my_kieskring_number

  The number of the kieskring in which this kieslijst resides.

  Specifications: spec_public

### my_candidate_count

    private byte my_candidate_count

  The number of candidates in this kieslijst.

  Specifications: spec_public

### my_vote_count

    private int my_vote_count

  The total number of votes counted in this kieslijst.

  Specifications: spec_public

Constructor Detail

### KiesLijst

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

  Construct a new kieslijst object given the specified initialization values.

  See Also:
    `

    `
  Specifications:
    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;
    assignable 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,
                          non_null 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.
  Specifications: pure
    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;
    ensures \result .number() == a_number;
    ensures \result .name().equals(a_name);
    ensures \result .candidateCount() >= 0;
    ensures MY_CACHED_KIESLIJSTEN[a_kieskring_number*KiesKring.MAX_KIESLIJSTEN_PER_KIESKRING+a_number] != null;

### number

    byte number()

  Returns:
    the number of this kieslijst.

  Specifications: pure
    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.

  Specifications: pure non_null
    normal_behavior
    ensures \result .length() <= GROEPERING_NAME_MAX_LENGTH;
    ensures \result == my_name;

### addCandidate

    void addCandidate(non_null Candidate a_candidate)

  Add a candidate to this kieslijst.

  Parameters:
    `a_candidate` - the candidate to add.

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

  Specifications: pure non_null
    normal_behavior
    ensures \result == my_candidates;

### candidateCount

    byte candidateCount()

  Returns:
    the number of candidates in this kieslijst.

  Specifications: pure
    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.

  Specifications:
    normal_behavior
    assignable my_vote_count;
    ensures my_vote_count == \old(my_vote_count+1);

### voteCount

    int voteCount()

  Returns:
    the number of votes counted in this kieslijst.

  Specifications: pure
    normal_behavior
    ensures \result == my_vote_count;

### clear

    void clear()

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

  Specifications:
    normal_behavior
    assignable 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)

  {@inheritDoc}

  Overrides:
    `equals` in class `java.lang.Object`

### hashCode

    public int hashCode()

  {@inheritDoc}

  Overrides:
    `hashCode` in class `java.lang.Object`

### toString

    public java.lang.String toString()

  {@inheritDoc}

  Overrides:
    `toString` in class `java.lang.Object`

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