<commit_before>package election.tally;

import java.util.logging.Logger;

/**
 * The Candidate object records the number of votes received during each round
 * of counting. Votes can only be added to the candidate's stack while the
 * candidate has a status of <code>CONTINUING</code>.
 * 
 * @see <a href="http://www.cev.ie/htm/tenders/pdf/1_2.pdf"> Department of
 *      Environment and Local Government, Count Requirements and Commentary on
 *      Count Rules, section 3-14</a>
 * @author <NAME>
 */

public class Candidate extends CandidateStatus {
  
  /**
   * Maximum expected number of candidates in any one constituency.
   * 
   * @see <a
   *      href="http://en.wikipedia.org/wiki/List_of_political_parties_in_the_Republic_of_Ireland">List
   *      of political parties in Ireland</a> The average number of candidates
   *      could be much less.
   */
  public static final int                     MAX_CANDIDATES  = 20;
  
  /**
   * Identifier for the candidate. The data should be loaded in such a way that
   * the assignment of candidate IDs is fair and unbiased.
   */
  /*@ public invariant 0 <= candidateID;
    @ public constraint \old(candidateID) != NO_CANDIDATE
    @   ==> candidateID == \old(candidateID);
    @*/
  protected transient/*@ spec_public @*/int  candidateID;
  
  /** Number of votes added at each count */
  /*@ public invariant (\forall int i; 0 < i && i < votesAdded.length;
    @   0 <= votesAdded[i]);
    @ public initially (\forall int i; 0 < i && i < votesAdded.length;
    @   votesAdded[i] == 0);	
    @ public invariant votesAdded.length == CountConfiguration.MAXCOUNT;
    @*/
  protected/*@ spec_public non_null @*/int[] votesAdded      =
                                                                  new int[CountConfiguration.MAXCOUNT];
  
  /** Number of votes removed at each count */
  /*@ public invariant (\forall int i; 0 < i && i < votesRemoved.length;
    @                                  0 <= votesRemoved[i]);
    @ public initially (\forall int i; 0 < i && i < votesRemoved.length;
    @                                  votesRemoved[i] == 0);
    @ public invariant votesRemoved.length == CountConfiguration.MAXCOUNT;
    @*/
  protected/*@ spec_public non_null @*/int[] votesRemoved    =
                                                                  new int[CountConfiguration.MAXCOUNT];
  
  //@ public invariant votesAdded != votesRemoved;
  //@ public invariant votesRemoved != votesAdded;
  
  /** The status of the candidate at the latest count */
  /*@ public invariant state == ELECTED || state == ELIMINATED ||
    @   state == CONTINUING;
    @ public initially state == CONTINUING;
    @*/
  protected transient/*@ spec_public @*/byte state;
  
  /** The number of rounds of counting so far */
  //@ public invariant 0 <= lastCountNumber;
  //@ public initially lastCountNumber == 0;
  //@ public constraint \old(lastCountNumber) <= lastCountNumber;
  //@ public invariant lastCountNumber <= CountConfiguration.MAXCOUNT;
  protected transient/*@ spec_public @*/int  lastCountNumber;

  private Logger logger;
  
  public static final int                     NO_CANDIDATE    = 0;
  
  /**
   * Next available value for candidate ID number.
   */
  //@ private constraint \old(nextCandidateID) <= nextCandidateID;
  private static int                          nextCandidateID =
                                                                  MAX_CANDIDATES + 1;
  
  /**
   * Gets number of votes added or removed in this round of counting.
   * 
   * @param count
   *        This count number
   * @return A positive number if the candidate received transfers or a negative
   *         number if the candidate's surplus was distributed or the candidate
   *         was eliminated and votes transfered to another.
   */
  /*@ protected normal_behavior
    @   requires 0 <= count;
    @   requires count < CountConfiguration.MAXCOUNT;
    @   requires votesAdded.length == CountConfiguration.MAXCOUNT;
    @   requires votesRemoved.length == CountConfiguration.MAXCOUNT;
    @   ensures \result == votesAdded[count] - votesRemoved[count];
    @*/
  protected/*@ pure @*/int getVoteAtCount(final int count) {
    return (votesAdded[count] - votesRemoved[count]);
  }
  
