SOA
© 2004 SoS Group
All Rights Reserved

sos.koa
Class MenuPanel

java.lang.Object
  extended byjava.awt.Component
      extended byjava.awt.Container
          extended byjavax.swing.JComponent
              extended byjavax.swing.JPanel
                  extended bysos.koa.MenuPanel
All Implemented Interfaces:
javax.accessibility.Accessible, java.awt.image.ImageObserver, KOAConstants, java.awt.MenuContainer, java.io.Serializable

public class MenuPanel
extends javax.swing.JPanel
implements KOAConstants

This class is the top-most class of the system and tracks and controls the overall tally process.

Version:
$Id: MenuPanel.java,v 1.63 2004/05/18 18:52:46 hubbers Exp $
Author:
Martijn Oostdijk (martijno@cs.kun.nl)

Class Specifications
invariant state == INIT_STATE||state == CLEARED_STATE||state == CANDIDATES_IMPORTED_STATE||state == VOTES_IMPORTED_STATE||state == PRIVATE_KEY_IMPORTED_STATE||state == PUBLIC_KEY_IMPORTED_STATE||state == VOTES_DECRYPTED_STATE||state == VOTES_COUNTED_STATE||state == REPORT_GENERATED_STATE;
invariant (state >= VOTES_IMPORTED_STATE ==> rawVotes != null);
invariant (state >= VOTES_COUNTED_STATE ==> voteSet != null);
invariant (state >= CANDIDATES_IMPORTED_STATE ==> candidates != null);
invariant (state >= PRIVATE_KEY_IMPORTED_STATE ==> privateKey != null);
invariant (state >= PUBLIC_KEY_IMPORTED_STATE ==> publicKey != null);
constraint \old(theInstance) == theInstance;
constraint state == INIT_STATE||state == \old(state)||state == \old(state)+1;

Nested Class Summary
 
Nested classes inherited from class javax.swing.JPanel
javax.swing.JPanel.AccessibleJPanel
 
Nested classes inherited from class javax.swing.JComponent
javax.swing.JComponent.AccessibleJComponent
 
Nested classes inherited from class java.awt.Container
java.awt.Container.AccessibleAWTContainer
 
Nested classes inherited from class java.awt.Component
java.awt.Component.AccessibleAWTComponent, java.awt.Component.BltBufferStrategy, java.awt.Component.FlipBufferStrategy
 
Field Summary
[spec_public] (package private)  CandidateList candidates
          The candidates.
(package private)  javax.swing.JButton clearButton
          GUI stuff.
(package private)  javax.swing.JButton countButton
          GUI stuff.
[spec_public] (package private)  java.io.File currentDir
          The current directory used in file browser pop-ups.
(package private)  javax.swing.JButton decryptButton
          GUI stuff.
(package private)  javax.swing.JButton exitButton
          GUI stuff.
(package private)  HelpAdapter helpAdapter
          The help window.
(package private)  javax.swing.JButton helpButton
          GUI stuff.
(package private)  javax.swing.JButton importCandidatesButton
          GUI stuff.
(package private)  javax.swing.JButton importPrivateKeyButton
          GUI stuff.
(package private)  javax.swing.JButton importPublicKeyButton
          GUI stuff.
(package private)  javax.swing.JButton importVotesButton
          GUI stuff.
[spec_public] (package private)  java.security.PrivateKey privateKey
          Private RSA key to decode the votes.
[spec_public] (package private)  java.security.PublicKey publicKey
          Public key.
[spec_public] (package private)  java.util.ArrayList rawVotes
          The (raw, imported) votes.
(package private)  javax.swing.JButton reportButton
          GUI stuff.
(package private)  javax.swing.JButton restartButton
          GUI stuff.
[spec_public] (package private)  int state
          The state of the application.
[spec_public] private static MenuPanel theInstance
          The (single) menu panel instance.
[spec_public] (package private)  VoteSet voteSet
          The counted votes.
 
Fields inherited from class javax.swing.JPanel
 
Fields inherited from class javax.swing.JComponent
accessibleContext, listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
 
Fields inherited from class java.awt.Container
 
Fields inherited from class java.awt.Component
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
 
