sos.koa
Class District

java.lang.Object
  sos.koa.District

All Implemented Interfaces:

java.lang.Comparable, java.io.Serializable

class District

extends java.lang.Object

implements java.lang.Comparable, java.io.Serializable

A district is a region of the country within a kieskring. Each kieskring has one or more districts.

Version:

$Id: District.java,v 1.21 2004/05/16 20:37:39 kiniry Exp $

Author:

Joe Kiniry (kiniry@cs.kun.nl)

Class Specifications

invariant 0 <= my_number&&my_number <= KiesKring.MAX_DISTRICTS_PER_KIESKRING; invariant my_name.length() <= DISTRICT_NAME_MAX_LENGTH; invariant (my_kiesKring != null) ==> this.owner == my_kiesKring;

Field Summary
(package private) static byte	DISTRICT_NAME_MAX_LENGTH           The maximum length, in characters, of a district's name.
(package private) static byte	DISTRICT_NUMBER_MAX_LENGTH           The maximum length, in digits, of a district's number.
[spec_public] private  KiesKring	my_kiesKring           Each district is in exactly one KiesKring.
[spec_public] private  java.lang.String	my_name           The name of this district.
[spec_public] private  int	my_number           The number of this district.

 

Constructor Summary
(package private)	District(int a_district_number, non_null java.lang.String a_district_name)           Construct a new district object given the specified initialization values.

 

Method Summary
(package private)  void	clear()           Clears the information of this district.
int	compareTo(java.lang.Object an_object)
boolean	equals(java.lang.Object an_object)           {@inheritDoc}
int	hashCode()           {@inheritDoc}
(package private)  KiesKring	kiesKring()
(package private)  java.lang.String	name()
(package private)  int	number()
java.lang.String	toString()           {@inheritDoc}

 

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

 

Field Detail

DISTRICT_NUMBER_MAX_LENGTH

static final byte DISTRICT_NUMBER_MAX_LENGTH

The maximum length, in digits, of a district's number.

DISTRICT_NAME_MAX_LENGTH

static final byte DISTRICT_NAME_MAX_LENGTH

The maximum length, in characters, of a district's name.

my_number

private int my_number

The number of this district.

Specifications: spec_public

my_name

private java.lang.String my_name

The name of this district.

Specifications: spec_public non_null

my_kiesKring

private KiesKring my_kiesKring

Each district is in exactly one KiesKring.

Specifications: spec_public

District

District(int a_district_number,
         non_null java.lang.String a_district_name)

Construct a new district object given the specified initialization values.

Parameters:

a_district_number - the number of the new district.

a_district_name - the name of the new district.

Specifications:

private normal_behavior
requires 0 <= a_district_number;
requires a_district_number <= KiesKring.MAX_DISTRICTS_PER_KIESKRING;
requires a_district_name.length() <= DISTRICT_NAME_MAX_LENGTH;
assignable \everything;
ensures number() == a_district_number;
ensures name().equals(a_district_name);

clear

final void clear()

Clears the information of this district.

Specifications:

normal_behavior
assignable objectState;
ensures number() == 0;
ensures name().equals("");
ensures kiesKring() == null;

number

final int number()

Returns:

the number of this district.

Specifications: pure

normal_behavior
ensures 0 <= \result &&\result <= KiesKring.MAX_DISTRICTS_PER_KIESKRING;
ensures \result == my_number;

name

final java.lang.String name()

Returns:

the name of this district.

Specifications: pure non_null

normal_behavior
ensures \result .length() <= DISTRICT_NAME_MAX_LENGTH;
ensures \result == my_name;

kiesKring

final KiesKring kiesKring()

Returns:

the kieskring of this district.

Specifications: pure

normal_behavior
ensures \result == my_kiesKring;

equals

public final boolean equals(java.lang.Object an_object)

{@inheritDoc}

Overrides:

equals in class java.lang.Object

hashCode

public final int hashCode()

{@inheritDoc}

Overrides:

hashCode in class java.lang.Object

toString

public final java.lang.String toString()

{@inheritDoc}

Overrides:

toString in class java.lang.Object

compareTo

public final int compareTo(java.lang.Object an_object)

Specified by:

compareTo in interface java.lang.Comparable