  /**
   * Original number of votes received by this candidate before transfers due to
   * elimination or distribution of surplus votes.
   * 
   * @return Gross total of votes received
   */
  /*@ requires lastCountNumber < votesAdded.length;
    @
    @*/
  public/*@ pure @*/int getTotalVote() {
    int originalVote = 0;
    
    for (int i = 0; i <= lastCountNumber; i++) {
      originalVote += votesAdded[i];
    }
    
    return originalVote;
  }
  
  /**
   * Get status at the current round of counting; {@link #ELECTED},
   * {@link #ELIMINATED} or {@link #CONTINUING}
   * 
   * @return State value for this candidate
   */
  /*@ public normal_behavior
    @   ensures \result == state;
    @*/
  public/*@ pure @*/byte getStatus() {
    return state;
  }
  
  /**
   * Get the unique ID of this candidate.
   * 
   * @return The candidate ID number
   */
  /*@ public normal_behavior
    @   ensures \result == candidateID;
    @*/
  public/*@ pure @*/int getCandidateID() {
    return candidateID;
  }
  
  /**
   * This is the default constructor method for a <code>Candidate</code>
   */
  /*@ ensures state == CONTINUING;
    @ ensures lastCountNumber == 0;
    @*/
  public Candidate() {
    super();
    candidateID = getUniqueID();
    initialiseVotes(); //@ nowarn;
    // TODO ESC 2011.01.14 Possible violation of object invariant (Invariant)
    logger = Logger.getLogger("ie.votail.Candidate");
  }
  
  /**
  * 
  */
  protected void initialiseVotes() {
    state = CONTINUING;
    for (int i = 0; i < CountConfiguration.MAXCOUNT; i++) {
      votesAdded[i] = 0;
      votesRemoved[i] = 0;
    }
    lastCountNumber = 1;
  }
  
  /**
   * Create a <code>candidate</code> where the identifier is already known
   * 
   * @param theCandidateID
   */
  public Candidate(int theCandidateID) {
    if (0 < theCandidateID) {
      this.candidateID = theCandidateID;
    }
    else {
      this.candidateID = getUniqueID();
    }
    initialiseVotes(); //@ nowarn;
    logger = Logger.getLogger("ie.votail.Candidate");
    // TODO ESC 2011.01.14 Possible violation of object invariant
  }
  
  public static int getUniqueID() {
    return nextCandidateID++;
  }
  
  /**
   * Add a number of votes to the candidate's ballot pile.
   * 
   * @design This method cannot be called twice for the same candidate in the
   *         same round of counting.
   * @param numberOfVotes
   *        Number of votes to add
   * @param count
   *        The round of counting at which the votes were added
   */
  /*@ public normal_behavior
    @   requires state == CONTINUING;
    @   requires lastCountNumber <= count;
    @   requires 0 <= count;
    @   requires count < votesAdded.length;
    @   requires 0 <= numberOfVotes;
    @   assignable lastCountNumber, votesAdded[count];
    @   ensures numberOfVotes <= votesAdded[count];
    @   ensures lastCountNumber == count;
    @*/
  public void addVote(final int numberOfVotes, final int count) {
    votesAdded[count] += numberOfVotes;
    updateCountNumber(count);
  } //@ nowarn;
  // TODO ESC 2011.01.14 Postcondition possibly not established (Post)

  /**
   * @param count
   */
  //@ assignable lastCountNumber;
  protected void updateCountNumber(final int count) {
    if (lastCountNumber < count) {
      lastCountNumber = count;
    }
  }
  
