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)

Class Specifications
invariant ( \forall int i; 0 <= i&&i < MY_CACHED_KIESKRINGEN.length; MY_CACHED_KIESKRINGEN[i].owner == MY_CACHED_KIESKRINGEN);
invariant my_kiesLijsten.length == MAX_KIESLIJSTEN_PER_KIESKRING+1;
invariant my_kiesLijsten.owner == this;
invariant ( \forall int i; 0 <= i&&i < my_kiesLijsten.length; my_kiesLijsten[i].owner == this);
invariant 0 <= my_number;
invariant my_number <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;
invariant my_name.length() <= KIESKRING_NAME_MAX_LENGTH;
invariant my_name.owner == this;
invariant my_districts.length == MAX_DISTRICTS_PER_KIESKRING+1;
invariant my_districts.owner == this;
invariant ( \forall int i; 0 <= i&&i < my_districts.length; my_districts[i].owner == this);
invariant 0 <= my_district_count&&my_district_count <= MAX_DISTRICTS_PER_KIESKRING;
invariant my_district_count == ( \sum int i; 0 <= i&&i < my_districts.length; (my_districts[i] != null) ? 1 : 0);
invariant 0 <= my_kieslijst_count&&my_kieslijst_count <= MAX_KIESLIJSTEN_PER_KIESKRING;
invariant my_kieslijst_count == ( \sum int i; 0 <= i&&i < my_kiesLijsten.length; (my_kiesLijsten[i] != null) ? 1 : 0);

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.
[spec_public] private static KiesKring[] MY_CACHED_KIESKRINGEN
          A cache of all kieskringen that have been constructed thus far.
[spec_public] private  byte my_district_count
          The number of districts in this kieskring.
[spec_public] private  District[] my_districts
          The districts of this kieskring.
[spec_public] private  byte my_kieslijst_count
          The number of kieslijsten in this kieskring.
[spec_public] (package private)  KiesLijst[] my_kiesLijsten
          A list of all kieslijst in this kieskring, indexed on kieslijst number.
[spec_public] private  java.lang.String my_name
          The name (kieskringnaam) of this kieskring.
[spec_public] private  byte my_number
          The number (kieskringnummer) of this kieskring.
 
Constructor Summary
private KiesKring(byte a_kieskring_number, non_null java.lang.String a_kieskring_name)
          Construct a new kieskring object given the specified initialization values.
 
Method Summary
(package private)  boolean addDistrict(non_null District a_district)
          Add a district to this kieskring.
(package private)  boolean addKiesLijst(non_null 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)
          {@inheritDoc}
(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(non_null District a_district)
           
 int hashCode()
          {@inheritDoc}
(package private)  boolean hasKiesLijst(non_null KiesLijst a_kieslijst)
           
(package private)  byte kieslijstCount()
           
(package private) static KiesKring make(byte a_kieskring_number, non_null 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()
          {@inheritDoc}
 
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.


KIESKRING_NAME_MAX_LENGTH

static final byte KIESKRING_NAME_MAX_LENGTH
The maximum length, in characters, of the name of a kieskring.


MAX_DISTRICTS_PER_KIESKRING

static final int MAX_DISTRICTS_PER_KIESKRING
The maximum number of districts that can exist in a single kieskring.


MAX_KIESLIJSTEN_PER_KIESKRING

static final byte MAX_KIESLIJSTEN_PER_KIESKRING
The maximum number of kieslijsten that can exist in a single kieskring.


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

Specifications: spec_public non_null

my_kiesLijsten

final KiesLijst[] my_kiesLijsten
A list of all kieslijst in this kieskring, indexed on kieslijst number.

Specifications: spec_public non_null

my_number

private byte my_number
The number (kieskringnummer) of this kieskring.

Specifications: spec_public

my_name

private java.lang.String my_name
The name (kieskringnaam) of this kieskring.

Specifications: spec_public non_null

my_districts

private final District[] my_districts
The districts of this kieskring.

Specifications: spec_public non_null

my_district_count

private byte my_district_count
The number of districts in this kieskring.

Specifications: spec_public

my_kieslijst_count

private byte my_kieslijst_count
The number of kieslijsten in this kieskring.

Specifications: spec_public
Constructor Detail

KiesKring

private KiesKring(byte a_kieskring_number,
                  non_null 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.
Specifications: pure
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,
                      non_null 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.
Specifications: non_null
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;
assignable \everything;
ensures \result .number() == a_kieskring_number;
ensures \result .name().equals(a_kieskring_name);

number

byte number()
Returns:
the number of this kieskring.
Specifications: pure
normal_behavior
ensures 0 <= \result &&\result <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;

name

java.lang.String name()
Returns:
the name of this kieskring.
Specifications: pure non_null
normal_behavior
ensures \result .length() <= KIESKRING_NAME_MAX_LENGTH;

addDistrict

boolean addDistrict(non_null 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.
Specifications:
normal_behavior
requires !hasDistrict(a_district);
assignable objectState;
assignable 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);
assignable \nothing;
ensures !\result ;

getDistricten

District[] getDistricten()
Returns:
the districts of this kieskring.
Specifications: pure
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.
Specifications: pure
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(non_null District a_district)
Parameters:
a_district - the district to check for.
Returns:
a flag indicating if this kieskring contains the specified district.
Specifications: pure
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.
Specifications: pure
normal_behavior
ensures \result == my_district_count;
    implies_that
ensures \result >= 0;

addKiesLijst

boolean addKiesLijst(non_null 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.
Specifications:
normal_behavior
requires hasKiesLijst(a_kieslijst);
requires (* a_kieslijst.number() !?= KiesLijst.BLANCO; *);
assignable \nothing;
ensures !\result ;
     also
normal_behavior
requires !hasKiesLijst(a_kieslijst);
requires (* a_kieslijst.number() !?= KiesLijst.BLANCO; *);
assignable objectState;
assignable 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.
Specifications: pure
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.
Specifications: pure
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(non_null 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.
Specifications: pure
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.
Specifications: pure
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.

Specifications:
normal_behavior
assignable objectState;
assignable 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)
{@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

SOA
© 2004 SoS Group
All Rights Reserved