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 AuditLog

    java.lang.Object
      sos.koa.AuditLog

public class AuditLog
extends java.lang.Object

This class is used to store all the information needed to generate the 'Verwerkingsverslag' report. In addition it is also used to store information needed for the 'Resultaat van de stemming' report.

Version:
  $Id: AuditLog.java,v 1.23 2004/05/18 18:52:46 hubbers Exp $
Author:
  Engelbert Hubbers (hubbers@cs.kun.nl)

Class Specifications
invariant votingNrOfRegisteredVoters >= importVotesNrOfVotes; invariant votingNrOfRegisteredVoters >= decryptNrOfVotes; invariant votingNrOfRegisteredVoters >= countNrOfVotes; invariant votingNrOfRegisteredVoters >= 0; invariant kiesKringen.owner == this; invariant importCandidatesNrOfLists >= 0; invariant importCandidatesNrOfCandidates >= 0; invariant importCandidatesNrOfBlanco >= 0; invariant importVotesSuccess ==> importCandidatesSuccess; invariant importVotesNrOfKieskringen >= 0; invariant importVotesNrOfVotes >= decryptNrOfVotes; invariant importVotesNrOfVotes >= countNrOfVotes; invariant importVotesNrOfVotes >= 0; invariant importPrivKeySuccess ==> importCandidatesSuccess; invariant importPrivKeySuccess ==> importVotesSuccess; invariant importPubKeySuccess ==> importCandidatesSuccess; invariant importPubKeySuccess ==> importVotesSuccess; invariant importPubKeySuccess ==> importPrivKeySuccess; invariant keypairSuccess ==> importCandidatesSuccess; invariant keypairSuccess ==> importVotesSuccess; invariant keypairSuccess ==> importPrivKeySuccess; invariant keypairSuccess ==> importPubKeySuccess; invariant decryptSuccess ==> importCandidatesSuccess; invariant decryptSuccess ==> importVotesSuccess; invariant decryptSuccess ==> importPrivKeySuccess; invariant decryptSuccess ==> importPubKeySuccess; invariant decryptSuccess ==> keypairSuccess; invariant decryptNrOfVotes >= countNrOfVotes; invariant decryptNrOfVotes >= 0; invariant countSuccess ==> importCandidatesSuccess; invariant countSuccess ==> importVotesSuccess; invariant countSuccess ==> importPrivKeySuccess; invariant countSuccess ==> importPubKeySuccess; invariant countSuccess ==> keypairSuccess; invariant countSuccess ==> decryptSuccess; invariant countNrOfVotes >= 0;

Field Summary
`[spec_public] private static java.lang.String[]` | `countErrors` List of the errors encountered during counting.
`[spec_public] private static int` | `countNrOfVotes` The number of successfully counted votes.
`[spec_public] private static boolean` | `countSuccess` To indicate whether the counting process succeeded or not.
`[spec_public] private static java.lang.String` | `countTimestampEnd` Timestamp for finish of counting.
`[spec_public] private static java.lang.String` | `countTimestampStart` Timestamp for start of counting.
`[spec_public] private static java.lang.String[]` | `decryptErrors` List of the errors encountered during decryption.
`[spec_public] private static int` | `decryptNrOfVotes` The number of successfully decrypted votes.
`[spec_public] private static boolean` | `decryptSuccess` To indicate whether the decryption process succeeded or not.
`[spec_public] private static java.lang.String` | `decryptTimestampEnd` Timestamp for finish of decrypting.
`[spec_public] private static java.lang.String` | `decryptTimestampStart` Timestamp for start of decrypting.
`[spec_public] private static java.lang.String` | `importCandidatesError` To log what went wrong during the import.
`[spec_public] private static java.lang.String` | `importCandidatesFileName` The filename of the file read.
`[spec_public] private static java.lang.String` | `importCandidatesFileTimestamp` The timestamp of the file read.
`[spec_public] private static int` | `importCandidatesNrOfBlanco` The non-negative number of 'blanco' candidates.
`[spec_public] private static int` | `importCandidatesNrOfCandidates` The non-negative number of candidates found in the file.
`[spec_public] private static int` | `importCandidatesNrOfLists` The non-negative number of kieslijsten found in the file.
`[spec_public] private static java.lang.String` | `importCandidatesRefNr` The candidates reference number.
`[spec_public] private static boolean` | `importCandidatesSuccess` To indicate whether importing the candidates succeeded or not.
`[spec_public] private static java.lang.String` | `importPrivKeyError` To log what went wrong during the import.
`[spec_public] private static java.lang.String` | `importPrivKeyFileName` The filename of the file read.
`[spec_public] private static java.lang.String` | `importPrivKeyFileTimestamp` The timestamp of the file read.
`[spec_public] private static boolean` | `importPrivKeySuccess` To indicate whether importing the private key succeeded or not.
`[spec_public] private static java.lang.String` | `importPubKeyError` To log what went wrong during the import.
`[spec_public] private static java.lang.String` | `importPubKeyFileName` The filename of the file read.
`[spec_public] private static java.lang.String` | `importPubKeyFileTimestamp` The timestamp of the file read.
`[spec_public] private static boolean` | `importPubKeySuccess` To indicate whether importing the public key succeeded or not.
`[spec_public] private static java.lang.String` | `importVotesError` To log what went wrong during the import.
`[spec_public] private static java.lang.String` | `importVotesFileName` The filename of the file read.
`[spec_public] private static java.lang.String` | `importVotesFileTimestamp` The timestamp of the file read.
`[spec_public] private static int` | `importVotesNrOfKieskringen` The number of kieskringen found in the file with the votes.
`[spec_public] private static int` | `importVotesNrOfVotes` The number of encrypted votes found in the file with the votes.
`[spec_public] private static boolean` | `importVotesSuccess` To indicate whether importing the votes succeeded or not.
`[spec_public] private static boolean` | `keypairSuccess` To indicate whether the private and public key match.
`[spec_public] private static java.util.TreeMap` | `kiesKringen` The TreeMap that is used to store the kiesKringen found in the file with the votes.
`[spec_public] private static java.lang.String` | `logTimestamp` The creation time of the audit log.
`[spec_public] private static java.lang.String` | `votingBureau` The string that contains the name of the voting bureau.
`[spec_public] private static java.lang.String` | `votingChairman` The string that contains the name of the voting chairman.
`[spec_public] private static java.lang.String` | `votingElection` The string that contains the name of the election.
`[spec_public] private static java.lang.String` | `votingElectionTimestampEnd` The string that contains the ending time of the election.
`[spec_public] private static java.lang.String` | `votingElectionTimestampStart` The string that contains the starting time of the election.
`[spec_public] private static java.lang.String` | `votingExportTimestamp` The string that contains the timestamp for the export of the votes.
`[spec_public] private static java.lang.String` | `votingInterval` The string that contains the voting interval.
`[spec_public] private static int` | `votingNrOfRegisteredVoters` The number of registered voters.
`[spec_public] private static java.lang.String` | `votingState` The string that contains the state of the voting.

Constructor Summary
`AuditLog()`

Method Summary
`static KiesKring` | `addKiesKring(byte number, non_null java.lang.String name)`
`static void` | `clear()` Resets everything to the initial values.
`static java.lang.String[]` | `getCountErrors()` Retrieve errors encountered during counting of the votes.
`static int` | `getCountNrOfVotes()` Retrieve the number of votes counted.
`static boolean` | `getCountSuccess()` Retrieve whether the count process was successful or not.
`static java.lang.String` | `getCountTimestampEnd()` Retrieve the end time of the counting process.
`static java.lang.String` | `getCountTimestampStart()` Retrieve the start time of the counting process.
`static java.lang.String` | `getCurrentTimestamp()` Get the current time.
`static java.lang.String[]` | `getDecryptErrors()` Retrieve errors encountered during decryption of the votes.
`static int` | `getDecryptNrOfVotes()` Retrieve the number of votes decrypted.
`static boolean` | `getDecryptSuccess()` Retrieve whether the decrypt process was successful or not.
`static java.lang.String` | `getDecryptTimestampEnd()` Retrieve the end time of the decryption.
`static java.lang.String` | `getDecryptTimestampStart()` Retrieve the start time of the decryption.
`static java.lang.String` | `getImportCandidatesError()` Retrieve errors encountered during the import of candidates.
`static java.lang.String` | `getImportCandidatesFileName()` Retrieve the name of the candidate file.
`static java.lang.String` | `getImportCandidatesFileTimestamp()` Retrieve modification time of the candidate file.
`static int` | `getImportCandidatesNrOfBlanco()` Retrieve the number of BLANCO candidates.
`static int` | `getImportCandidatesNrOfCandidates()` Retrieve the number of candidates.
`static int` | `getImportCandidatesNrOfLists()` Retrieve the number of candidate lists (kieslijsten).
`static java.lang.String` | `getImportCandidatesRefNr()` Retrieve the candidates reference number.
`static boolean` | `getImportCandidatesSuccess()` Retrieve whether importing the candidates was successful.
`static java.lang.String` | `getImportPrivKeyError()` Retrieve errors encountered during the import of the private key.
`static java.lang.String` | `getImportPrivKeyFileName()` Retrieve the name of the private key file.
`static java.lang.String` | `getImportPrivKeyFileTimestamp()` Retrieve modification time of the private key file.
`static boolean` | `getImportPrivKeySuccess()` Retrieve whether importing the private key was successful.
`static java.lang.String` | `getImportPubKeyError()` Retrieve errors encountered during the import of the public key.
`static java.lang.String` | `getImportPubKeyFileName()` Retrieve the name of the public key file.
`static java.lang.String` | `getImportPubKeyFileTimestamp()` Retrieve modification time of the public key file.
`static boolean` | `getImportPubKeySuccess()` Retrieve whether importing the public key was successful.
`static java.lang.String` | `getImportVotesError()` Retrieve errors encountered during the import of votes.
`static java.lang.String` | `getImportVotesFileName()` Retrieve the name of the vote file.
`static java.lang.String` | `getImportVotesFileTimestamp()` Retrieve modification time of the vote file.
`static int` | `getImportVotesNrOfKieskringen()` Retrieve the number of kieskringen.
`static int` | `getImportVotesNrOfVotes()` Retrieve the number of votes.
`static boolean` | `getImportVotesSuccess()` Retrieve whether importing the encrypted votes was successful.
`static boolean` | `getKeypairSuccess()` Retrieve whether the private key and the public key form a pair.
`static java.lang.String` | `getLogTimestamp()` Retrieve the timestamp for the creation of the audit log.
`static javax.xml.transform.Source` | `getSourceForAuditLog()` Returns a Source object for this object so it can be used as input for a JAXP transformation.
`static java.lang.String` | `getVotingBureau()` Retrieve the name of the voting bureau.
`static java.lang.String` | `getVotingChairman()` Retrieve the name of the voting chairman.
`static java.lang.String` | `getVotingElection()` Retrieve the name of the election.
`static java.lang.String` | `getVotingElectionTimestampEnd()` Retrieve the end time of the election.
`static java.lang.String` | `getVotingElectionTimestampStart()` Retrieve the start time of the election.
`static java.lang.String` | `getVotingExportTimestamp()` Retrieve the timestamp of the export of the votes.
`static java.lang.String` | `getVotingInterval()` Retrieve the voting interval.
`static int` | `getVotingNrOfRegisteredVoters()` Retrieve the number of registered voters.
`static java.lang.String` | `getVotingState()` Retrieve the voting state.
`static boolean` | `hasKiesKring(byte a_kieskring_number)`
`static void` | `setCountErrors(java.lang.String[] s)` Record errors encountered during counting of the votes.
`static void` | `setCountNrOfVotes(int i)` Record the number of votes counted.
`static void` | `setCountSuccess(boolean b)` Record whether the count process was successful or not.
`static void` | `setCountTimestampEnd(java.lang.String s)` Record the end time of the counting process.
`static void` | `setCountTimestampStart(java.lang.String s)` Record the start time of the counting process.
`static void` | `setDecryptErrors(java.lang.String[] s)` Record errors encountered during decryption of the votes.
`static void` | `setDecryptNrOfVotes(int i)` Record the number of votes decrypted.
`static void` | `setDecryptSuccess(boolean b)` Record whether the decrypt process was successful or not.
`static void` | `setDecryptTimestampEnd(java.lang.String s)` Record the end time of the decryption.
`static void` | `setDecryptTimestampStart(java.lang.String s)` Record the start time of the decryption.
`static void` | `setImportCandidatesError(java.lang.String s)` Record errors encountered during the import of candidates.
`static void` | `setImportCandidatesFileName(java.lang.String s)` Record the name of the candidate file.
`static void` | `setImportCandidatesFileTimestamp(java.lang.String s)` Record modification time of the candidate file.
`static void` | `setImportCandidatesNrOfBlanco(int i)` Record the number of BLANCO candidates.
`static void` | `setImportCandidatesNrOfCandidates(int i)` Record the number of candidates.
`static void` | `setImportCandidatesNrOfLists(int i)` Record the number of candidate lists (kieslijsten).
`static void` | `setImportCandidatesRefNr(java.lang.String s)` Record the candidates reference number.
`static void` | `setImportCandidatesSuccess(boolean b)` Record whether importing the candidates was successful.
`static void` | `setImportPrivKeyError(java.lang.String s)` Record errors encountered during the import of the private key.
`static void` | `setImportPrivKeyFileName(java.lang.String s)` Record the name of the private key file.
`static void` | `setImportPrivKeyFileTimestamp(java.lang.String s)` Record modification time of the private key file.
`static void` | `setImportPrivKeySuccess(boolean b)` Record whether importing the private key was successful.
`static void` | `setImportPubKeyError(java.lang.String s)` Record errors encountered during the import of the public key.
`static void` | `setImportPubKeyFileName(java.lang.String s)` Record the name of the public key file.
`static void` | `setImportPubKeyFileTimestamp(java.lang.String s)` Record modification time of the public key file.
`static void` | `setImportPubKeySuccess(boolean b)` Record whether importing the public key was successful.
`static void` | `setImportVotesError(java.lang.String s)` Record errors encountered during the import of votes.
`static void` | `setImportVotesFileName(java.lang.String s)` Record the name of the vote file.
`static void` | `setImportVotesFileTimestamp(java.lang.String s)` Record modification time of the vote file.
`static void` | `setImportVotesNrOfKieskringen(int i)` Record the number of kieskringen.
`static void` | `setImportVotesNrOfVotes(int i)` Record the number of votes.
`static void` | `setImportVotesSuccess(boolean b)` Record whether importing the encrypted votes was successful.
`static void` | `setKeypairSuccess(boolean b)` Record whether the private key and the public key form a pair.
`static void` | `setLogTimestamp()` Record the timestamp for the creation of the audit log.
`static void` | `setVotingBureau(java.lang.String s)` Record the name of the voting bureau.
`static void` | `setVotingChairman(java.lang.String s)` Record the name of the voting chairman.
`static void` | `setVotingElection(java.lang.String s)` Record the name of the election.
`static void` | `setVotingElectionTimestampEnd(java.lang.String s)` Record the end time of the election.
`static void` | `setVotingElectionTimestampStart(java.lang.String s)` Record the start time of the election.
`static void` | `setVotingExportTimestamp(java.lang.String s)` Record the timestamp of the export of the votes.
`static void` | `setVotingInterval(java.lang.String s)` Record the voting interval.
`static void` | `setVotingNrOfRegisteredVoters(int i)` Record the number of registered voters.
`static void` | `setVotingState(java.lang.String s)` Record the voting state.

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### logTimestamp

    private static java.lang.String logTimestamp

  The creation time of the audit log.

  Specifications: spec_public

### votingInterval

    private static java.lang.String votingInterval

  The string that contains the voting interval.

  Specifications: spec_public

### votingNrOfRegisteredVoters

    private static int votingNrOfRegisteredVoters

  The number of registered voters. We assume this non-negative number is greater or equal to the imported nr of votes from the 'stembus export'.

  Specifications: spec_public

### votingBureau

    private static java.lang.String votingBureau

  The string that contains the name of the voting bureau.

  Specifications: spec_public

### votingChairman

    private static java.lang.String votingChairman

  The string that contains the name of the voting chairman.

  Specifications: spec_public

### votingState

    private static java.lang.String votingState

  The string that contains the state of the voting.

  Specifications: spec_public

### votingElection

    private static java.lang.String votingElection

  The string that contains the name of the election.

  Specifications: spec_public

### votingElectionTimestampStart

    private static java.lang.String votingElectionTimestampStart

  The string that contains the starting time of the election.

  Specifications: spec_public

### votingElectionTimestampEnd

    private static java.lang.String votingElectionTimestampEnd

  The string that contains the ending time of the election.

  Specifications: spec_public

### votingExportTimestamp

    private static java.lang.String votingExportTimestamp

  The string that contains the timestamp for the export of the votes.

  Specifications: spec_public

### kiesKringen

    private static java.util.TreeMap kiesKringen

  The TreeMap that is used to store the kiesKringen found in the file with the votes.

  Specifications: spec_public non_null

### importCandidatesSuccess

    private static boolean importCandidatesSuccess

  To indicate whether importing the candidates succeeded or not.

  Specifications: spec_public

### importCandidatesError

    private static java.lang.String importCandidatesError

  To log what went wrong during the import.

  Specifications: spec_public

### importCandidatesFileName

    private static java.lang.String importCandidatesFileName

  The filename of the file read.

  Specifications: spec_public

### importCandidatesFileTimestamp

    private static java.lang.String importCandidatesFileTimestamp

  The timestamp of the file read.

  Specifications: spec_public

### importCandidatesRefNr

    private static java.lang.String importCandidatesRefNr

  The candidates reference number.

  Specifications: spec_public

### importCandidatesNrOfLists

    private static int importCandidatesNrOfLists

  The non-negative number of kieslijsten found in the file.

  Specifications: spec_public

### importCandidatesNrOfCandidates

    private static int importCandidatesNrOfCandidates

  The non-negative number of candidates found in the file.

  Specifications: spec_public

### importCandidatesNrOfBlanco

    private static int importCandidatesNrOfBlanco

  The non-negative number of 'blanco' candidates. Typically this should be one.

  Specifications: spec_public

### importVotesSuccess

    private static boolean importVotesSuccess

  To indicate whether importing the votes succeeded or not.

  Specifications: spec_public

### importVotesError

    private static java.lang.String importVotesError

  To log what went wrong during the import.

  Specifications: spec_public

### importVotesFileName

    private static java.lang.String importVotesFileName

  The filename of the file read.

  Specifications: spec_public

### importVotesFileTimestamp

    private static java.lang.String importVotesFileTimestamp

  The timestamp of the file read.

  Specifications: spec_public

### importVotesNrOfKieskringen

    private static int importVotesNrOfKieskringen

  The number of kieskringen found in the file with the votes.

  Specifications: spec_public

### importVotesNrOfVotes

    private static int importVotesNrOfVotes

  The number of encrypted votes found in the file with the votes. Note that this includes also malformed 'votes'.

  Specifications: spec_public

### importPrivKeySuccess

    private static boolean importPrivKeySuccess

  To indicate whether importing the private key succeeded or not.

  Specifications: spec_public

### importPrivKeyError

    private static java.lang.String importPrivKeyError

  To log what went wrong during the import.

  Specifications: spec_public

### importPrivKeyFileName

    private static java.lang.String importPrivKeyFileName

  The filename of the file read.

  Specifications: spec_public

### importPrivKeyFileTimestamp

    private static java.lang.String importPrivKeyFileTimestamp

  The timestamp of the file read.

  Specifications: spec_public

### importPubKeySuccess

    private static boolean importPubKeySuccess

  To indicate whether importing the public key succeeded or not.

  Specifications: spec_public

### importPubKeyError

    private static java.lang.String importPubKeyError

  To log what went wrong during the import.

  Specifications: spec_public

### importPubKeyFileName

    private static java.lang.String importPubKeyFileName

  The filename of the file read.

  Specifications: spec_public

### importPubKeyFileTimestamp

    private static java.lang.String importPubKeyFileTimestamp

  The timestamp of the file read.

  Specifications: spec_public

### keypairSuccess

    private static boolean keypairSuccess

  To indicate whether the private and public key match.

  Specifications: spec_public

### decryptSuccess

    private static boolean decryptSuccess

  To indicate whether the decryption process succeeded or not.

  Specifications: spec_public

### decryptErrors

    private static java.lang.String[] decryptErrors

  List of the errors encountered during decryption.

  Specifications: spec_public

### decryptTimestampStart

    private static java.lang.String decryptTimestampStart

  Timestamp for start of decrypting.

  Specifications: spec_public

### decryptTimestampEnd

    private static java.lang.String decryptTimestampEnd

  Timestamp for finish of decrypting.

  Specifications: spec_public

### decryptNrOfVotes

    private static int decryptNrOfVotes

  The number of successfully decrypted votes. This includes also possible illegal votes.

  Specifications: spec_public

### countSuccess

    private static boolean countSuccess

  To indicate whether the counting process succeeded or not.

  Specifications: spec_public

### countErrors

    private static java.lang.String[] countErrors

  List of the errors encountered during counting.

  Specifications: spec_public

### countTimestampStart

    private static java.lang.String countTimestampStart

  Timestamp for start of counting.

  Specifications: spec_public

### countTimestampEnd

    private static java.lang.String countTimestampEnd

  Timestamp for finish of counting.

  Specifications: spec_public

### countNrOfVotes

    private static int countNrOfVotes

  The number of successfully counted votes.

  Specifications: spec_public

Constructor Detail

### AuditLog

    public AuditLog()

Method Detail

### getCurrentTimestamp

    public static java.lang.String getCurrentTimestamp()

  Get the current time.

  Returns:
    the current time.
  Specifications: pure non_null

### setLogTimestamp

    public static void setLogTimestamp()

  Record the timestamp for the creation of the audit log.

  Specifications:
    normal_behavior
    requires true;
    assignable logTimestamp;
    ensures logTimestamp != null;

### getLogTimestamp

    public static java.lang.String getLogTimestamp()

  Retrieve the timestamp for the creation of the audit log.

  Returns:
    creation time of the audit log.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == logTimestamp;

### setVotingInterval

    public static void setVotingInterval(java.lang.String s)

  Record the voting interval.

  Parameters:
    `s` - the voting interval.
  Specifications:
    normal_behavior
    requires s != null;
    assignable votingInterval;
    ensures votingInterval == s;

### getVotingInterval

    public static java.lang.String getVotingInterval()

  Retrieve the voting interval.

  Returns:
    the voting interval.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == votingInterval;

### setVotingNrOfRegisteredVoters

    public static void setVotingNrOfRegisteredVoters(int i)

  Record the number of registered voters.

  Parameters:
    `i` - the number of registered voters.
  Specifications:
    normal_behavior
    requires i >= 0;
    requires i >= countNrOfVotes;
    requires i >= decryptNrOfVotes;
    requires i >= importVotesNrOfVotes;
    assignable votingNrOfRegisteredVoters;
    ensures votingNrOfRegisteredVoters == i;

### getVotingNrOfRegisteredVoters

    public static int getVotingNrOfRegisteredVoters()

  Retrieve the number of registered voters.

  Returns:
    the number of registered voters.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == votingNrOfRegisteredVoters;

### setImportCandidatesSuccess

    public static void setImportCandidatesSuccess(boolean b)

  Record whether importing the candidates was successful.

  Parameters:
    `b` - successful or not.
  Specifications:
    normal_behavior
    assignable importCandidatesSuccess;
    ensures importCandidatesSuccess == b;

### getImportCandidatesSuccess

    public static boolean getImportCandidatesSuccess()

  Retrieve whether importing the candidates was successful.

  Returns:
    successful or not.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importCandidatesSuccess;

### setImportCandidatesError

    public static void setImportCandidatesError(java.lang.String s)

  Record errors encountered during the import of candidates.

  Parameters:
    `s` - the error text.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importCandidatesError;
    ensures importCandidatesError == s;

### getImportCandidatesError

    public static java.lang.String getImportCandidatesError()

  Retrieve errors encountered during the import of candidates.

  Returns:
    the error text.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importCandidatesError;

### setImportCandidatesFileName

    public static void setImportCandidatesFileName(java.lang.String s)

  Record the name of the candidate file.

  Parameters:
    `s` - the filename.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importCandidatesFileName;
    ensures importCandidatesFileName == s;

### getImportCandidatesFileName

    public static java.lang.String getImportCandidatesFileName()

  Retrieve the name of the candidate file.

  Returns:
    the filename.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importCandidatesFileName;

### setImportCandidatesFileTimestamp

    public static void setImportCandidatesFileTimestamp(java.lang.String s)

  Record modification time of the candidate file.

  Parameters:
    `s` - the modification time.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importCandidatesFileTimestamp;
    ensures importCandidatesFileTimestamp == s;

### getImportCandidatesFileTimestamp

    public static java.lang.String getImportCandidatesFileTimestamp()

  Retrieve modification time of the candidate file.

  Returns:
    the modification time.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importCandidatesFileTimestamp;

### setImportCandidatesRefNr

    public static void setImportCandidatesRefNr(java.lang.String s)

  Record the candidates reference number.

  Parameters:
    `s` - the candidate reference number.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importCandidatesRefNr;
    ensures importCandidatesRefNr == s;

### getImportCandidatesRefNr

    public static java.lang.String getImportCandidatesRefNr()

  Retrieve the candidates reference number.

  Returns:
    the candidate reference number.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importCandidatesRefNr;

### setImportCandidatesNrOfLists

    public static void setImportCandidatesNrOfLists(int i)

  Record the number of candidate lists (kieslijsten).

  Parameters:
    `i` - the number of kieslijsten.
  Specifications:
    normal_behavior
    requires i >= 0;
    assignable importCandidatesNrOfLists;
    ensures importCandidatesNrOfLists == i;

### getImportCandidatesNrOfLists

    public static int getImportCandidatesNrOfLists()

  Retrieve the number of candidate lists (kieslijsten).

  Returns:
    the number of kieslijsten.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importCandidatesNrOfLists;

### setImportCandidatesNrOfCandidates

    public static void setImportCandidatesNrOfCandidates(int i)

  Record the number of candidates.

  Parameters:
    `i` - the number of candidates.
  Specifications:
    normal_behavior
    requires i >= 0;
    assignable importCandidatesNrOfCandidates;
    ensures importCandidatesNrOfCandidates == i;

### getImportCandidatesNrOfCandidates

    public static int getImportCandidatesNrOfCandidates()

  Retrieve the number of candidates.

  Returns:
    the number of candidates.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importCandidatesNrOfCandidates;

### setImportCandidatesNrOfBlanco

    public static void setImportCandidatesNrOfBlanco(int i)

  Record the number of BLANCO candidates.

  Parameters:
    `i` - the number of BLANCO candidates. Typically, this should be 1.
  Specifications:
    normal_behavior
    requires i >= 0;
    assignable importCandidatesNrOfBlanco;
    ensures importCandidatesNrOfBlanco == i;

### getImportCandidatesNrOfBlanco

    public static int getImportCandidatesNrOfBlanco()

  Retrieve the number of BLANCO candidates.

  Returns:
    the number of BLANCO candidates. Typically, this should be 1.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importCandidatesNrOfBlanco;

### setImportVotesSuccess

    public static void setImportVotesSuccess(boolean b)

  Record whether importing the encrypted votes was successful.

  Parameters:
    `b` - successful or not.
  Specifications:
    normal_behavior
    assignable importVotesSuccess;
    ensures importVotesSuccess == b;

### getImportVotesSuccess

    public static boolean getImportVotesSuccess()

  Retrieve whether importing the encrypted votes was successful.

  Returns:
    successful or not.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importVotesSuccess;

### setImportVotesError

    public static void setImportVotesError(java.lang.String s)

  Record errors encountered during the import of votes.

  Parameters:
    `s` - the errors.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importVotesError;
    ensures importVotesError == s;

### getImportVotesError

    public static java.lang.String getImportVotesError()

  Retrieve errors encountered during the import of votes.

  Returns:
    the errors.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importVotesError;

### setImportVotesFileName

    public static void setImportVotesFileName(java.lang.String s)

  Record the name of the vote file.

  Parameters:
    `s` - the filename.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importVotesFileName;
    ensures importVotesFileName == s;

### getImportVotesFileName

    public static java.lang.String getImportVotesFileName()

  Retrieve the name of the vote file.

  Returns:
    the filename.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importVotesFileName;

### setImportVotesFileTimestamp

    public static void setImportVotesFileTimestamp(java.lang.String s)

  Record modification time of the vote file.

  Parameters:
    `s` - the modification time.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importVotesFileTimestamp;
    ensures importVotesFileTimestamp == s;

### getImportVotesFileTimestamp

    public static java.lang.String getImportVotesFileTimestamp()

  Retrieve modification time of the vote file.

  Returns:
    the modification time.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importVotesFileTimestamp;

### setImportVotesNrOfKieskringen

    public static void setImportVotesNrOfKieskringen(int i)

  Record the number of kieskringen.

  Parameters:
    `i` - the number of kieskringen.
  Specifications:
    normal_behavior
    requires i >= 0;
    assignable importVotesNrOfKieskringen;
    ensures importVotesNrOfKieskringen == i;

### getImportVotesNrOfKieskringen

    public static int getImportVotesNrOfKieskringen()

  Retrieve the number of kieskringen.

  Returns:
    the number of kieskringen.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importVotesNrOfKieskringen;

### setImportVotesNrOfVotes

    public static void setImportVotesNrOfVotes(int i)

  Record the number of votes.

  Parameters:
    `i` - the number of votes.
  Specifications:
    normal_behavior
    requires i >= 0;
    requires votingNrOfRegisteredVoters >= i;
    requires i >= countNrOfVotes;
    requires i >= decryptNrOfVotes;
    assignable importVotesNrOfVotes;
    ensures importVotesNrOfVotes == i;

### getImportVotesNrOfVotes

    public static int getImportVotesNrOfVotes()

  Retrieve the number of votes.

  Returns:
    the number of votes.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importVotesNrOfVotes;

### setVotingBureau

    public static void setVotingBureau(java.lang.String s)

  Record the name of the voting bureau.

  Parameters:
    `s` - the voting bureau.
  Specifications:
    normal_behavior
    requires s != null;
    assignable votingBureau;
    ensures votingBureau == s;

### getVotingBureau

    public static java.lang.String getVotingBureau()

  Retrieve the name of the voting bureau.

  Returns:
    the voting bureau.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == votingBureau;

### setVotingChairman

    public static void setVotingChairman(java.lang.String s)

  Record the name of the voting chairman.

  Parameters:
    `s` - the voting chairman.
  Specifications:
    normal_behavior
    requires s != null;
    assignable votingChairman;
    ensures votingChairman == s;

### getVotingChairman

    public static java.lang.String getVotingChairman()

  Retrieve the name of the voting chairman.

  Returns:
    the voting chairman.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == votingChairman;

### setVotingState

    public static void setVotingState(java.lang.String s)

  Record the voting state.

  Parameters:
    `s` - the voting state.
  Specifications:
    normal_behavior
    requires s != null;
    assignable votingState;
    ensures votingState == s;

### getVotingState

    public static java.lang.String getVotingState()

  Retrieve the voting state.

  Returns:
    the voting state.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == votingState;

### setVotingElection

    public static void setVotingElection(java.lang.String s)

  Record the name of the election.

  Parameters:
    `s` - the election.
  Specifications:
    normal_behavior
    requires s != null;
    assignable votingElection;
    ensures votingElection == s;

### getVotingElection

    public static java.lang.String getVotingElection()

  Retrieve the name of the election.

  Returns:
    the election.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == votingElection;

### setVotingElectionTimestampStart

    public static void setVotingElectionTimestampStart(java.lang.String s)

  Record the start time of the election.

  Parameters:
    `s` - the start time of the election.
  Specifications:
    normal_behavior
    requires s != null;
    assignable votingElectionTimestampStart;
    ensures votingElectionTimestampStart == s;

### getVotingElectionTimestampStart

    public static java.lang.String getVotingElectionTimestampStart()

  Retrieve the start time of the election.

  Returns:
    the start time of the election.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == votingElectionTimestampStart;

### setVotingElectionTimestampEnd

    public static void setVotingElectionTimestampEnd(java.lang.String s)

  Record the end time of the election.

  Parameters:
    `s` - the end time of the election.
  Specifications:
    normal_behavior
    requires s != null;
    assignable votingElectionTimestampEnd;
    ensures votingElectionTimestampEnd == s;

### getVotingElectionTimestampEnd

    public static java.lang.String getVotingElectionTimestampEnd()

  Retrieve the end time of the election.

  Returns:
    the end time of the election.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == votingElectionTimestampEnd;

### setVotingExportTimestamp

    public static void setVotingExportTimestamp(java.lang.String s)

  Record the timestamp of the export of the votes.

  Parameters:
    `s` - the timestamp of the export of the votes.
  Specifications:
    normal_behavior
    requires s != null;
    assignable votingExportTimestamp;
    ensures votingExportTimestamp == s;

### getVotingExportTimestamp

    public static java.lang.String getVotingExportTimestamp()

  Retrieve the timestamp of the export of the votes.

  Returns:
    the timestamp of the export of the votes.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == votingExportTimestamp;

### setImportPrivKeySuccess

    public static void setImportPrivKeySuccess(boolean b)

  Record whether importing the private key was successful.

  Parameters:
    `b` - successful or not.
  Specifications:
    normal_behavior
    assignable importPrivKeySuccess;
    ensures importPrivKeySuccess == b;

### getImportPrivKeySuccess

    public static boolean getImportPrivKeySuccess()

  Retrieve whether importing the private key was successful.

  Returns:
    successful or not.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importPrivKeySuccess;

### setImportPrivKeyError

    public static void setImportPrivKeyError(java.lang.String s)

  Record errors encountered during the import of the private key.

  Parameters:
    `s` - the errors.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importPrivKeyError;
    ensures importPrivKeyError == s;

### getImportPrivKeyError

    public static java.lang.String getImportPrivKeyError()

  Retrieve errors encountered during the import of the private key.

  Returns:
    the errors.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importPrivKeyError;

### setImportPrivKeyFileName

    public static void setImportPrivKeyFileName(java.lang.String s)

  Record the name of the private key file.

  Parameters:
    `s` - the filename.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importPrivKeyFileName;
    ensures importPrivKeyFileName == s;

### getImportPrivKeyFileName

    public static java.lang.String getImportPrivKeyFileName()

  Retrieve the name of the private key file.

  Returns:
    the filename.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importPrivKeyFileName;

### setImportPrivKeyFileTimestamp

    public static void setImportPrivKeyFileTimestamp(java.lang.String s)

  Record modification time of the private key file.

  Parameters:
    `s` - the modification time.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importPrivKeyFileTimestamp;
    ensures importPrivKeyFileTimestamp == s;

### getImportPrivKeyFileTimestamp

    public static java.lang.String getImportPrivKeyFileTimestamp()

  Retrieve modification time of the private key file.

  Returns:
    the modification time.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importPrivKeyFileTimestamp;

### setImportPubKeySuccess

    public static void setImportPubKeySuccess(boolean b)

  Record whether importing the public key was successful.

  Parameters:
    `b` - successful or not.
  Specifications:
    normal_behavior
    assignable importPubKeySuccess;
    ensures importPubKeySuccess == b;

### getImportPubKeySuccess

    public static boolean getImportPubKeySuccess()

  Retrieve whether importing the public key was successful.

  Returns:
    successful or not.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importPubKeySuccess;

### setImportPubKeyError

    public static void setImportPubKeyError(java.lang.String s)

  Record errors encountered during the import of the public key.

  Parameters:
    `s` - the errors.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importPubKeyError;
    ensures importPubKeyError == s;

### getImportPubKeyError

    public static java.lang.String getImportPubKeyError()

  Retrieve errors encountered during the import of the public key.

  Returns:
    the errors. /*@ normal_behavior
  Specifications: pure

### setImportPubKeyFileName

    public static void setImportPubKeyFileName(java.lang.String s)

  Record the name of the public key file.

  Parameters:
    `s` - the filename.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importPubKeyFileName;
    ensures importPubKeyFileName == s;

### getImportPubKeyFileName

    public static java.lang.String getImportPubKeyFileName()

  Retrieve the name of the public key file.

  Returns:
    the filename.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importPubKeyFileName;

### setImportPubKeyFileTimestamp

    public static void setImportPubKeyFileTimestamp(java.lang.String s)

  Record modification time of the public key file.

  Parameters:
    `s` - the modification time.
  Specifications:
    normal_behavior
    requires s != null;
    assignable importPubKeyFileTimestamp;
    ensures importPubKeyFileTimestamp == s;

### getImportPubKeyFileTimestamp

    public static java.lang.String getImportPubKeyFileTimestamp()

  Retrieve modification time of the public key file.

  Returns:
    the modification time.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == importPubKeyFileTimestamp;

### setKeypairSuccess

    public static void setKeypairSuccess(boolean b)

  Record whether the private key and the public key form a pair.

  Parameters:
    `b` - successful or not.
  Specifications:
    normal_behavior
    assignable keypairSuccess;
    ensures keypairSuccess == b;

### getKeypairSuccess

    public static boolean getKeypairSuccess()

  Retrieve whether the private key and the public key form a pair.

  Returns:
    successful or not.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == keypairSuccess;

### setDecryptSuccess

    public static void setDecryptSuccess(boolean b)

  Record whether the decrypt process was successful or not.

  Parameters:
    `b` - successful or not.
  Specifications:
    normal_behavior
    assignable decryptSuccess;
    ensures decryptSuccess == b;

### getDecryptSuccess

    public static boolean getDecryptSuccess()

  Retrieve whether the decrypt process was successful or not.

  Returns:
    successful or not.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == decryptSuccess;

### setDecryptErrors

    public static void setDecryptErrors(java.lang.String[] s)

  Record errors encountered during decryption of the votes.

  Parameters:
    `s` - the errors.
  Specifications:
    normal_behavior
    requires s != null;
    assignable decryptErrors;
    ensures decryptErrors == s;

### getDecryptErrors

    public static java.lang.String[] getDecryptErrors()

  Retrieve errors encountered during decryption of the votes.

  Returns:
    the errors.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == decryptErrors;

### setDecryptTimestampStart

    public static void setDecryptTimestampStart(java.lang.String s)

  Record the start time of the decryption.

  Parameters:
    `s` - the start time of the decryption.
  Specifications:
    normal_behavior
    requires s != null;
    assignable decryptTimestampStart;
    ensures decryptTimestampStart == s;

### getDecryptTimestampStart

    public static java.lang.String getDecryptTimestampStart()

  Retrieve the start time of the decryption.

  Returns:
    the start time of the decryption.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == decryptTimestampStart;

### setDecryptTimestampEnd

    public static void setDecryptTimestampEnd(java.lang.String s)

  Record the end time of the decryption.

  Parameters:
    `s` - the end time of the decryption
  Specifications:
    normal_behavior
    requires s != null;
    assignable decryptTimestampEnd;
    ensures decryptTimestampEnd == s;

### getDecryptTimestampEnd

    public static java.lang.String getDecryptTimestampEnd()

  Retrieve the end time of the decryption.

  Returns:
    the end time of the decryption
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == decryptTimestampEnd;

### setDecryptNrOfVotes

    public static void setDecryptNrOfVotes(int i)

  Record the number of votes decrypted.

  Parameters:
    `i` - the number of votes decrypted.
  Specifications:
    normal_behavior
    requires i >= 0;
    requires importVotesNrOfVotes >= i;
    requires i >= countNrOfVotes;
    assignable decryptNrOfVotes;
    ensures decryptNrOfVotes == i;

### getDecryptNrOfVotes

    public static int getDecryptNrOfVotes()

  Retrieve the number of votes decrypted.

  Returns:
    the number of votes decrypted.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == decryptNrOfVotes;

### setCountSuccess

    public static void setCountSuccess(boolean b)

  Record whether the count process was successful or not.

  Parameters:
    `b` - successful or not.
  Specifications:
    normal_behavior
    assignable countSuccess;
    ensures countSuccess == b;

### getCountSuccess

    public static boolean getCountSuccess()

  Retrieve whether the count process was successful or not.

  Returns:
    successful or not.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == countSuccess;

### setCountErrors

    public static void setCountErrors(java.lang.String[] s)

  Record errors encountered during counting of the votes.

  Parameters:
    `s` - the errors.
  Specifications:
    normal_behavior
    requires s != null;
    assignable countErrors;
    ensures countErrors == s;

### getCountErrors

    public static java.lang.String[] getCountErrors()

  Retrieve errors encountered during counting of the votes.

  Returns:
    the errors. /*@ normal_behavior
  Specifications: pure

### setCountTimestampStart

    public static void setCountTimestampStart(java.lang.String s)

  Record the start time of the counting process.

  Parameters:
    `s` - the start time of the counting process.
  Specifications:
    normal_behavior
    requires s != null;
    assignable countTimestampStart;
    ensures countTimestampStart == s;

### getCountTimestampStart

    public static java.lang.String getCountTimestampStart()

  Retrieve the start time of the counting process.

  Returns:
    the start time of the counting process.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == countTimestampStart;

### setCountTimestampEnd

    public static void setCountTimestampEnd(java.lang.String s)

  Record the end time of the counting process.

  Parameters:
    `s` - the end time of the counting process.
  Specifications:
    normal_behavior
    requires s != null;
    assignable countTimestampEnd;
    ensures countTimestampEnd == s;

### getCountTimestampEnd

    public static java.lang.String getCountTimestampEnd()

  Retrieve the end time of the counting process.

  Returns:
    the end time of the counting process.
  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == countTimestampEnd;

### setCountNrOfVotes

    public static void setCountNrOfVotes(int i)

  Record the number of votes counted.

  Parameters:
    `i` - the number of votes counted.
  Specifications:
    normal_behavior
    requires i >= 0;
    requires i <= decryptNrOfVotes;
    assignable countNrOfVotes;
    ensures countNrOfVotes == i;

### getCountNrOfVotes

    public static int getCountNrOfVotes()

  Retrieve the number of votes counted.

  Specifications: pure
    normal_behavior
    requires true;
    ensures \result == countNrOfVotes;

### getSourceForAuditLog

    public static javax.xml.transform.Source getSourceForAuditLog()

  Returns a Source object for this object so it can be used as input for a JAXP transformation.

  Returns:
    Source The Source object
  Specifications: pure

### addKiesKring

    public static KiesKring addKiesKring(byte number,
                                         non_null java.lang.String name)

  Specifications: non_null
    normal_behavior
    requires (* all parameters must be of the proper length *);
    requires 0 <= number&&number <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;
    requires name.length() <= KiesKring.KIESKRING_NAME_MAX_LENGTH;
    assignable \everything;
    ensures (* all fields are properly initialized *);
    ensures \result .number() == number;
    ensures \result .name().equals(name);

### hasKiesKring

    public static boolean hasKiesKring(byte a_kieskring_number)

  Specifications: pure
    normal_behavior
    ensures \result ==> kiesKringen.containsKey(new Byte(a_kieskring_number));
    ensures \result <== kiesKringen.containsKey(new Byte(a_kieskring_number));

### clear

    public static void clear()

  Resets everything to the initial values.

  Specifications:
    normal_behavior
    assignable logTimestamp;
    assignable votingInterval;
    assignable votingNrOfRegisteredVoters;
    assignable votingBureau;
    assignable votingChairman;
    assignable votingState;
    assignable votingElection;
    assignable votingElectionTimestampStart;
    assignable votingElectionTimestampEnd;
    assignable votingExportTimestamp;
    assignable kiesKringen;
    assignable importCandidatesSuccess;
    assignable importCandidatesError;
    assignable importCandidatesFileName;
    assignable importCandidatesFileTimestamp;
    assignable importCandidatesRefNr;
    assignable importCandidatesNrOfLists;
    assignable importCandidatesNrOfCandidates;
    assignable importCandidatesNrOfBlanco;
    assignable importVotesSuccess;
    assignable importVotesError;
    assignable importVotesFileName;
    assignable importVotesFileTimestamp;
    assignable importVotesNrOfKieskringen;
    assignable importVotesNrOfVotes;
    assignable importPrivKeySuccess;
    assignable importPrivKeyError;
    assignable importPrivKeyFileName;
    assignable importPrivKeyFileTimestamp;
    assignable importPubKeySuccess;
    assignable importPubKeyError;
    assignable importPubKeyFileName;
    assignable importPubKeyFileTimestamp;
    assignable keypairSuccess;
    assignable decryptSuccess;
    assignable decryptErrors;
    assignable decryptTimestampStart;
    assignable decryptTimestampEnd;
    assignable decryptNrOfVotes;
    assignable countSuccess;
    assignable countErrors;
    assignable countTimestampStart;
    assignable countTimestampEnd;
    assignable countNrOfVotes;
    ensures logTimestamp.equals("");
    ensures votingInterval.equals("");
    ensures votingNrOfRegisteredVoters == 0;
    ensures votingBureau.equals("");
    ensures votingChairman.equals("");
    ensures votingState.equals("");
    ensures votingElection.equals("");
    ensures votingElectionTimestampStart.equals("");
    ensures votingElectionTimestampEnd.equals("");
    ensures votingExportTimestamp.equals("");
    ensures kiesKringen.isEmpty();
    ensures !importCandidatesSuccess;
    ensures importCandidatesError.equals("");
    ensures importCandidatesFileName.equals("");
    ensures importCandidatesFileTimestamp.equals("");
    ensures importCandidatesRefNr.equals("");
    ensures importCandidatesNrOfLists == 0;
    ensures importCandidatesNrOfCandidates == 0;
    ensures importCandidatesNrOfBlanco == 0;
    ensures !importVotesSuccess;
    ensures importVotesError.equals("");
    ensures importVotesFileName.equals("");
    ensures importVotesFileTimestamp.equals("");
    ensures importVotesNrOfKieskringen == 0;
    ensures importVotesNrOfVotes == 0;
    ensures !importPrivKeySuccess;
    ensures importPrivKeyError.equals("");
    ensures importPrivKeyFileName.equals("");
    ensures importPrivKeyFileTimestamp.equals("");
    ensures !importPubKeySuccess;
    ensures importPubKeyError.equals("");
    ensures importPubKeyFileName.equals("");
    ensures importPubKeyFileTimestamp.equals("");
    ensures !keypairSuccess;
    ensures !decryptSuccess;
    ensures decryptErrors == null;
    ensures decryptTimestampStart.equals("");
    ensures decryptTimestampEnd.equals("");
    ensures decryptNrOfVotes == 0;
    ensures !countSuccess;
    ensures countErrors == null;
    ensures countTimestampStart.equals("");
    ensures countTimestampEnd.equals("");
    ensures countNrOfVotes == 0;

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