Fields inherited from interface sos.koa.KOAConstants
ADDITIONAL_INFO_EXTRA, ADDITIONAL_INFO_MAX_HEIGHT, ADDITIONAL_INFO_MAX_WIDTH, AUDITLOG, AUDITLOG_PDF, AUDITLOG_XML, AUDITLOG_XSL, BASEDIR, CANDIDATES_IMPORTED_STATE, CLEAR_BUT_TXT, CLEAR_FAILURE_MSG, CLEAR_SUCCESS_MSG, CLEAR_TASK_MSG, CLEAR_WARNING_MSG, CLEAR_WARNING_MSG_1, CLEAR_WARNING_MSG_2, CLEARED_STATE, COUNT_BUT_TXT, COUNT_FAILURE_MSG, COUNT_SUCCESS_MSG, COUNT_TASK_MSG, COUNT_WARNING_MSG, DECRYPT_BUT_TXT, DECRYPT_ERROR_MSG, DECRYPT_ERROR_TAG, DECRYPT_FAILURE_MSG, DECRYPT_SUCCESS_MSG, DECRYPT_TASK_MSG, DECRYPT_WARNING_MSG, DECRYPTEDFILE, DEFAULT_VOTING_INTERVAL, EXIT_BUT_TXT, EXIT_FAILURE_MSG, EXIT_SUCCESS_MSG, EXIT_TASK_MSG, EXIT_WARNING_MSG, FORWARD_BACK_OPTIONS, FORWARD_MOREINFO_BACK_OPTIONS, HELP_BUT_TXT, HELP_TASK_MSG, IMPORT_CANDIDATES_BUT_TXT, IMPORT_CANDIDATES_FAILURE_MSG, IMPORT_CANDIDATES_SUCCESS_MSG, IMPORT_CANDIDATES_TASK_MSG, IMPORT_CANDIDATES_WARNING_MSG, IMPORT_KEY_FAILURE_MSG, IMPORT_KEY_SUCCESS_MSG, IMPORT_KEY_WARNING_MSG, IMPORT_PRIVATE_KEY_BUT_TXT, IMPORT_PRIVATE_KEY_TASK_MSG, IMPORT_PUBLIC_KEY_BUT_TXT, IMPORT_PUBLIC_KEY_TASK_MSG, IMPORT_VOTES_BUT_TXT, IMPORT_VOTES_FAILURE_MSG, IMPORT_VOTES_SUCCESS_MSG, IMPORT_VOTES_TASK_MSG, IMPORT_VOTES_WARNING_MSG, INIT_STATE, LESSINFO_OPTION, MAX_ENCRYPTED_VOTE_LENGTH, MAX_KEY_LENGTH, MOREINFO_OPTION, NO_ERRORS_MSG, NUMBER_OF_REDUNDANT_FIELDS, OK_CANCEL_OPTIONS, OK_LESSINFO_CANCEL_OPTIONS, OK_LESSINFO_OPTIONS, OK_MOREINFO_CANCEL_OPTIONS, OK_MOREINFO_OPTIONS, OK_OPTIONS, OUTDIR, PRIVATE_KEY_IMPORTED_STATE, PRIVATE_KEYTYPE, PUBLIC_KEY_IMPORTED_STATE, PUBLIC_KEYTYPE, RECOUNT, RECOUNT_PDF, RECOUNT_XML, RECOUNT_XSL, RELEASE, REPORT_BUT_TXT, REPORT_FAILURE_MSG, REPORT_GENERATED_STATE, REPORT_OPTIONS, REPORT_SUCCESS_MSG, REPORT_TASK_MSG, REPORT_WARNING_MSG, RESTART_BUT_TXT, RESTART_FAILURE_MSG, RESTART_SUCCESS_MSG, RESTART_TASK_MSG, RESTART_WARNING_MSG, TASK_CANCELED_MSG, TITLE, VOTES_COUNTED_STATE, VOTES_DECRYPTED_STATE, VOTES_IGNORED_SEE_MORE_INFO_MSG, VOTES_IMPORTED_STATE, YES_CANCEL_OPTIONS, YES_NO_OPTIONS
 
Fields inherited from interface java.awt.image.ImageObserver
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
 
Constructor Summary
private MenuPanel()
          Constructs a menu panel.
 
