pt.ua.gboard
Class GBoard

java.lang.Object
  java.awt.Component
      java.awt.Container
          javax.swing.JComponent
              pt.ua.gboard.GBoard

All Implemented Interfaces:

java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable

public class GBoard
extends javax.swing.JComponent

This module implements a simplified (and yet quite powerful) graphical board. This board is build as a 2D matrix of cells accepting Gelem objects to be drawed. All drawings are persistent within the board, so once a Gelem is drawed the GBoard object will take care of its correct drawing (for example when the dimensions of the board change). Normally a Gelem uses only one cell (1x1), but it may occupy a rectangle of cells (NxM), as long as it fits inside the board.

Top-left coordinate is (0,0).

Multiple independent GBoard can be created, used, and destroyed (terminate). The last closing board will also terminate the application.

To use GBoard the normal procedure is:

1. create a new GBoard object;
2. draw/erase/move gelems in any position;
3. terminate.

invariant: numberOfLines() > 0 && numberOfColumns() > 0
invariant: numberOfLayers() > 0

This class follows DbC(tm) methodology (@see Wikipedia). Where possible, contracts are implement with JML (@see Wikipedia) and native's Java assert.

Author:

Miguel Oliveira e Silva (mos@ua.pt)

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class javax.swing.JComponent

javax.swing.JComponent.AccessibleJComponent

Nested classes/interfaces inherited from class java.awt.Component

java.awt.Component.BaselineResizeBehavior

Field Summary

Fields inherited from class javax.swing.JComponent

TOOL_TIP_TEXT_KEY, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW

Fields inherited from class java.awt.Component

BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

Fields inherited from interface java.awt.image.ImageObserver

ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH

Constructor Summary

GBoard(java.lang.String name, int numberOfLines, int numberOfColumns, int numberOfLayers)
Constructs a new GBoard with (numberOfLines x numberOfColumns) cells and numberOfLayers layers.

GBoard(java.lang.String name, int numberOfLines, int numberOfColumns, int defaultCellWidth, int defaultCellHeight, int numberOfLayers)
Constructs a new GBoard with (numberOfLines x numberOfColumns) cells and numberOfLayers layers.

Method Summary

boolean	active() Is object GBoard still active?
int	cellHeight() Returns the current height of each cell (in pixels).
int	cellWidth() Returns the current width of each cell (in pixels).
java.awt.Container	contentPane()
void	draw(Gelem gelem, int line, int column, int layer) Add and draw a gelem.
void	erase(Gelem gelem, int line, int column) Erase a gelem from position (in any layer where it exists).
void	erase(Gelem gelem, int line, int column, int layer) Erase a gelem.
void	erase(int line, int column) Erase all gelems from a position (in all layers).
void	erase(int line, int column, int minLayer, int maxLayer) Erases all gelems from a position in layers belonging to interval [minLayer, maxLayer].
void	eraseAll() Erases all drawed gelems.
void	eraseAll(int minLayer, int maxLayer) Erases all drawed gelems in layers belonging to interval [minLayer, maxLayer].
boolean	exists(Gelem gelem, int line, int column) Checks if a gelem exists in a position in any layer.
boolean	exists(Gelem gelem, int line, int column, int layer) Checks if a gelem exists in a position at a layer.
boolean	exists(Gelem gelem, int line, int column, int minLayer, int maxLayer) Checks if a gelem exists in a position in the layer interval [minLayer, maxLayer].
boolean	exists(int line, int column) Checks if any gelem exists in a position at any layer.
boolean	exists(int line, int column, int layer) Checks if any gelem exists in a position at a layer.
boolean	exists(int line, int column, int minLayer, int maxLayer) Checks if any gelem exists in a position in the layer interval [minLayer, maxLayer].
javax.swing.JFrame	frame()
boolean	gelemFitsInside(Gelem gelem, int line, int column) Checks if a gelem fits inside current GBoard
int	gelemLayer(Gelem gelem, int line, int column) Returns the topmost layer containing gelem in that position.
java.awt.Dimension	getPreferredSize()
boolean	inputListenerExists() Checks if exists an input handler.
void	move(Gelem gelem, int fromLine, int fromColumn, int toLine, int toColumn) Move gelems within the same layer.
void	move(Gelem gelem, int fromLine, int fromColumn, int fromLayer, int toLine, int toColumn, int toLayer) Move a gelem.
int	numberOfColumns() Board's number of columns.
int	numberOfLayers() Board's number of layers.
int	numberOfLines() Board's number of lines.
void	popInputHandler() Pops the board's top input handler.
void	pushInputHandler(GBoardInputHandler handler) Pushes a new board input handler.
static void	sleep(int msec) Stops thread execution for msec milliseconds.
void	terminate() Terminates the GBoard (closing also the attached window).
Gelem	topGelem(int line, int column) Returns the topest gelem at position (line,column), or null if none exists.
Gelem	topGelem(int line, int column, int minLayer, int maxLayer) Returns the topest gelem at position (line,column) in layers belonging to interval [minLayer, maxLayer], or null if none exists.
boolean	validColumn(int column) Checks if column is valid.
boolean	validLayer(int layer) Checks if layer is valid.
boolean	validLine(int line) Checks if line is valid.
boolean	validPosition(int line, int column) Checks if position is valid.

