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

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