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 KiesKring

    java.lang.Object
      sos.koa.KiesKring

All Implemented Interfaces:
  java.lang.Comparable, java.io.Serializable

final class KiesKring
extends java.lang.Object
implements java.lang.Comparable, java.io.Serializable

A kieskring in an election.

Version:
  $Id: KiesKring.java,v 1.31 2004/05/16 20:37:39 kiniry Exp $
Author:
  Joe Kiniry (kiniry@cs.kun.nl)

Field Summary
`(package private) static byte` | `KIESKRING_NAME_MAX_LENGTH` The maximum length, in characters, of the name of a kieskring.
`(package private) static byte` | `KIESKRING_NUMBER_MAX_LENGTH` The maximum length, in digits represented by characters, of the number of a kieskring.
`(package private) static int` | `MAX_DISTRICTS_PER_KIESKRING` The maximum number of districts that can exist in a single kieskring.
`(package private) static byte` | `MAX_KIESLIJSTEN_PER_KIESKRING` The maximum number of kieslijsten that can exist in a single kieskring.
`private static KiesKring[]` | `MY_CACHED_KIESKRINGEN` A cache of all kieskringen that have been constructed thus far.
`private byte` | `my_district_count` The number of districts in this kieskring.
`private District[]` | `my_districts` The districts of this kieskring.
`private byte` | `my_kieslijst_count` The number of kieslijsten in this kieskring.
`(package private) KiesLijst[]` | `my_kiesLijsten` A list of all kieslijst in this kieskring, indexed on kieslijst number.
`private java.lang.String` | `my_name` The name (kieskringnaam) of this kieskring.
`private byte` | `my_number` The number (kieskringnummer) of this kieskring.

Constructor Summary
`private` | `KiesKring(byte a_kieskring_number, java.lang.String a_kieskring_name)` Construct a new kieskring object given the specified initialization values.

Method Summary
`(package private) boolean` | `addDistrict(District a_district)` Add a district to this kieskring.
`(package private) boolean` | `addKiesLijst(KiesLijst a_kieslijst)` Adds the specified kieslijst to this kieskring.
`(package private) void` | `clear()` Clears all data in this `KiesKring` instance.
`int` | `compareTo(java.lang.Object an_object)`
`(package private) byte` | `districtCount()`
`boolean` | `equals(java.lang.Object an_object)`
`(package private) District` | `getDistrict(byte a_district_number)`
`(package private) District[]` | `getDistricten()`
`(package private) KiesLijst` | `getKiesLijst(byte a_kieslijst_number)`
`(package private) KiesLijst[]` | `getKiesLijsten()`
`(package private) boolean` | `hasDistrict(District a_district)`
`int` | `hashCode()`
`(package private) boolean` | `hasKiesLijst(KiesLijst a_kieslijst)`
`(package private) byte` | `kieslijstCount()`
`(package private) static KiesKring` | `make(byte a_kieskring_number, java.lang.String a_kieskring_name)` A factory method used to construct new kieskring objects.
`(package private) java.lang.String` | `name()`
`(package private) byte` | `number()`
`java.lang.String` | `toString()`

Methods inherited from class java.lang.Object
`clone, finalize, getClass, notify, notifyAll, wait, wait, wait`

Field Detail

### KIESKRING_NUMBER_MAX_LENGTH

    static final byte KIESKRING_NUMBER_MAX_LENGTH

  The maximum length, in digits represented by characters, of the number of a kieskring.

  See Also:
    Constant Field Values

### KIESKRING_NAME_MAX_LENGTH

    static final byte KIESKRING_NAME_MAX_LENGTH

  The maximum length, in characters, of the name of a kieskring.

  See Also:
    Constant Field Values

### MAX_DISTRICTS_PER_KIESKRING

    static final int MAX_DISTRICTS_PER_KIESKRING

  The maximum number of districts that can exist in a single kieskring.

  See Also:
    Constant Field Values