Method Summary
 void addExitButtonListener(java.awt.event.ActionListener l)
          Adds an action listener to the exit button.
 void clear()
          Clears the list of candidates, the keys, the raw votes, and the counted votes.
 CandidateList getCandidateList()
          Gets the candidate list.
(package private)  java.io.File getCurrentDir()
          Gets the current directory used in file browser pop-ups.
 java.security.PrivateKey getPrivateKey()
          Gets the imported private key or null if the key has not been imported yet.
 java.security.PublicKey getPublicKey()
          Gets the imported public key or null if the key has not been imported yet.
 java.util.ArrayList getRawVotes()
          Gets the raw votes list.
 int getState()
          Gets the current state.
static MenuPanel getTheMenuPanel()
          Static factory method to get the menu panel instance.
 VoteSet getVoteSet()
          Gets the vote set.
static void main(java.lang.String[] arg)
          Main method creates frame and calls constructor.
 void setCandidateList(CandidateList candidates)
          Sets the candidate list.
(package private)  void setCurrentDir(non_null java.io.File currentDir)
          Sets the current directory used in file browser pop-ups.
 void setEnabled(boolean b)
          Enables/disables the GUI.
private  void setEnabled(boolean b0, boolean b1, boolean b2, boolean b3, boolean b4, boolean b5, boolean b6, boolean b7, boolean b8, boolean b9)
          Enables/disables the 10 task buttons of the GUI.
 void setPrivateKey(java.security.PrivateKey privateKey)
          Sets the private key.
 void setPublicKey(java.security.PublicKey publicKey)
          Sets the public key.
 void setRawVotes(non_null java.util.ArrayList rawVotes)
          Sets the raw votes list.
 void setState(int state)
          Sets the state to state.
 void setVoteSet(VoteSet voteSet)
          Sets the vote set.
 
Methods inherited from class javax.swing.JPanel
getAccessibleContext, getUI, getUIClassID, paramString, setUI, updateUI
 
Methods inherited from class javax.swing.JComponent
addAncestorListener, addNotify, addPropertyChangeListener, addPropertyChangeListener, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, fireVetoableChange, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAncestorListeners, getAutoscrolls, getBorder, getBounds, getClientProperty, getComponentGraphics, getConditionForKeyStroke, getDebugGraphicsOptions, getDefaultLocale, getGraphics, getHeight, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPreferredSize, getPropertyChangeListeners, getPropertyChangeListeners, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getToolTipText, getTopLevelAncestor, getTransferHandler, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, isDoubleBuffered, isLightweightComponent, isManagingFocus, isMaximumSizeSet, isMinimumSizeSet, isOpaque, isOptimizedDrawingEnabled, isPaintingTile, isPreferredSizeSet, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintComponent, paintImmediately, paintImmediately, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processKeyBinding, processKeyEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, removePropertyChangeListener, removePropertyChangeListener, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, setFont, setForeground, setInputMap, setInputVerifier, setMaximumSize, setMinimumSize, setNextFocusableComponent, setOpaque, setPreferredSize, setRequestFocusEnabled, setToolTipText, setTransferHandler, setUI, setVerifyInputWhenFocusTarget, setVisible, unregisterKeyboardAction, update
 
Methods inherited from class java.awt.Container
add, add, add, add, add, addContainerListener, addImpl, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getLayout, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, processContainerEvent, processEvent, remove, remove, removeAll, removeContainerListener, setFocusCycleRoot, setFocusTraversalKeys, setFocusTraversalPolicy, setLayout, transferFocusBackward, transferFocusDownCycle, validate, validateTree
 
Methods inherited from class java.awt.Component
action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, coalesceEvents, contains, createImage, createImage, createVolatileImage, createVolatileImage, disableEvents, dispatchEvent, enable, enableEvents, enableInputMethods, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getFontMetrics, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocale, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMouseWheelListeners, getName, getParent, getPeer, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, hide, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processMouseEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, repaint, repaint, repaint, resize, resize, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setFocusable, setFocusTraversalKeysEnabled, setIgnoreRepaint, setLocale, setLocation, setLocation, setName, setSize, setSize, show, show, size, toString, transferFocus, transferFocusUpCycle
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

theInstance

private static MenuPanel theInstance
The (single) menu panel instance.

