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)

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.
private KiesKring	my_kiesKring Each district is in exactly one KiesKring.
private java.lang.String	my_name The name of this district.
private int	my_number The number of this district.

Constructor Summary

(package private)

District(int a_district_number, 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)
int	hashCode()
(package private) KiesKring	kiesKring()
(package private) java.lang.String	name()
(package private) int	number()
java.lang.String	toString()

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.

See Also:

Constant Field Values

DISTRICT_NAME_MAX_LENGTH

static final byte DISTRICT_NAME_MAX_LENGTH

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

See Also:

Constant Field Values

my_number

private int my_number

The number of this district.

my_name

private java.lang.String my_name

The name of this district.

my_kiesKring

private KiesKring my_kiesKring

Each district is in exactly one KiesKring.

Constructor Detail

District

District(int a_district_number,
         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.

 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;
   modifies \everything;
   ensures number() == a_district_number;
   ensures name().equals(a_district_name);
 

Method Detail

clear

final void clear()

Clears the information of this district.

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

number

final int number()

Returns:

the number of this district.

 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.

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

kiesKring

final KiesKring kiesKring()

Returns:

the kieskring of this district.

 normal_behavior
   ensures \result == my_kiesKring;
 

equals

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

hashCode

public final int hashCode()

toString

public final java.lang.String toString()

compareTo

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

Specified by:

compareTo in interface java.lang.Comparable