### MAX_KIESLIJSTEN_PER_KIESKRING

    static final byte MAX_KIESLIJSTEN_PER_KIESKRING

  The maximum number of kieslijsten that can exist in a single kieskring.

  See Also:
    Constant Field Values

### MY_CACHED_KIESKRINGEN

    private static final KiesKring[] MY_CACHED_KIESKRINGEN

  A cache of all kieskringen that have been constructed thus far. This cache is used by the factory method `make(byte, java.lang.String)`.

### my_kiesLijsten

    final KiesLijst[] my_kiesLijsten

  A list of all kieslijst in this kieskring, indexed on kieslijst number.

### my_number

    private byte my_number

  The number (kieskringnummer) of this kieskring.

### my_name

    private java.lang.String my_name

  The name (kieskringnaam) of this kieskring.

### my_districts

    private final District[] my_districts

  The districts of this kieskring.

### my_district_count

    private byte my_district_count

  The number of districts in this kieskring.

### my_kieslijst_count

    private byte my_kieslijst_count

  The number of kieslijsten in this kieskring.

Constructor Detail

### KiesKring

    private KiesKring(byte a_kieskring_number,
                      java.lang.String a_kieskring_name)

  Construct a new kieskring object given the specified initialization values.

  This method is private and not to be used by clients. Instead, the factory method `make(byte, java.lang.String)` should be used.

Parameters:
  `a_kieskring_number` - the number of the new kieskring.
  `a_kieskring_name` - the name of the new kieskring.

       private normal_behavior
         requires 0 <= a_kieskring_number;
         requires a_kieskring_number <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;
         requires a_kieskring_name.length() <= KIESKRING_NAME_MAX_LENGTH;
         ensures number() == a_kieskring_number;
         ensures name().equals(a_kieskring_name);

Method Detail

### make

    static KiesKring make(byte a_kieskring_number,
                          java.lang.String a_kieskring_name)

  A factory method used to construct new kieskring objects.

  Parameters:
    `a_kieskring_number` - the number of the new kieskring.
    `a_kieskring_name` - the name of the new kieskring.
  Returns:
    the new kieskring.

         normal_behavior
           requires 0 <= a_kieskring_number;
           requires a_kieskring_number <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;
           requires a_kieskring_name.length() <= KIESKRING_NAME_MAX_LENGTH;
           modifies \everything;
           ensures \result.number() == a_kieskring_number;
           ensures \result.name().equals(a_kieskring_name);

### number

    byte number()

  Returns:
    the number of this kieskring.

         normal_behavior
           ensures 0 <= \result && \result <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;

### name

    java.lang.String name()

  Returns:
    the name of this kieskring.

         normal_behavior
           ensures \result.length() <= KIESKRING_NAME_MAX_LENGTH;

### addDistrict

    boolean addDistrict(District a_district)

  Add a district to this kieskring.

  Parameters:
    `a_district` - the district to add.
  Returns:
    `false` if this kieskring already contained the given district; `true` if otherwise.

         normal_behavior
           requires !hasDistrict(a_district);
           modifies objectState;
           modifies a_district.owner;
           ensures hasDistrict(a_district);
           ensures \result <==> !\old(hasDistrict(a_district));
           ensures districtCount() == \old(districtCount() + 1);
         also
         normal_behavior
           requires hasDistrict(a_district);
           modifies \nothing;
           ensures !\result;

### getDistricten

    District[] getDistricten()

  Returns:
    the districts of this kieskring.

         normal_behavior
           requires true;
           ensures \result == my_districts;
           ensures districtCount() == \old(districtCount());

### getDistrict

    District getDistrict(byte a_district_number)

  Parameters:
    `a_district_number` - the number of the district to get.
  Returns:
    the district in this kieskring with the given number. A `null` is returned if no such district exists.

         normal_behavior
           requires 0 <= a_district_number && a_district_number <= MAX_DISTRICTS_PER_KIESKRING;
           ensures \result == my_districts[a_district_number];
           ensures districtCount() == \old(districtCount());