Specifications: spec_public non_null

state

int state
The state of the application.

Specifications: spec_public

restartButton

javax.swing.JButton restartButton
GUI stuff.

Specifications: non_null

clearButton

javax.swing.JButton clearButton
GUI stuff.

Specifications: non_null

importCandidatesButton

javax.swing.JButton importCandidatesButton
GUI stuff.

Specifications: non_null

importVotesButton

javax.swing.JButton importVotesButton
GUI stuff.

Specifications: non_null

importPrivateKeyButton

javax.swing.JButton importPrivateKeyButton
GUI stuff.

Specifications: non_null

importPublicKeyButton

javax.swing.JButton importPublicKeyButton
GUI stuff.

Specifications: non_null

decryptButton

javax.swing.JButton decryptButton
GUI stuff.

Specifications: non_null

countButton

javax.swing.JButton countButton
GUI stuff.

Specifications: non_null

reportButton

javax.swing.JButton reportButton
GUI stuff.

Specifications: non_null

helpButton

javax.swing.JButton helpButton
GUI stuff.

Specifications: non_null

exitButton

javax.swing.JButton exitButton
GUI stuff.

Specifications: non_null

rawVotes

java.util.ArrayList rawVotes
The (raw, imported) votes.

Specifications: spec_public

voteSet

VoteSet voteSet
The counted votes.

Specifications: spec_public

candidates

CandidateList candidates
The candidates.

Specifications: spec_public

privateKey

java.security.PrivateKey privateKey
Private RSA key to decode the votes.

Specifications: spec_public

publicKey

java.security.PublicKey publicKey
Public key.

Specifications: spec_public

currentDir

java.io.File currentDir
The current directory used in file browser pop-ups.

Specifications: spec_public non_null

helpAdapter

HelpAdapter helpAdapter
The help window.

Specifications: non_null
Constructor Detail

MenuPanel

private MenuPanel()
Constructs a menu panel. Don't use this constructor, use getTheMenuPanel instead.

Specifications:
private normal_behavior
assignable objectState;
ensures state == INIT_STATE;
Method Detail

getTheMenuPanel

public static MenuPanel getTheMenuPanel()
Static factory method to get the menu panel instance. This enforces the singleton property.

Returns:
the menu panel instance.
Specifications: pure non_null
public behavior
ensures \result == theInstance;

setCandidateList

public void setCandidateList(CandidateList candidates)
Sets the candidate list.

Parameters:
candidates - the new candidate list.
Specifications:
normal_behavior
requires candidates != null;
assignable this.candidates;
ensures state == \old(state);

getCandidateList

public CandidateList getCandidateList()
Gets the candidate list.

Returns:
the candidate list.
Specifications: pure
normal_behavior
ensures state == \old(state);

getRawVotes

public java.util.ArrayList getRawVotes()
Gets the raw votes list. The raw votes list contains byte arrays representing encrypted votes, and strings representing unencrypted votes.

Returns:
the raw voteslist.
Specifications: pure
normal_behavior
ensures state == \old(state);
ensures \result == rawVotes;

setRawVotes

public void setRawVotes(non_null java.util.ArrayList rawVotes)
Sets the raw votes list. The raw votes list contains byte arrays representing encrypted votes, and strings representing unencrypted votes.

Parameters:
rawVotes - the new raw votes list.
Specifications:
normal_behavior
assignable this.rawVotes;
ensures this.rawVotes.equals(rawVotes);

getVoteSet

public VoteSet getVoteSet()
Gets the vote set. The vote set contains counted votes.

Returns:
the vote set.
Specifications: pure
normal_behavior
ensures \result .equals(voteSet);

setVoteSet

public void setVoteSet(VoteSet voteSet)
Sets the vote set. The vote set contains counted votes.

Parameters:
voteSet - the new vote set.
Specifications:
normal_behavior
assignable this.voteSet;
ensures this.rawVotes.equals(rawVotes);

setPrivateKey

public void setPrivateKey(java.security.PrivateKey privateKey)
Sets the private key.

Parameters:
privateKey - the new private key.
Specifications:
normal_behavior
requires privateKey != null;
assignable this.privateKey;
ensures this.privateKey.equals(privateKey);

setPublicKey

