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 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`

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