  /**
   * Removes a number of votes from a candidates ballot stack.
   * 
   * @design This method cannot be called twice for the same candidate in the
   *         same round of counting.
   * @param numberOfVotes
   *        Number of votes to remove from this candidate
   * @param count
   *        The round of counting at which the votes were removed
   */
  /*@ public normal_behavior
    @   requires state == ELIMINATED || state == ELECTED;
    @   requires lastCountNumber <= count;
    @   requires 0 <= count;
    @   requires count < votesRemoved.length;
    @   requires 0 <= numberOfVotes;
    @   requires numberOfVotes <= getTotalAtCount(count);
    @   assignable lastCountNumber, votesRemoved[count];
    @   ensures numberOfVotes <= votesRemoved[count];
    @   ensures lastCountNumber == count;
    @*/
  public void removeVote(final int numberOfVotes, final int count) {
    votesRemoved[count] += numberOfVotes;
    updateCountNumber(count);
  } //@ nowarn Post;
  // TODO ESC 2011.01.14 Postcondition possibly not established (Post)
  
  /** Declares the candidate to be elected */
  /*@ public normal_behavior
    @   requires state == CONTINUING;
    @   assignable state, lastCountNumber;
    @   ensures state == ELECTED;
    @*/
  public void declareElected(int countNumber) {
    state = ELECTED;
    updateCountNumber(countNumber);
    logger.info("Candidate " + candidateID + " elected on count number "
        + countNumber);
  }
  
