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)

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