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 Candidate

    java.lang.Object
      sos.koa.Candidate

All Implemented Interfaces:
  java.lang.Comparable, java.io.Serializable

public class Candidate
extends java.lang.Object
implements java.lang.Comparable, java.io.Serializable

A candidate in an election.

Version:
  $Id: Candidate.java,v 1.30 2004/05/16 20:37:40 kiniry Exp $
Author:
  Joe Kiniry (kiniry@cs.kun.nl)

Class Specifications
invariant my_lastname.length() <= LASTNAME_MAX_LENGTH; invariant my_lastname.owner == this; invariant my_firstname.length() <= FIRSTNAME_MAX_LENGTH; invariant my_firstname.owner == this; invariant my_initials.length() <= INITIALS_MAX_LENGTH; invariant my_initials.owner == this; invariant my_gender == MALE||my_gender == FEMALE||my_gender == UNKNOWN; invariant 0 <= my_position_number; invariant my_position_number <= KiesLijst.MAX_CANDIDATES_PER_KIESLIJST; invariant my_city_of_residence.length() <= CITY_OF_RESIDENCE_MAX_LENGTH; invariant my_city_of_residence.owner == this; invariant my_vote_count >= 0;

Field Summary
`(package private) static byte` | `CITY_OF_RESIDENCE_MAX_LENGTH` The maximum length, in digits represented by characters, of the city of residence of a candidate.
`(package private) static char` | `FEMALE` The possible values of the gender of a candidate.
`(package private) static byte` | `FIRSTNAME_MAX_LENGTH` The maximum length, in characters, of the firstname of a candidate.
`(package private) static byte` | `INITIALS_MAX_LENGTH` The maximum length, in characters, of the initials of a candidate.
`(package private) static byte` | `LASTNAME_MAX_LENGTH` The maximum length, in character, of the lastname (surname) of a candidate.
`(package private) static char` | `MALE` The possible values of the gender of a candidate.
`[spec_public] private java.lang.String` | `my_city_of_residence` The city of residence (woonplaats) of a candidate.
`[spec_public] private java.lang.String` | `my_firstname` The firstname (roepnaam) of a candidate.
`[spec_public] private char` | `my_gender` The gender (geslacht) of a candidate.
`[spec_public] private java.lang.String` | `my_initials` The initials (voorletters) of a candidate.
`[spec_public] private KiesKring` | `my_kiesKring` The kieskring of a candidate.
`[spec_public] private KiesLijst` | `my_kiesLijst` The kieslijst of a candidate.
`[spec_public] private java.lang.String` | `my_lastname` The lastname (achternaam) of a candidate.
`[spec_public] private byte` | `my_position_number` The position number (positienummer) of a candidate.
`[spec_public] private int` | `my_vote_count` The number of votes cast for this candidate.
`(package private) static byte` | `POSITION_NUMBER_MAX_LENGTH` The maximum length, in digits represented by characters, of the position number of a candidate.
`(package private) static char` | `UNKNOWN` The possible values of the gender of a candidate.

Constructor Summary
`(package private)` | `Candidate(non_null java.lang.String a_lastname, non_null java.lang.String a_firstname, non_null java.lang.String some_initials, char a_gender, byte a_position_number, non_null java.lang.String a_city_of_residence, non_null KiesKring a_kieskring, non_null KiesLijst a_kieslijst)` Construct a new candidate object given the specified initialization values.

Method Summary
`(package private) java.lang.String` | `cityOfResidence()`
`int` | `compareTo(java.lang.Object an_object)`
`boolean` | `equals(java.lang.Object an_object)` {@inheritDoc}
`(package private) java.lang.String` | `firstname()`
`(package private) char` | `gender()`
`int` | `hashCode()` {@inheritDoc}
`(package private) int` | `incrementVoteCount()`
`(package private) java.lang.String` | `initials()`
`(package private) KiesKring` | `kiesKring()`
`(package private) KiesLijst` | `kiesLijst()`
`(package private) java.lang.String` | `lastname()`
`(package private) byte` | `position_number()`
`java.lang.String` | `toString()` {@inheritDoc}
`(package private) int` | `voteCount()`

Methods inherited from class java.lang.Object
`clone, finalize, getClass, notify, notifyAll, wait, wait, wait`

Field Detail

### LASTNAME_MAX_LENGTH

    static final byte LASTNAME_MAX_LENGTH

  The maximum length, in character, of the lastname (surname) of a candidate.

### FIRSTNAME_MAX_LENGTH

    static final byte FIRSTNAME_MAX_LENGTH

  The maximum length, in characters, of the firstname of a candidate.

### INITIALS_MAX_LENGTH

    static final byte INITIALS_MAX_LENGTH

  The maximum length, in characters, of the initials of a candidate.

### MALE

    static final char MALE

  The possible values of the gender of a candidate.

### FEMALE

    static final char FEMALE

  The possible values of the gender of a candidate.

### UNKNOWN

    static final char UNKNOWN

  The possible values of the gender of a candidate.

### POSITION_NUMBER_MAX_LENGTH

    static final byte POSITION_NUMBER_MAX_LENGTH

  The maximum length, in digits represented by characters, of the position number of a candidate.

### CITY_OF_RESIDENCE_MAX_LENGTH

    static final byte CITY_OF_RESIDENCE_MAX_LENGTH

  The maximum length, in digits represented by characters, of the city of residence of a candidate.

