EventSlider Class Diagram

Ancestor class specifications:

java.lang.Object
java.awt.Component
java.awt.Container
javax.swing.JComponent
javax.swing.JSlider

EventSlider Class Specification

Invariant

An EventSlider object...

- is drawn as a line (either horizontal or vertical) with a button-like slider that can be positioned either programmatically or via a user drag action.

- should be added to a container object with its upper-left corner x pixels from the left and y pixels from the top. (The upper left corner of the container is (0, 0).)

- the outer dimensions of the text field are given by width and height.

- if necessary, the slider image is clipped to the boundaries of its GUI container.

- min and max represent, respectively, the minimum (leftmost or bottommost) and the maximum (rightmost or topmost) position of the slider image.

- min <= val <= max

- val == min + (max - min) * min_to_val_distance / min_to_max_distance

Constructor Methods

public EventSlider( int z, int mn, int mx, int v )

pre: mn <= v <= mx

and (z == HORIZONTAL or z == VERTICAL)

post: A new EventSlider object is created

and val == v and min == mn and max == mx

and (z == HORIZONTAL implies the slider is horizontally oriented)

and (z == VERTICAL implies the slider is vertically oriented)

and x == 0 and y == 0

and width == 0 and height == 0

(Note that EventSliders don't appear until added.)

Update Methods

public void setBounds( int initX, int initY, int w, int h)

post: x == initX and y == initY

and width == w and height == h

public void setLocation( int intX, int initY )

post: x == initX and y == initY

public void setSize( int w, int h )

post: width == w and height == h

public void setValue( int v )

pre: min <= v <= max

post: val == v

public void setMinimum( int m )

pre: m <= val

post: min == m

public void setMaximum( int m )

pre: val <= m

post: max == m

Query Methods

public int getX( )

post: result == x

public int getY( )

post: result == y

public int getWidth( )

post: result == width

public int getHeight( )

post: result == height

public java.awt.Container getParent( )

post: this text field is added to a Container

implies result == the Container to which this is added

and this text field is not added implies result == null

public int getMinimum( )

post: result == min

public int getMaximum( )

post: result == max

public int getValue( )

post: result == val

Event Handler Method

public abstract void stateChanged( java.awt.event.ChangeEvent e )

note: This method is called whenever this slider is dragged. The e parameter passes an associated event object. The class inheriting EventSlider must override this method.