  /** Declares the candidate to be eliminated */
  /*@ public normal_behavior
    @   requires state == CONTINUING;
    @   assignable this.state;
    @   ensures state == ELIMINATED;
    @*/
  public void declareEliminated(int countNumber) {
    state = ELIMINATED;
    updateCountNumber(countNumber);
    logger.info("Candidate " + this.candidateID + " excluded on count number "<commit_msg>Incomplete - task : Extend unit tests for complete coverage - fixed build<commit_after>package election.tally;

import java.util.logging.Logger;

/**
 * The Candidate object records the number of votes received during each round
 * of counting. Votes can only be added to the candidate's stack while the
 * candidate has a status of <code>CONTINUING</code>.
 * 
 * @see <a href="http://www.cev.ie/htm/tenders/pdf/1_2.pdf"> Department of
 *      Environment and Local Government, Count Requirements and Commentary on
 *      Count Rules, section 3-14</a>
 * @author <NAME>
 */

public class Candidate extends CandidateStatus {
  
  /**
   * Maximum expected number of candidates in any one constituency.
   * 
   * @see <a
   *      href="http://en.wikipedia.org/wiki/List_of_political_parties_in_the_Republic_of_Ireland">List
   *      of political parties in Ireland</a> The average number of candidates
   *      could be much less.
   */
  public static final int                     MAX_CANDIDATES  = 20;
  
  /**
   * Identifier for the candidate. The data should be loaded in such a way that
   * the assignment of candidate IDs is fair and unbiased.
   */
  /*@ public invariant 0 <= candidateID;
    @ public constraint \old(candidateID) != NO_CANDIDATE
    @   ==> candidateID == \old(candidateID);
    @*/
  protected transient/*@ spec_public @*/int  candidateID;
  
  /** Number of votes added at each count */
  /*@ public invariant (\forall int i; 0 < i && i < votesAdded.length;
    @   0 <= votesAdded[i]);
    @ public initially (\forall int i; 0 < i && i < votesAdded.length;
    @   votesAdded[i] == 0);	
    @ public invariant votesAdded.length == CountConfiguration.MAXCOUNT;
    @*/
  protected/*@ spec_public non_null @*/int[] votesAdded      =
                                                                  new int[CountConfiguration.MAXCOUNT];
  
  /** Number of votes removed at each count */
  /*@ public invariant (\forall int i; 0 < i && i < votesRemoved.length;
    @                                  0 <= votesRemoved[i]);
    @ public initially (\forall int i; 0 < i && i < votesRemoved.length;
    @                                  votesRemoved[i] == 0);
    @ public invariant votesRemoved.length == CountConfiguration.MAXCOUNT;
    @*/
  protected/*@ spec_public non_null @*/int[] votesRemoved    =
                                                                  new int[CountConfiguration.MAXCOUNT];
  
  //@ public invariant votesAdded != votesRemoved;
  //@ public invariant votesRemoved != votesAdded;
  
  /** The status of the candidate at the latest count */
  /*@ public invariant state == ELECTED || state == ELIMINATED ||
    @   state == CONTINUING;
    @ public initially state == CONTINUING;
    @*/
  protected transient/*@ spec_public @*/byte state;
  
  /** The number of rounds of counting so far */
  //@ public invariant 0 <= lastCountNumber;
  //@ public initially lastCountNumber == 0;
  //@ public constraint \old(lastCountNumber) <= lastCountNumber;
  //@ public invariant lastCountNumber <= CountConfiguration.MAXCOUNT;
  protected transient/*@ spec_public @*/int  lastCountNumber;

  private Logger logger;
  
  public static final int                     NO_CANDIDATE    = 0;
  
  /**
   * Next available value for candidate ID number.
   */
  //@ private constraint \old(nextCandidateID) <= nextCandidateID;
  private static int                          nextCandidateID =
                                                                  MAX_CANDIDATES + 1;
  
  /**
   * Gets number of votes added or removed in this round of counting.
   * 
   * @param count
   *        This count number
   * @return A positive number if the candidate received transfers or a negative
   *         number if the candidate's surplus was distributed or the candidate
   *         was eliminated and votes transfered to another.
   */
  /*@ protected normal_behavior
    @   requires 0 <= count;
    @   requires count < CountConfiguration.MAXCOUNT;
    @   requires votesAdded.length == CountConfiguration.MAXCOUNT;
    @   requires votesRemoved.length == CountConfiguration.MAXCOUNT;
    @   ensures \result == votesAdded[count] - votesRemoved[count];
    @*/
  protected/*@ pure @*/int getVoteAtCount(final int count) {
    return (votesAdded[count] - votesRemoved[count]);
  }
  
  /**
   * Original number of votes received by this candidate before transfers due to
   * elimination or distribution of surplus votes.
   * 
   * @return Gross total of votes received
   */
  /*@ requires lastCountNumber < votesAdded.length;
    @
    @*/
  public/*@ pure @*/int getTotalVote() {
    int originalVote = 0;
    
    for (int i = 0; i <= lastCountNumber; i++) {
      originalVote += votesAdded[i];
    }
    
    return originalVote;
  }
  
  /**
    @deprecated - use getTotalVote() instead
  */
  // ensures \result == getTotalVote();
  public /*@ pure */ int getOriginalVote() {
    return getTotalVote();
  }
  
  /**
   * Get status at the current round of counting; {@link #ELECTED},
   * {@link #ELIMINATED} or {@link #CONTINUING}
   * 
   * @return State value for this candidate
   */
  /*@ public normal_behavior
    @   ensures \result == state;
    @*/
  public/*@ pure @*/byte getStatus() {
    return state;
  }
  
  /**
   * Get the unique ID of this candidate.
   * 
   * @return The candidate ID number
   */
  /*@ public normal_behavior
    @   ensures \result == candidateID;
    @*/
  public/*@ pure @*/int getCandidateID() {
    return candidateID;
  }
  
  /**
   * This is the default constructor method for a <code>Candidate</code>
   */
  /*@ ensures state == CONTINUING;
    @ ensures lastCountNumber == 0;
    @*/
  public Candidate() {
    super();
    candidateID = getUniqueID();
    initialiseVotes(); //@ nowarn;
    // TODO ESC 2011.01.14 Possible violation of object invariant (Invariant)
    logger = Logger.getLogger("ie.votail.Candidate");
  }
  
  /**
  * 
  */
  protected void initialiseVotes() {
    state = CONTINUING;
    for (int i = 0; i < CountConfiguration.MAXCOUNT; i++) {
      votesAdded[i] = 0;
      votesRemoved[i] = 0;
    }
    lastCountNumber = 1;
  }
  
  /**
   * Create a <code>candidate</code> where the identifier is already known
   * 
   * @param theCandidateID
   */
  public Candidate(int theCandidateID) {
    if (0 < theCandidateID) {
      this.candidateID = theCandidateID;
    }
    else {
      this.candidateID = getUniqueID();
    }
    initialiseVotes(); //@ nowarn;
    logger = Logger.getLogger("ie.votail.Candidate");
    // TODO ESC 2011.01.14 Possible violation of object invariant
  }
  
  public static int getUniqueID() {
    return nextCandidateID++;
  }
  
  /**
   * Add a number of votes to the candidate's ballot pile.
   * 
   * @design This method cannot be called twice for the same candidate in the
   *         same round of counting.
   * @param numberOfVotes
   *        Number of votes to add
   * @param count
   *        The round of counting at which the votes were added
   */
  /*@ public normal_behavior
    @   requires state == CONTINUING;
    @   requires lastCountNumber <= count;
    @   requires 0 <= count;
    @   requires count < votesAdded.length;
    @   requires 0 <= numberOfVotes;
    @   assignable lastCountNumber, votesAdded[count];
    @   ensures numberOfVotes <= votesAdded[count];
    @   ensures lastCountNumber == count;
    @*/
  public void addVote(final int numberOfVotes, final int count) {
    votesAdded[count] += numberOfVotes;
    updateCountNumber(count);
  } //@ nowarn;
  // TODO ESC 2011.01.14 Postcondition possibly not established (Post)

  /**
   * @param count
   */
  //@ assignable lastCountNumber;
  protected void updateCountNumber(final int count) {
    if (lastCountNumber < count) {
      lastCountNumber = count;
    }
  }
  
  /**
   * Removes a number of votes from a candidates ballot stack.
   * 
   * @design This method cannot be called twice for the same candidate in the
   *         same round of counting.
   * @param numberOfVotes
   *        Number of votes to remove from this candidate
   * @param count
   *        The round of counting at which the votes were removed
   */
  /*@ public normal_behavior
    @   requires state == ELIMINATED || state == ELECTED;
    @   requires lastCountNumber <= count;
    @   requires 0 <= count;
    @   requires count < votesRemoved.length;
    @   requires 0 <= numberOfVotes;
    @   requires numberOfVotes <= getTotalAtCount(count);
    @   assignable lastCountNumber, votesRemoved[count];
    @   ensures numberOfVotes <= votesRemoved[count];
    @   ensures lastCountNumber == count;
    @*/
  public void removeVote(final int numberOfVotes, final int count) {
    votesRemoved[count] += numberOfVotes;
    updateCountNumber(count);
  } //@ nowarn Post;
  // TODO ESC 2011.01.14 Postcondition possibly not established (Post)
  
  /** Declares the candidate to be elected */
  /*@ public normal_behavior
    @   requires state == CONTINUING;
    @   assignable state, lastCountNumber;
    @   ensures state == ELECTED;
    @*/
  public void declareElected(int countNumber) {
    state = ELECTED;
    updateCountNumber(countNumber);
    logger.info("Candidate " + candidateID + " elected on count number "
        + countNumber);
  }
  
  /** Declares the candidate to be eliminated */
  /*@ public normal_behavior
    @   requires state == CONTINUING;
    @   assignable this.state, lastCountNumber;
    @   ensures state == ELIMINATED;
    @*/
  public void declareEliminated(int countNumber) {
    state = ELIMINATED;
    updateCountNumber(countNumber);
    logger.info("Candidate " + this.candidateID + " excluded on count number "
{'fraction_non_alphanumeric': 0.10508988294314381, 'fraction_numerical': 0.006793478260869565, 'mean_word_length': 2.478822032357753, 'pattern_counts': {'":': 0, '<': 91, '<?xml version=': 0, '>': 27, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 22, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5505230', 'n_tokens_mistral': 5653, 'n_tokens_neox': 5475, 'n_words': 1687}