sos.koa
Class VoteSet

java.lang.Object
  sos.koa.VoteSet

All Implemented Interfaces:

java.io.Serializable

public class VoteSet

extends java.lang.Object

implements java.io.Serializable

The set of votes in an election.

Version:

$Id: VoteSet.java,v 1.29 2004/05/17 16:56:40 hubbers Exp $

Author:

Joe Kiniry (kiniry@cs.kun.nl)

See Also:

Serialized Form

Field Summary

private CandidateList	my_candidate_list The list of all candidates in an election.
private boolean	my_vote_has_been_finalized A flag that indicates that the vote has been finalized and the only thing happening henceforth is requesting the total count.
private boolean	my_vote_has_been_initialized A flag that indicates that the vote has been initialized and the only thing happening henceforth is counting then finalizing.

Constructor Summary

(package private)

VoteSet(CandidateList a_candidate_list) Constructs a new, initialized VoteSet for the provided CandidateList.

Method Summary

(package private) void	addVote(int a_candidate_code) Add a single vote to this vote set for the specified candidate code.
(package private) void	addVote(java.lang.String a_candidate_code) Add a single vote to this vote set for the specified candidate code.
(package private) void	finalizeVote() Finalize the vote for this vote set.
(package private) void	initializeVote() Initialize the vote for this vote set.
(package private) boolean	validateKiesKringNumber(java.lang.String a_candidate_code, java.lang.String a_kieskring_number) Validate the information provided, which are the redundant components of an encrypted vote.
(package private) boolean	validateRedundantInfo(java.lang.String a_candidate_code, java.lang.String a_lastname, java.lang.String some_initials, java.lang.String a_party_name, java.lang.String a_party_number, java.lang.String a_position_number) Validate the information provided, which are the redundant components of an encrypted vote.
(package private) boolean	validCandidate(int a_candidate_code)
(package private) boolean	validCandidate(java.lang.String a_candidate_code)
(package private) int	voteCount(int a_candidate_code)
(package private) int	voteCount(java.lang.String a_candidate_code)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

my_vote_has_been_initialized

private boolean my_vote_has_been_initialized

A flag that indicates that the vote has been initialized and the only thing happening henceforth is counting then finalizing.

my_vote_has_been_finalized

private boolean my_vote_has_been_finalized

A flag that indicates that the vote has been finalized and the only thing happening henceforth is requesting the total count.

my_candidate_list

private CandidateList my_candidate_list

The list of all candidates in an election.

Constructor Detail

VoteSet

VoteSet(CandidateList a_candidate_list)

Constructs a new, initialized VoteSet for the provided CandidateList.

Parameters:

a_candidate_list - the CandidateList to be used in the vote.

 normal_behavior
   ensures my_candidate_list == a_candidate_list;
   ensures !my_vote_has_been_initialized && !my_vote_has_been_finalized;
 

Method Detail

validateRedundantInfo

final boolean validateRedundantInfo(java.lang.String a_candidate_code,
                                    java.lang.String a_lastname,
                                    java.lang.String some_initials,
                                    java.lang.String a_party_name,
                                    java.lang.String a_party_number,
                                    java.lang.String a_position_number)
                             throws KOAException

Validate the information provided, which are the redundant components of an encrypted vote. Validation means that the given position number corresponds to the candidate who has all of the other provided information.

Parameters:

a_candidate_code - the candidate's code.

a_lastname - the candidate's lastname.

some_initials - the candidate's initials.

a_party_name - the candidate's party name.

a_party_number - the candidate's party number.

a_position_number - the candidate's position number.

Returns:

a flag indicating the validity of the provided data.

Throws:

java.lang.IllegalArgumentException - is thrown if the vote has not been initialized or the vote has already been finalized.

KOAException

See Also:

