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 MenuPanel

    java.lang.Object
      java.awt.Component
          java.awt.Container
              javax.swing.JComponent
                  javax.swing.JPanel
                      sos.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.

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