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)

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`

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