### my_lastname

    private java.lang.String my_lastname

  The lastname (achternaam) of a candidate.

  Specifications: spec_public non_null

### my_firstname

    private java.lang.String my_firstname

  The firstname (roepnaam) of a candidate.

  Specifications: spec_public non_null

### my_initials

    private java.lang.String my_initials

  The initials (voorletters) of a candidate.

  Specifications: spec_public non_null

### my_gender

    private char my_gender

  The gender (geslacht) of a candidate.

  Specifications: spec_public

### my_position_number

    private byte my_position_number

  The position number (positienummer) of a candidate.

  Specifications: spec_public

### my_city_of_residence

    private java.lang.String my_city_of_residence

  The city of residence (woonplaats) of a candidate.

  Specifications: spec_public non_null

### my_kiesKring

    private KiesKring my_kiesKring

  The kieskring of a candidate.

  Specifications: spec_public non_null

### my_kiesLijst

    private KiesLijst my_kiesLijst

  The kieslijst of a candidate.

  Specifications: spec_public non_null

### my_vote_count

    private int my_vote_count

  The number of votes cast for this candidate.

  Specifications: spec_public

Constructor Detail

### Candidate

    Candidate(non_null java.lang.String a_lastname,
              non_null java.lang.String a_firstname,
              non_null java.lang.String some_initials,
              char a_gender,
              byte a_position_number,
              non_null java.lang.String a_city_of_residence,
              non_null KiesKring a_kieskring,
              non_null KiesLijst a_kieslijst)

  Construct a new candidate object given the specified initialization values.

  Parameters:
    `a_lastname` - the lastname of the new candidate.
    `a_firstname` - the firstname of the new candidate.
    `some_initials` - the initial of the new candidate.
    `a_gender` - the gender of the new candidate.
    `a_position_number` - the position number of the new candidate.
    `a_city_of_residence` - the city of residence of the new candidate.
    `a_kieskring` - the kieskring of the new candidate.
    `a_kieslijst` - the kieslijst of the new candidate.

  Specifications:
    normal_behavior
    requires (* all parameters must be of the proper length *);
    requires a_lastname.length() <= LASTNAME_MAX_LENGTH;
    requires a_firstname.length() <= FIRSTNAME_MAX_LENGTH;
    requires some_initials.length() <= INITIALS_MAX_LENGTH;
    requires a_gender == MALE||a_gender == FEMALE||a_gender == UNKNOWN;
    requires 0 <= a_position_number;
    requires a_position_number <= KiesLijst.MAX_CANDIDATES_PER_KIESLIJST;
    requires a_city_of_residence.length() <= CITY_OF_RESIDENCE_MAX_LENGTH;
    requires a_kieslijst.candidateCount() < KiesLijst.MAX_CANDIDATES_PER_KIESLIJST;
    assignable \everything;
    ensures (* all fields are properly initialized *);
    ensures lastname().equals(a_lastname);
    ensures firstname().equals(a_firstname);
    ensures initials().equals(some_initials);
    ensures gender() == a_gender;
    ensures position_number() == a_position_number;
    ensures cityOfResidence().equals(a_city_of_residence);
    ensures kiesKring().equals(a_kieskring);
    ensures kiesLijst().equals(a_kieslijst);
    ensures kiesLijst().candidateCount() == \old(a_kieslijst.candidateCount()+1);

Method Detail

### lastname

    final java.lang.String lastname()

  Returns:
    the lastname of this candidate.

  Specifications: pure non_null
    normal_behavior
    ensures \result .length() <= LASTNAME_MAX_LENGTH;

### firstname

    final java.lang.String firstname()

  Returns:
    the firstname of this candidate.

  Specifications: pure non_null
    normal_behavior
    ensures \result .length() <= FIRSTNAME_MAX_LENGTH;

### initials

    final java.lang.String initials()

  Returns:
    the initials of this candidate.

  Specifications: pure non_null
    normal_behavior
    ensures \result .length() <= INITIALS_MAX_LENGTH;

### gender

    final char gender()

  Returns:
    the gender of this candidate.

  Specifications: pure
    normal_behavior
    ensures \result == MALE||\result == FEMALE||\result == UNKNOWN;

### position_number

    final byte position_number()

  Returns:
    the position number of this candidate.

  Specifications: pure
    normal_behavior
    ensures 0 <= \result &&\result <= KiesLijst.MAX_CANDIDATES_PER_KIESLIJST;

### cityOfResidence

    final java.lang.String cityOfResidence()

  Returns:
    the city of residence of this candidate.
  Specifications: pure non_null

### kiesKring

    final KiesKring kiesKring()

  Returns:
    the kieskring of this candidate.

  Specifications: pure non_null
    normal_behavior
    ensures \result == my_kiesKring;

### kiesLijst

    final KiesLijst kiesLijst()

  Returns:
    the kieslijst of this candidate.

  Specifications: pure non_null
    normal_behavior
    ensures \result == my_kiesLijst;

### incrementVoteCount

    final int incrementVoteCount()

  Returns:
    the vote count of this candidate.

  Specifications:
    normal_behavior
    assignable my_vote_count;
    ensures my_vote_count == \old(my_vote_count+1);

### voteCount

    final int voteCount()

  Returns:
    the vote count of this candidate.

  Specifications: pure
    normal_behavior
    ensures \result == my_vote_count;

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