Methods inherited from class javax.swing.JComponent

addAncestorListener, addNotify, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, getAccessibleContext, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAncestorListeners, getAutoscrolls, getBaseline, getBaselineResizeBehavior, getBorder, getBounds, getClientProperty, getComponentPopupMenu, getConditionForKeyStroke, getDebugGraphicsOptions, getDefaultLocale, getFontMetrics, getGraphics, getHeight, getInheritsPopupMenu, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPopupLocation, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getToolTipText, getTopLevelAncestor, getTransferHandler, getUIClassID, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, isDoubleBuffered, isLightweightComponent, isManagingFocus, isOpaque, isOptimizedDrawingEnabled, isPaintingForPrint, isPaintingTile, isRequestFocusEnabled, isValidateRoot, paint, paintImmediately, paintImmediately, print, printAll, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setComponentPopupMenu, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, setEnabled, setFocusTraversalKeys, setFont, setForeground, setInheritsPopupMenu, setInputMap, setInputVerifier, setMaximumSize, setMinimumSize, setNextFocusableComponent, setOpaque, setPreferredSize, setRequestFocusEnabled, setToolTipText, setTransferHandler, setVerifyInputWhenFocusTarget, setVisible, unregisterKeyboardAction, update, updateUI

Methods inherited from class java.awt.Container

add, add, add, add, add, addContainerListener, addPropertyChangeListener, addPropertyChangeListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getLayout, getMousePosition, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, remove, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusCycleRoot, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setLayout, transferFocusBackward, transferFocusDownCycle, validate

Methods inherited from class java.awt.Component

action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, contains, createImage, createImage, createVolatileImage, createVolatileImage, dispatchEvent, enable, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocale, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, hide, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, 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

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

GBoard

public GBoard(java.lang.String name,
              int numberOfLines,
              int numberOfColumns,
              int numberOfLayers)

Constructs a new GBoard with (numberOfLines x numberOfColumns) cells and numberOfLayers layers. The initial dimensions of cells will be: 60x60.

requires: name != null
requires: numberOfLines >= 1 && numberOfColumns >= 1
requires: numberOfLayers >= 1

Parameters:

name - board name

numberOfLines - number of lines

numberOfColumns - number of columns

numberOfLayers - number of layers

GBoard

public GBoard(java.lang.String name,
              int numberOfLines,
              int numberOfColumns,
              int defaultCellWidth,
              int defaultCellHeight,
              int numberOfLayers)

Constructs a new GBoard with (numberOfLines x numberOfColumns) cells and numberOfLayers layers.

requires: name != null
requires: numberOfLines >= 1 && numberOfColumns >= 1
requires: defaultCellWidth >= 1 && defaultCellHeight >= 1
requires: numberOfLayers >= 1

Parameters:

name - board name

numberOfLines - number of lines

numberOfColumns - number of columns

defaultCellWidth - width in pixels of each cell

defaultCellHeight - height in pixels of each cell

numberOfLayers - number of layers

Method Detail

terminate

public void terminate()

Terminates the GBoard (closing also the attached window).

requires: active()

ensures: !active()

active

public boolean active()

Is object GBoard still active?

Returns:

boolean true if active, otherwise it returns false

numberOfLines

public int numberOfLines()

Board's number of lines.

Returns:

int number of lines

numberOfColumns

public int numberOfColumns()

Board's number of columns.

Returns:

int number of column

numberOfLayers

public int numberOfLayers()

Board's number of layers.

Returns:

int number of layers

validLine

public boolean validLine(int line)

Checks if line is valid.