initializeVote(),

 normal_behavior
   requires my_vote_has_been_initialized && !my_vote_has_been_finalized;
   requires (* all parameters must be of the proper length *);
   requires a_lastname.length() <= Candidate.LASTNAME_MAX_LENGTH;
   requires some_initials.length() <= Candidate.INITIALS_MAX_LENGTH;
   requires a_position_number.length() <= Candidate.POSITION_NUMBER_MAX_LENGTH;
   requires a_party_name.length() <= KiesKring.KIESKRING_NAME_MAX_LENGTH;
   requires 0 <= Byte.parseByte(a_party_number);
   requires Byte.parseByte(a_party_number) <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;
   requires 0 <= Byte.parseByte(a_position_number);
   requires Byte.parseByte(a_position_number) <= KiesLijst.MAX_CANDIDATES_PER_KIESLIJST;
   requires my_candidate_list.validCandidate(a_candidate_code);
   ensures \result ==> my_candidate_list.getCandidate(a_candidate_code) != null;
   ensures \result ==> my_candidate_list.getCandidate(a_candidate_code).lastname().equals(a_lastname);
   ensures \result ==> my_candidate_list.getCandidate(a_candidate_code).initials().equals(some_initials);
   ensures \result ==> my_candidate_list.getCandidate(a_candidate_code).kiesLijst().name().equals(a_party_name);
   ensures \result ==> my_candidate_list.getCandidate(a_candidate_code).kiesLijst().number() == Byte.parseByte(a_party_number);
   ensures \result <== (my_candidate_list.getCandidate(a_candidate_code) != null &&
                       my_candidate_list.getCandidate(a_candidate_code).lastname().equals(a_lastname) &&
                       my_candidate_list.getCandidate(a_candidate_code).initials().equals(some_initials) &&
                       my_candidate_list.getCandidate(a_candidate_code).kiesLijst().name().equals(a_party_name) &&
                       my_candidate_list.getCandidate(a_candidate_code).kiesLijst().number() == Byte.parseByte(a_party_number));
 also
 exceptional_behavior
   requires !(my_vote_has_been_initialized && !my_vote_has_been_finalized);
   signals (IllegalArgumentException) true;
 

validateKiesKringNumber

final boolean validateKiesKringNumber(java.lang.String a_candidate_code,
                                      java.lang.String a_kieskring_number)

Validate the information provided, which are the redundant components of an encrypted vote. Validation means that the kieskring represented by the given kieskring number contains the specified candidate code.

Parameters:

a_candidate_code - the code of the candidate to validate

a_kieskring_number - the number of the kieskring to validate.

Returns:

a flag indicating the validity of the provided data.

Throws:

java.lang.IllegalArgumentException - is thrown if the vote has not been initialized or the vote has already been finalized.

See Also:

initializeVote(),

 normal_behavior
   requires my_vote_has_been_initialized && !my_vote_has_been_finalized;
   requires 0 <= Byte.parseByte(a_kieskring_number);
   requires Byte.parseByte(a_kieskring_number) <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;
   requires my_candidate_list.validCandidate(a_candidate_code);
   ensures \result ==> my_candidate_list.getCandidate(a_candidate_code) != null;
   ensures \result ==> my_candidate_list.getCandidate(a_candidate_code).kiesKring().number() == Byte.parseByte(a_kieskring_number);
   ensures \result ==> AuditLog.hasKiesKring(my_candidate_list.getCandidate(a_candidate_code).kiesKring().number());
   ensures \result <== (my_candidate_list.getCandidate(a_candidate_code) != null &&
                        my_candidate_list.getCandidate(a_candidate_code).kiesKring().number() == Byte.parseByte(a_kieskring_number) &&
                        AuditLog.hasKiesKring(my_candidate_list.getCandidate(a_candidate_code).kiesKring().number())
                       );
 also
 exceptional_behavior
   requires !(my_vote_has_been_initialized && !my_vote_has_been_finalized);
   signals (IllegalArgumentException) true;
 

validCandidate

final boolean validCandidate(java.lang.String a_candidate_code)

Parameters:

a_candidate_code - the candidate code to check.

 normal_behavior
   requires 0 <= Integer.parseInt(a_candidate_code);
   ensures \result == my_candidate_list.validCandidate(a_candidate_code);
 

Returns:

a flag indicating if the specified candidate code is a valid candidate for this vote set.

validCandidate

final boolean validCandidate(int a_candidate_code)

Parameters:

a_candidate_code - the candidate code to check.

 normal_behavior
   requires 0 <= a_candidate_code;
   ensures \result == my_candidate_list.validCandidate(a_candidate_code);
 

Returns:

a flag indicating if the specified candidate code is a valid candidate for this vote set.

initializeVote

final void initializeVote()

Initialize the vote for this vote set. Initialization may only happen once. After initialization, the only methods that may be called are those whose preconditions are my_vote_has_been_initialized.

Throws:

