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)

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

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

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