### hasDistrict

    boolean hasDistrict(District a_district)

  Parameters:
    `a_district` - the district to check for.
  Returns:
    a flag indicating if this kieskring contains the specified district.

         normal_behavior
           ensures \result <==> (my_districts[a_district.number()] != null) &&
                                (my_districts[a_district.number()].equals(a_district));
           ensures districtCount() == \old(districtCount());

### districtCount

    byte districtCount()

  Returns:
    the number of districts in this kieskring.

         normal_behavior
           ensures \result == my_district_count;
           implies_that
           ensures \result >= 0;

### addKiesLijst

    boolean addKiesLijst(KiesLijst a_kieslijst)

  Adds the specified kieslijst to this kieskring.

  Parameters:
    `a_kieslijst` - the kieslijst to add.
  Returns:
    a flag indicating if the specified kieslijst was already in this kieskring.

         normal_behavior
           requires hasKiesLijst(a_kieslijst);
           requires (* a_kieslijst.number() !?= KiesLijst.BLANCO; *);
           modifies \nothing;
           ensures !\result;
         also
         normal_behavior
           requires !hasKiesLijst(a_kieslijst);
           requires (* a_kieslijst.number() !?= KiesLijst.BLANCO; *);
           modifies objectState;
           modifies a_kieslijst.owner;
           ensures hasKiesLijst(a_kieslijst);
           ensures kieslijstCount() == \old(kieslijstCount() + 1);
           ensures \result;

### getKiesLijsten

    KiesLijst[] getKiesLijsten()

  Returns:
    the kieslijsten that have been added to this kieskring.

         normal_behavior
           requires true;
           ensures \result == my_kiesLijsten;
           ensures kieslijstCount() == \old(kieslijstCount());

### getKiesLijst

    KiesLijst getKiesLijst(byte a_kieslijst_number)

  Parameters:
    `a_kieslijst_number` - the number of the kieslijst that we are interested in.
  Returns:
    the kieslijst represented by the specified kieslijst number.

         normal_behavior
           requires 0 <= a_kieslijst_number;
           requires a_kieslijst_number <= MAX_KIESLIJSTEN_PER_KIESKRING;
           ensures \result == my_kiesLijsten[a_kieslijst_number];
           ensures kieslijstCount() == \old(kieslijstCount());

### hasKiesLijst

    boolean hasKiesLijst(KiesLijst a_kieslijst)

  Parameters:
    `a_kieslijst` - the kieslijst that we wish to check for.
  Returns:
    a flag indicating if this kieskring contains the specified kieslijst.

         normal_behavior
           ensures \result <==> (my_kiesLijsten[a_kieslijst.number()] != null) &&
                                (my_kiesLijsten[a_kieslijst.number()].equals(a_kieslijst));
           ensures kieslijstCount() == \old(kieslijstCount());

### kieslijstCount

    byte kieslijstCount()

  Returns:
    the number of kieslijsten contained in this kieskring.

         normal_behavior
           ensures \result == my_kieslijst_count;
           implies_that
           ensures \result >= 0;

### clear

    void clear()

  Clears all data in this `KiesKring` instance. In particular, all district and kieslijsten references are cleared.

       normal_behavior
         modifies objectState;
         modifies MY_CACHED_KIESKRINGEN[*];

         ensures my_number == 0;
         ensures my_name == "";
         ensures my_district_count == 0;
         ensures my_kieslijst_count == 0;

         ensures (\forall int i; i < my_districts.length; my_districts[i] == null);
         ensures (\forall int i; i < my_kiesLijsten.length; my_kiesLijsten[i] == null);
         ensures (\forall int i; i < MY_CACHED_KIESKRINGEN.length;
                                 MY_CACHED_KIESKRINGEN[i] == null);

         ensures_redundantly number() == 0;
         ensures_redundantly name() == "";
         ensures_redundantly districtCount() == 0;
         ensures_redundantly kieslijstCount() == 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