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 VoteSet

java.lang.Object
  extended bysos.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)

Class Specifications
invariant my_vote_has_been_finalized ==> my_vote_has_been_initialized;
invariant my_candidate_list.owner == this;

Field Summary
[spec_public] private  CandidateList my_candidate_list
          The list of all candidates in an election.
[spec_public] 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.
[spec_public] 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(non_null 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(non_null 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(non_null java.lang.String a_candidate_code, non_null java.lang.String a_kieskring_number)
          Validate the information provided, which are the redundant components of an encrypted vote.
(package private)  boolean validateRedundantInfo(non_null java.lang.String a_candidate_code, non_null java.lang.String a_lastname, non_null java.lang.String some_initials, non_null java.lang.String a_party_name, non_null java.lang.String a_party_number, non_null 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(non_null java.lang.String a_candidate_code)
           
(package private)  int voteCount(int a_candidate_code)
           
(package private)  int voteCount(non_null 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.

Specifications: spec_public

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.

Specifications: spec_public

my_candidate_list

private CandidateList my_candidate_list
The list of all candidates in an election.

Specifications: spec_public non_null
Constructor Detail

VoteSet

VoteSet(non_null 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. 






Specifications: pure


 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(non_null java.lang.String a_candidate_code,
                                    non_null java.lang.String a_lastname,
                                    non_null java.lang.String some_initials,
                                    non_null java.lang.String a_party_name,
                                    non_null java.lang.String a_party_number,
                                    non_null 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(), 







Specifications: pure


 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(non_null java.lang.String a_candidate_code,
                                      non_null 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(), 







Specifications: pure


 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(non_null java.lang.String a_candidate_code)






Parameters:
a_candidate_code - the candidate code to check.
 


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






Specifications: pure


 normal_behavior

requires 0 <= Integer.parseInt(a_candidate_code);

ensures \result  == my_candidate_list.validCandidate(a_candidate_code);












validCandidate


final boolean validCandidate(int a_candidate_code)






Parameters:
a_candidate_code - the candidate code to check.
 


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






Specifications: pure


 normal_behavior

requires 0 <= a_candidate_code;

ensures \result  == my_candidate_list.validCandidate(a_candidate_code);












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:






Specifications:


 normal_behavior

requires !my_vote_has_been_initialized&&!my_vote_has_been_finalized;

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

assignable \nothing;

signals (IllegalArgumentException) true;












addVote


final void addVote(non_null 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.
 






Specifications:


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

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

assignable \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.
 






Specifications:


 normal_behavior

requires my_vote_has_been_initialized&&!my_vote_has_been_finalized;

requires 0 <= a_candidate_code;

requires validCandidate(a_candidate_code);

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

assignable \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:






Specifications:


 normal_behavior

requires my_vote_has_been_initialized&&!my_vote_has_been_finalized;

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

assignable \nothing;

signals (IllegalArgumentException) true;












voteCount


final int voteCount(non_null 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.
 






Specifications: pure


 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.
 






Specifications: pure


 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;























  

      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