method

com.dmdirc.addons.ui_swing.components. ListScroller__static_init

method	void com.dmdirc.addons.ui_swing.components. ListScroller(JList)
pre	list != null
post	init'ed(this.model)
post	init'ed(this.selectionModel)

method	void com.dmdirc.addons.ui_swing.components. ListScroller(ListModel, ListSelectionModel)
post	this.model == model
post	init'ed(this.model)
post	this.selectionModel == selectionModel
post	init'ed(this.selectionModel)

method	void mouseWheelMoved(MouseWheelEvent)
pre	e != null
pre	this.selectionModel != null
pre	(soft) this.model != null
unanalyzed	call on javax.swing.ListModel:getSize
unanalyzed	call on javax.swing.ListSelectionModel:getMinSelect ionIndex
unanalyzed	call on javax.swing.ListSelectionModel:setSelection Interval
test_vector	java.awt.event.MouseWheelEvent:getWheelRotation(... )@72: {0..232-1}, {-231..-1}

method	void changeFocus(bool)
pre	this.selectionModel != null
pre	(soft) this.model != null
presumption	javax.swing.ListSelectionModel:getMinSelectionIndex (...)@90 >= -231+1
presumption	javax.swing.ListSelectionModel:getMinSelectionIndex (...)@93 <= 232-2
unanalyzed	call on javax.swing.ListModel:getSize
test_vector	direction: {0}, {1}

method	int changeFocusUp(int)
pre	index >= -231+1
pre	(soft) this.model != null
presumption	javax.swing.ListModel:getSize(...)@109 >= -231+1
post	return_value <= 232-2
test_vector	index: {0}, {-231+1..-2, 1..232-1}, {-1}

method	int changeFocusDown(int)
pre	index <= 232-2
pre	this.model != null
post	return_value == One-of{0, index + 1}
post	return_value >= -231+1