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)

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

Constructor Detail

### 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);

Method Detail

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

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