WizardControlPanel.java

WizardControlPanel.java

current inspection = 2009-09-03 21:56:13 (id #1)

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

Kind	Annotation Text
post	init'ed(this.step)
post	new JButton(WizardControlPanel#1) num objects == 1
post	new JButton(WizardControlPanel#2) num objects == 1
post	new JLabel(WizardControlPanel#3) num objects == 1
post	this.next == &new JButton(WizardControlPanel#2)
post	this.prev == &new JButton(WizardControlPanel#1)
post	this.progress == &new JLabel(WizardControlPanel #3)
post	this.total == 0
unanalyzed	call on com.dmdirc.installer.ui.WizardControlPanel: add
unanalyzed	call on com.dmdirc.installer.ui.WizardControlPanel: setBorder
unanalyzed	call on com.dmdirc.installer.ui.WizardControlPanel: setLayout
unanalyzed	call on java.awt.Dimension
unanalyzed	call on java.awt.Font:getSize
unanalyzed	call on javax.swing.Box:createHorizontalGlue
unanalyzed	call on javax.swing.Box:createHorizontalStrut
unanalyzed	call on javax.swing.BoxLayout
unanalyzed	call on javax.swing.JButton
unanalyzed	call on javax.swing.JButton:getFont
unanalyzed	call on javax.swing.JButton:setPreferredSize
unanalyzed	call on javax.swing.JLabel
unanalyzed	call on javax.swing.JLabel:setText
unanalyzed	call on javax.swing.JPanel
unanalyzed	call on javax.swing.border.EtchedBorder

Kind	Annotation Text
presumption	java.awt.Font:getSize(...)@69 <= 4_294_967_285
presumption	java.awt.Font:getSize(...)@70 <= 4_294_967_285
presumption	javax.swing.JButton:getFont(...)@69 != null
presumption	javax.swing.JButton:getFont(...)@70 != null
post	init'ed(this.step)
post	init'ed(this.total)
post	new JButton(WizardControlPanel#1) num objects == 1
post	new JButton(WizardControlPanel#2) num objects == 1
post	new JLabel(WizardControlPanel#3) num objects == 1
post	this.next == &new JButton(WizardControlPanel#2)
post	this.prev == &new JButton(WizardControlPanel#1)
post	this.progress == &new JLabel(WizardControlPanel #3)
post	this.total == total
unanalyzed	call on javax.swing.JLabel:setText
unanalyzed	call on javax.swing.border.EtchedBorder

Kind	Annotation Text

Kind	Annotation Text
post	init'ed(return_value)
post	return_value == this.next

Kind	Annotation Text
post	init'ed(return_value)
post	return_value == this.prev

Kind	Annotation Text
post	init'ed(return_value)
post	return_value == this.progress

Kind	Annotation Text
pre	(soft) this.next != null
pre	(soft) this.prev != null
pre	init'ed(this.total)
pre	step <= 2³²-2
pre	this.progress != null
post	this.step == step + 1
post	this.step >= -2³¹+1
unanalyzed	call on javax.swing.JLabel:setText
test_vector	step: {-2³¹..-1}, {0}, {1.. 2³²-2}
test_vector	this.total - step: {-2³¹+1..0, 2..2³²-2}, {1}

Kind	Annotation Text
pre	init'ed(this.step)
pre	this.progress != null
post	init'ed(this.total)
post	this.total == total
unanalyzed	call on javax.swing.JLabel:setText