Parameters:

line - the line number

Returns:

boolean true if line is valid, otherwise it returns false

validColumn

public boolean validColumn(int column)

Checks if column is valid.

Parameters:

column - the column number

Returns:

boolean true if column is valid, otherwise it returns false

validPosition

public boolean validPosition(int line,
                             int column)

Checks if position is valid.

Parameters:

line - the line number

column - the column number

Returns:

boolean true if position is valid, otherwise it returns false

validLayer

public boolean validLayer(int layer)

Checks if layer is valid.

Parameters:

layer - the layer number

Returns:

boolean true if layer is valid, otherwise it returns false

gelemFitsInside

public boolean gelemFitsInside(Gelem gelem,
                               int line,
                               int column)

Checks if a gelem fits inside current GBoard

requires: gelem != null
requires: validPosition(line, column)

Parameters:

gelem - object

line - the line number

column - the column number

Returns:

boolean true if fits inside

exists

public boolean exists(Gelem gelem,
                      int line,
                      int column,
                      int layer)

Checks if a gelem exists in a position at a layer.

requires: gelem != null
requires: validPosition(line, column)
requires: validLayer(layer)

Parameters:

gelem - object

line - the line number

column - the column number

layer - the layer number

Returns:

boolean true if exists

exists

public boolean exists(Gelem gelem,
                      int line,
                      int column,
                      int minLayer,
                      int maxLayer)

Checks if a gelem exists in a position in the layer interval [minLayer, maxLayer].

requires: gelem != null
requires: validPosition(line, column)
requires: validLayer(minLayer)
requires: validLayer(maxLayer)
requires: maxLayer >= minLayer;

Parameters:

gelem - object

line - the line number

column - the column number

minLayer - the lower layer number

maxLayer - the higher (topest) layer number

Returns:

boolean true if exists

exists

public boolean exists(Gelem gelem,
                      int line,
                      int column)

Checks if a gelem exists in a position in any layer.

requires: gelem != null
requires: validPosition(line, column)

Parameters:

gelem - object

line - the line number

column - the column number

Returns:

boolean true if exists

exists

public boolean exists(int line,
                      int column,
                      int layer)

Checks if any gelem exists in a position at a layer.

requires: validPosition(line, column)
requires: validLayer(layer)

Parameters:

line - the line number

column - the column number

layer - the layer number

Returns:

boolean true if exists

exists

public boolean exists(int line,
                      int column,
                      int minLayer,
                      int maxLayer)

Checks if any gelem exists in a position in the layer interval [minLayer, maxLayer].

requires: validPosition(line, column)
requires: validLayer(minLayer)
requires: validLayer(maxLayer)
requires: maxLayer >= minLayer;

Parameters:

line - the line number

column - the column number

minLayer - the lower layer number

maxLayer - the higher (topest) layer number

Returns:

boolean true if exists

exists

public boolean exists(int line,
                      int column)

Checks if any gelem exists in a position at any layer.

requires: validPosition(line, column)

Parameters:

line - the line number

column - the column number

Returns:

boolean true if exists

gelemLayer

public int gelemLayer(Gelem gelem,
                      int line,
                      int column)

Returns the topmost layer containing gelem in that position.

requires: exists(gelem, line, column)

ensures: validLayer(\result)

Parameters:

gelem - object

line - the line number

column - the column number

Returns:

boolean true if exists

topGelem

public Gelem topGelem(int line,
                      int column)

Returns the topest gelem at position (line,column), or null if none exists.

requires: validPosition(line, column)

Parameters:

line - the line number

column - the column number

Returns:

Gelem the gelem's reference, or null

topGelem

public Gelem topGelem(int line,
                      int column,
                      int minLayer,
                      int maxLayer)

Returns the topest gelem at position (line,column) in layers belonging to interval [minLayer, maxLayer], or null if none exists.

requires: validPosition(line, column)
requires: validLayer(minLayer)
requires: validLayer(maxLayer)
requires: maxLayer >= minLayer;

Parameters:

line - the line number

column - the column number

minLayer - the lower layer number

maxLayer - the higher (topest) layer number

Returns:

Gelem the gelem's reference, or null

move

public void move(Gelem gelem,
                 int fromLine,
                 int fromColumn,
                 int fromLayer,
                 int toLine,
                 int toColumn,
                 int toLayer)

Move a gelem.