public void setPublicKey(java.security.PublicKey publicKey)
Sets the public key.

Parameters:
publicKey - the new public key.
Specifications:
normal_behavior
requires publicKey != null;
assignable this.publicKey;
ensures this.publicKey.equals(publicKey);

getPrivateKey

public java.security.PrivateKey getPrivateKey()
Gets the imported private key or null if the key has not been imported yet.

Returns:
the imported private key.
Specifications: pure non_null
normal_behavior
requires state >= PRIVATE_KEY_IMPORTED_STATE;
ensures state == \old(state);

getPublicKey

public java.security.PublicKey getPublicKey()
Gets the imported public key or null if the key has not been imported yet.

Returns:
the imported public key.
Specifications: pure non_null
normal_behavior
requires state >= PUBLIC_KEY_IMPORTED_STATE;
ensures state == \old(state);

getState

public int getState()
Gets the current state.

Returns:
the current state.
Specifications: pure
normal_behavior
ensures \result == state;

setState

public void setState(int state)
Sets the state to state. This automatically changes the GUI to reflect the change in state.

Parameters:
state - the new state.
Specifications:
normal_behavior
requires state == INIT_STATE||state == CLEARED_STATE||state == CANDIDATES_IMPORTED_STATE||state == VOTES_IMPORTED_STATE||state == PRIVATE_KEY_IMPORTED_STATE||state == PUBLIC_KEY_IMPORTED_STATE||state == VOTES_DECRYPTED_STATE||state == VOTES_COUNTED_STATE||state == REPORT_GENERATED_STATE;
assignable objectState;
ensures this.state == state;

setEnabled

public void setEnabled(boolean b)
Enables/disables the GUI. When enabling, the GUI only enables those buttons that are allowed in the current state. When disabling, the GUI disables all buttons.

Overrides:
setEnabled in class javax.swing.JComponent
Parameters:
b - a boolean indicating whether to enable or disable the GUI.
Specifications:
     also
normal_behavior
assignable objectState;
ensures state == \old(state);

setEnabled

private void setEnabled(boolean b0,
                        boolean b1,
                        boolean b2,
                        boolean b3,
                        boolean b4,
                        boolean b5,
                        boolean b6,
                        boolean b7,
                        boolean b8,
                        boolean b9)
Enables/disables the 10 task buttons of the GUI.

Parameters:
b0 - a boolean indicating whether to enable or disable button 1.
b1 - a boolean indicating whether to enable or disable button 2.
b2 - a boolean indicating whether to enable or disable button 3.
b3 - a boolean indicating whether to enable or disable button 4.
b4 - a boolean indicating whether to enable or disable button 5.
b5 - a boolean indicating whether to enable or disable button 6.
b6 - a boolean indicating whether to enable or disable button 7.
b7 - a boolean indicating whether to enable or disable button 8.
b8 - a boolean indicating whether to enable or disable button 9.
b9 - a boolean indicating whether to enable or disable button 10.
Specifications:
private normal_behavior
assignable objectState;
ensures state == \old(state);

setCurrentDir

void setCurrentDir(non_null java.io.File currentDir)
Sets the current directory used in file browser pop-ups.

Parameters:
currentDir - the new current directory.
Specifications:
behavior
assignable this.currentDir;
ensures this.currentDir.equals(currentDir);
ensures state == \old(state);

getCurrentDir

java.io.File getCurrentDir()
Gets the current directory used in file browser pop-ups.

Returns:
the current directory.
Specifications: pure non_null
behavior
ensures \result .equals(currentDir);

addExitButtonListener

public void addExitButtonListener(java.awt.event.ActionListener l)
Adds an action listener to the exit button.

Parameters:
l - the action listener.
Specifications:
normal_behavior
assignable objectState;
ensures state == \old(state);

clear

public void clear()
Clears the list of candidates, the keys, the raw votes, and the counted votes.

Specifications:
normal_behavior
assignable objectState;
ensures candidates == null;
ensures rawVotes == null;
ensures voteSet == null;
ensures privateKey == null;
ensures publicKey == null;

main

public static void main(java.lang.String[] arg)
Main method creates frame and calls constructor.

Parameters:
arg - the command line arguments.

SOA
© 2004 SoS Group
All Rights Reserved