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)

See Also:

Serialized Form

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.
private java.lang.String	my_city_of_residence The city of residence (woonplaats) of a candidate.
private java.lang.String	my_firstname The firstname (roepnaam) of a candidate.
private char	my_gender The gender (geslacht) of a candidate.
private java.lang.String	my_initials The initials (voorletters) of a candidate.
private KiesKring	my_kiesKring The kieskring of a candidate.
private KiesLijst	my_kiesLijst The kieslijst of a candidate.
private java.lang.String	my_lastname The lastname (achternaam) of a candidate.
private byte	my_position_number The position number (positienummer) of a candidate.
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(java.lang.String a_lastname, java.lang.String a_firstname, java.lang.String some_initials, char a_gender, byte a_position_number, java.lang.String a_city_of_residence, KiesKring a_kieskring, 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)
(package private) java.lang.String	firstname()
(package private) char	gender()
int	hashCode()
(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()
(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.

See Also:

Constant Field Values

FIRSTNAME_MAX_LENGTH

static final byte FIRSTNAME_MAX_LENGTH

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

See Also:

Constant Field Values

INITIALS_MAX_LENGTH

static final byte INITIALS_MAX_LENGTH

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

See Also:

Constant Field Values

MALE

static final char MALE

The possible values of the gender of a candidate.

See Also:

Constant Field Values

FEMALE

static final char FEMALE

The possible values of the gender of a candidate.

See Also:

Constant Field Values

UNKNOWN

static final char UNKNOWN

The possible values of the gender of a candidate.

See Also:

Constant Field Values

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.

See Also:

Constant Field Values

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.

See Also:

Constant Field Values

my_lastname

private java.lang.String my_lastname

The lastname (achternaam) of a candidate.

my_firstname

private java.lang.String my_firstname

The firstname (roepnaam) of a candidate.

my_initials

private java.lang.String my_initials

The initials (voorletters) of a candidate.

my_gender

private char my_gender

The gender (geslacht) of a candidate.

my_position_number

private byte my_position_number

The position number (positienummer) of a candidate.

my_city_of_residence

private java.lang.String my_city_of_residence

The city of residence (woonplaats) of a candidate.

my_kiesKring

private KiesKring my_kiesKring

The kieskring of a candidate.

my_kiesLijst

private KiesLijst my_kiesLijst

The kieslijst of a candidate.

my_vote_count

private int my_vote_count

The number of votes cast for this candidate.

Constructor Detail

Candidate

Candidate(java.lang.String a_lastname,
          java.lang.String a_firstname,
          java.lang.String some_initials,
          char a_gender,
          byte a_position_number,
          java.lang.String a_city_of_residence,
          KiesKring a_kieskring,
          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.

 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;
   modifies \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.

 normal_behavior
   ensures \result.length() <= LASTNAME_MAX_LENGTH;
 

firstname

final java.lang.String firstname()

Returns:

the firstname of this candidate.

 normal_behavior
   ensures \result.length() <= FIRSTNAME_MAX_LENGTH;
 

initials

final java.lang.String initials()

Returns:

the initials of this candidate.

 normal_behavior
   ensures \result.length() <= INITIALS_MAX_LENGTH;
 

gender

final char gender()

Returns:

the gender of this candidate.

 normal_behavior
   ensures \result == MALE || \result == FEMALE || \result == UNKNOWN;
 

position_number

final byte position_number()

Returns:

the position number of this candidate.

 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.

kiesKring

final KiesKring kiesKring()

Returns:

the kieskring of this candidate.

 normal_behavior
   ensures \result == my_kiesKring;
 

kiesLijst

final KiesLijst kiesLijst()

Returns:

the kieslijst of this candidate.

 normal_behavior
   ensures \result == my_kiesLijst;
 

incrementVoteCount

final int incrementVoteCount()

Returns:

the vote count of this candidate.

 normal_behavior
   modifies my_vote_count;
   ensures my_vote_count == \old(my_vote_count + 1);
 

voteCount

final int voteCount()

Returns:

the vote count of this candidate.

 normal_behavior
   ensures \result == my_vote_count;
 

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