requires: active()
requires: gelem != null
requires: validPosition(fromLine, fromColumn)
requires: validLayer(fromLayer)
requires: validPosition(toLine, toColumn)
requires: validLayer(toLayer)
requires: exists(gelem, fromLine, fromColumn, fromLayer)
requires: (fromLine == toLine && fromColumn == toColumn && fromLayer == toLayer) || !exists(gelem, toLine, toColumn, toLayer)

Parameters:

gelem - object

fromLine - the line number origin

fromColumn - the column number origin

fromLayer - the origin layer

toLine - the line number destination

toColumn - the column number destination

toLayer - the destination layer

move

public void move(Gelem gelem,
                 int fromLine,
                 int fromColumn,
                 int toLine,
                 int toColumn)

Move gelems within the same layer.

requires: active()
requires: gelem != null
requires: validPosition(fromLine, fromColumn)
requires: validPosition(toLine, toColumn)
requires: exists(gelem, fromLine, fromColumn)
requires: (fromLine == toLine && fromColumn == toColumn) || !exists(gelem, toLine, toColumn)

Parameters:

gelem - object

fromLine - the line number origin

fromColumn - the column number origin

toLine - the line number destination

toColumn - the column number destination

draw

public void draw(Gelem gelem,
                 int line,
                 int column,
                 int layer)

Add and draw a gelem.

requires: active()
requires: gelem != null
requires: validPosition(line, column)
requires: validLayer(layer)
requires: !exists(gelem, line, column, layer)
requires: gelemFitsInside(gelem, line, column)

ensures: exists(gelem, line, column, layer)

Parameters:

gelem - object

line - the line number

column - the column number

layer - the layer number

erase

public void erase(Gelem gelem,
                  int line,
                  int column,
                  int layer)

Erase a gelem.

requires: active()
requires: gelem != null
requires: validPosition(line, column)
requires: validLayer(layer)
requires: exists(gelem, line, column, layer)

ensures: !exists(gelem, line, column, layer)

Parameters:

gelem - object

line - the line number

column - the column number

layer - the layer number

erase

public void erase(Gelem gelem,
                  int line,
                  int column)

Erase a gelem from position (in any layer where it exists).

requires: active()
requires: gelem != null
requires: validPosition(line, column)
requires: exists(gelem, line, column)

ensures: !exists(gelem, line, column)

Parameters:

gelem - object

line - the line number

column - the column number

erase

public void erase(int line,
                  int column,
                  int minLayer,
                  int maxLayer)

Erases all gelems from a position in layers belonging to interval [minLayer, maxLayer].

requires: active()
requires: validPosition(line, column)
requires: validLayer(minLayer)
requires: validLayer(maxLayer)
requires: maxLayer >= minLayer;

Parameters:

line - the line number

column - the column number

minLayer - the lower layer number

maxLayer - the higher (topest) layer number

erase

public void erase(int line,
                  int column)

Erase all gelems from a position (in all layers).

requires: active()
requires: validPosition(line, column)

Parameters:

line - the line number

column - the column number

eraseAll

public void eraseAll()

Erases all drawed gelems.

requires: active()

eraseAll

public void eraseAll(int minLayer,
                     int maxLayer)

Erases all drawed gelems in layers belonging to interval [minLayer, maxLayer].

requires: active()
requires: validLayer(minLayer)
requires: validLayer(maxLayer)
requires: maxLayer >= minLayer;

Parameters:

minLayer - the lower layer number

maxLayer - the higher (topest) layer number

pushInputHandler

public void pushInputHandler(GBoardInputHandler handler)

Pushes a new board input handler.

requires: active()
requires: handler != null

Parameters:

handler - the input handler obejct's

popInputHandler

public void popInputHandler()

Pops the board's top input handler.

requires: inputListenerExists();

inputListenerExists

public boolean inputListenerExists()

Checks if exists an input handler.

Returns:

boolean true if exists

cellWidth

public int cellWidth()

Returns the current width of each cell (in pixels).

Returns:

int number of pixels

cellHeight

public int cellHeight()

Returns the current height of each cell (in pixels).

Returns:

int number of pixels

sleep

public static void sleep(int msec)

Stops thread execution for msec milliseconds.

requires: msec >= 0

ensures: not interrupted!

Parameters:

msec - duration

getPreferredSize

public java.awt.Dimension getPreferredSize()

Overrides:

getPreferredSize in class javax.swing.JComponent

frame

public javax.swing.JFrame frame()

contentPane

public java.awt.Container contentPane()