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

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

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