SOA
© 2004 SoS Group
All Rights Reserved

sos.koa
Class KiesKring

java.lang.Object
  extended bysos.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

SOA
© 2004 SoS Group
All Rights Reserved