java.lang.IllegalArgumentException - is thrown if the vote has not been initialized or the vote has already been finalized.

See Also:

 normal_behavior
   requires !my_vote_has_been_initialized && !my_vote_has_been_finalized;
   modifies my_vote_has_been_initialized;
   ensures my_vote_has_been_initialized;
 also
 exceptional_behavior
   requires my_vote_has_been_initialized || my_vote_has_been_finalized;
   modifies \nothing;
   signals (IllegalArgumentException) true;
 

addVote

final void addVote(java.lang.String a_candidate_code)

Add a single vote to this vote set for the specified candidate code.

Parameters:

a_candidate_code - the candidate code for which to increment the vote count by one.

Throws:

java.lang.IllegalArgumentException - is thrown if the vote has not been initialized or the vote has already been finalized.

 normal_behavior
   requires my_vote_has_been_initialized && !my_vote_has_been_finalized;
   requires 0 <= Integer.parseInt(a_candidate_code);
   requires validCandidate(a_candidate_code);
   modifies \everything;
   ensures my_candidate_list.getCandidate(a_candidate_code).voteCount() ==
           \old(my_candidate_list.getCandidate(a_candidate_code).voteCount() + 1);
 also
 exceptional_behavior
   requires !(my_vote_has_been_initialized && !my_vote_has_been_finalized);
   modifies \nothing;
   signals (IllegalArgumentException) true;
 

addVote

final void addVote(int a_candidate_code)

Add a single vote to this vote set for the specified candidate code.

Parameters:

a_candidate_code - the candidate code for which to increment the vote count by one.

Throws:

java.lang.IllegalArgumentException - is thrown if the vote has not been initialized or the vote has already been finalized.

 normal_behavior
   requires my_vote_has_been_initialized && !my_vote_has_been_finalized;
   requires 0 <= a_candidate_code;
   requires validCandidate(a_candidate_code);
   modifies \everything;
   ensures my_candidate_list.getCandidate(a_candidate_code).voteCount() ==
           \old(my_candidate_list.getCandidate(a_candidate_code).voteCount() + 1);
 also
 exceptional_behavior
   requires !(my_vote_has_been_initialized && !my_vote_has_been_finalized);
   modifies \nothing;
   signals (IllegalArgumentException) true;
 

finalizeVote

final void finalizeVote()

Finalize the vote for this vote set. Finalization may only happen once. After finalization, the only methods that may be called are those whose preconditions are my_vote_has_been_finalized. Finalizing the vote means that no more votes are to be counted.

Throws:

java.lang.IllegalArgumentException - is thrown if the vote has not been initialized or the vote has already been finalized.

See Also:

 normal_behavior
   requires my_vote_has_been_initialized && !my_vote_has_been_finalized;
   modifies my_vote_has_been_finalized;
   ensures my_vote_has_been_finalized;
 also
 exceptional_behavior
   requires !(my_vote_has_been_initialized && !my_vote_has_been_finalized);
   modifies \nothing;
   signals (IllegalArgumentException) true;
 

voteCount

final int voteCount(java.lang.String a_candidate_code)

Parameters:

a_candidate_code - the candidate code of interest.

Returns:

the number of votes cast for the specified candidate code.

Throws:

java.lang.IllegalArgumentException - is thrown if the vote has not been initialized and the vote has note been finalized.

 normal_behavior
   requires my_vote_has_been_initialized && my_vote_has_been_finalized;
   requires 0 <= Integer.parseInt(a_candidate_code);
   requires validCandidate(a_candidate_code);
   ensures 0 <= \result;
 also
 exceptional_behavior
   requires !(my_vote_has_been_initialized && my_vote_has_been_finalized);
   signals (IllegalArgumentException) true;
 

voteCount

final int voteCount(int a_candidate_code)

Parameters:

a_candidate_code - the candidate code of interest.

Returns:

the number of votes cast for the specified candidate code.

Throws:

java.lang.IllegalArgumentException - is thrown if the vote has not been initialized and the vote has note been finalized.

 normal_behavior
   requires my_vote_has_been_initialized && my_vote_has_been_finalized;
   requires 0 <= a_candidate_code;
   requires validCandidate(a_candidate_code);
   ensures 0 <= \result;
 also
 exceptional_behavior
   requires !(my_vote_has_been_initialized && my_vote_has_been_finalized);
   signals (IllegalArgumentException) true;