|
SOA © 2004 SoS Group All Rights Reserved |
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object sos.koa.KiesKring
A kieskring in an election.
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 |
static final byte KIESKRING_NUMBER_MAX_LENGTH
static final byte KIESKRING_NAME_MAX_LENGTH
static final int MAX_DISTRICTS_PER_KIESKRING
static final byte MAX_KIESLIJSTEN_PER_KIESKRING
private static final KiesKring[] MY_CACHED_KIESKRINGEN
make(byte,
java.lang.String)
.
final KiesLijst[] my_kiesLijsten
private byte my_number
private java.lang.String my_name
private final District[] my_districts
private byte my_district_count
private byte my_kieslijst_count
Constructor Detail |
private KiesKring(byte a_kieskring_number, java.lang.String a_kieskring_name)
This method is private and not to be used by clients.
Instead, the factory method make(byte, java.lang.String)
should be used.
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 |
static KiesKring make(byte a_kieskring_number, java.lang.String a_kieskring_name)
a_kieskring_number
- the number of the new kieskring.a_kieskring_name
- the name of 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);
byte number()
normal_behavior ensures 0 <= \result && \result <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;
java.lang.String name()
normal_behavior ensures \result.length() <= KIESKRING_NAME_MAX_LENGTH;
boolean addDistrict(District a_district)
a_district
- the district to add.
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;
District[] getDistricten()
normal_behavior requires true; ensures \result == my_districts; ensures districtCount() == \old(districtCount());
District getDistrict(byte a_district_number)
a_district_number
- the number of the district to get.
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());
boolean hasDistrict(District a_district)
a_district
- the district to check for.
normal_behavior ensures \result <==> (my_districts[a_district.number()] != null) && (my_districts[a_district.number()].equals(a_district)); ensures districtCount() == \old(districtCount());
byte districtCount()
normal_behavior ensures \result == my_district_count; implies_that ensures \result >= 0;
boolean addKiesLijst(KiesLijst a_kieslijst)
a_kieslijst
- the kieslijst to add.
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;
KiesLijst[] getKiesLijsten()
normal_behavior requires true; ensures \result == my_kiesLijsten; ensures kieslijstCount() == \old(kieslijstCount());
KiesLijst getKiesLijst(byte a_kieslijst_number)
a_kieslijst_number
- the number of the kieslijst that we are
interested in.
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());
boolean hasKiesLijst(KiesLijst a_kieslijst)
a_kieslijst
- the kieslijst that we wish to check for.
normal_behavior ensures \result <==> (my_kiesLijsten[a_kieslijst.number()] != null) && (my_kiesLijsten[a_kieslijst.number()].equals(a_kieslijst)); ensures kieslijstCount() == \old(kieslijstCount());
byte kieslijstCount()
normal_behavior ensures \result == my_kieslijst_count; implies_that ensures \result >= 0;
void clear()
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;
public boolean equals(java.lang.Object an_object)
public int hashCode()
public java.lang.String toString()
public int compareTo(java.lang.Object an_object)
compareTo
in interface java.lang.Comparable
|
SOA © 2004 SoS Group All Rights Reserved |
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |