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

AuditLog

public AuditLog()

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;