StepLayout.java

StepLayout.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void addLayoutComponent(Step)

Kind	Annotation Text
pre	step != null
pre	this.steps != null
test_vector	java.util.List:isEmpty(...)@251: {1}, {0}

void addLayoutComponent(Component, Object)

Kind	Annotation Text
pre	comp != null
pre	this.steps != null
unanalyzed	call on com.dmdirc.addons.ui_swing.wizard. Step:getTreeLock
unanalyzed	call on com.dmdirc.addons.ui_swing.wizard. Step:setVisible
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:isEmpty

void addLayoutComponent(String, Component)

Kind	Annotation Text
pre	comp != null
pre	this.steps != null
unanalyzed	call on com.dmdirc.addons.ui_swing.wizard. Step:getTreeLock
unanalyzed	call on com.dmdirc.addons.ui_swing.wizard. Step:setVisible
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.List:isEmpty

void com.dmdirc.addons.ui_swing.wizard.StepLayout()

Kind	Annotation Text
post	new ArrayList(StepLayout#1) num objects == 1
post	this.currentStep == -1
post	this.hGap == 0
post	this.steps == &new ArrayList(StepLayout#1)
post	this.vGap == 0
unanalyzed	call on java.util.ArrayList

void com.dmdirc.addons.ui_swing.wizard.StepLayout(int, int)

Kind	Annotation Text
post	init'ed(this.hGap)
post	init'ed(this.vGap)
post	new ArrayList(StepLayout#1) num objects == 1
post	this.currentStep == -1
post	this.hGap == hGap
post	this.steps == &new ArrayList(StepLayout#1)
post	this.vGap == vGap

void com.dmdirc.addons.ui_swing.wizard.StepLayout(int, int, Container)

Kind	Annotation Text
post	init'ed(this.hGap)
post	init'ed(this.parent)
post	init'ed(this.vGap)
post	new ArrayList(StepLayout#1) num objects == 1
post	this.currentStep == -1
post	this.hGap == hGap
post	this.parent == parent
post	this.steps == &new ArrayList(StepLayout#1)
post	this.vGap == vGap

void com.dmdirc.addons.ui_swing.wizard.StepLayout(Container)

Kind	Annotation Text
post	init'ed(this.parent)
post	new ArrayList(StepLayout#1) num objects == 1
post	this.currentStep == -1
post	this.hGap == 0
post	this.parent == parent
post	this.steps == &new ArrayList(StepLayout#1)
post	this.vGap == 0
unanalyzed	call on java.util.ArrayList

com.dmdirc.addons.ui_swing.wizard.StepLayout__static_init

Kind	Annotation Text

void first(Container)

Kind	Annotation Text
pre	(soft) this.steps != null
pre	parent != null
post	possibly_updated(this.currentStep)
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:validate
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:size

float getLayoutAlignmentX(Container)

Kind	Annotation Text
post	return_value == 1/2

float getLayoutAlignmentY(Container)

Kind	Annotation Text
post	return_value == 1/2

Step getStep(int)

Kind	Annotation Text
pre	this.steps != null
post	init'ed(return_value)

List getSteps()

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

void invalidateLayout(Container)

Kind	Annotation Text

bool isEmpty()

Kind	Annotation Text
pre	this.steps != null
post	init'ed(return_value)

void last(Container)

Kind	Annotation Text
pre	(soft) this.steps != null
pre	parent != null
presumption	java.awt.Container:getComponentCount(...)@153 >= -2³¹+1
post	possibly_updated(this.currentStep)
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:validate
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:size

void layoutContainer(Container)

Kind	Annotation Text
pre	(soft) init'ed(this.hGap)
pre	(soft) init'ed(this.vGap)
pre	parent != null
presumption	java.awt.Container:getComponent(...)@382 != null
presumption	java.awt.Container:getComponent(...)@393 != null
presumption	java.awt.Container:getHeight(...)@383 - (this.vGap*2 + insets.top@376 + insets. bottom@376) in {-2³¹..2³²-1}
presumption	java.awt.Container:getInsets(...)@376 != null
presumption	java.awt.Container:getWidth(...)@383 - (this.hGap*2 + insets.left@376 + insets. right@376) in {-2³¹..2³²-1}
presumption	this.hGap + insets.left@376 in {-2³¹.. 2³²-1}
presumption	this.hGap*2 + insets.left@376 + insets.right@376 in {-6_442_450_943..6_442_450_943}
presumption	this.hGap*2 + insets.left@376 in {-2³².. 8_589_934_590}
presumption	this.vGap + insets.top@376 in {-2³¹.. 2³²-1}
presumption	this.vGap*2 + insets.top@376 + insets.bottom@376 in {-6_442_450_943..6_442_450_943}
presumption	this.vGap*2 + insets.top@376 in {-2³².. 8_589_934_590}
test_vector	java.awt.Component:isVisible(...)@387: {0}, {1}

Dimension maximumLayoutSize(Container)

Kind	Annotation Text
post	new Dimension(maximumLayoutSize#1) num objects == 1
post	return_value == &new Dimension(maximumLayoutSiz e#1)

Dimension minimumLayoutSize(Container)

Kind	Annotation Text
pre	init'ed(this.hGap)
pre	init'ed(this.vGap)
pre	parent != null
presumption	java.awt.Component:getMinimumSize(...)@313 != null
presumption	java.awt.Container:getComponent(...)@312 != null
presumption	java.awt.Container:getInsets(...)@306 != null
post	new Dimension(minimumLayoutSize#1) num objects == 1
post	return_value == &new Dimension(minimumLayoutSiz e#1)

void next(Container)

Kind	Annotation Text
pre	(soft) this.steps != null
pre	parent != null
pre	this.currentStep <= 2³²-2
post	init'ed(this.currentStep)
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:validate
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:size

Dimension preferredLayoutSize(Container)

Kind	Annotation Text
pre	init'ed(this.hGap)
pre	init'ed(this.vGap)
pre	parent != null
presumption	java.awt.Component:getPreferredSize(...)@285 != null
presumption	java.awt.Container:getComponent(...)@284 != null
presumption	java.awt.Container:getInsets(...)@278 != null
post	new Dimension(preferredLayoutSize#1) num objects == 1
post	return_value == &new Dimension(preferredLayoutS ize#1)

void previous(Container)

Kind	Annotation Text
pre	(soft) this.steps != null
pre	parent != null
pre	this.currentStep >= -2³¹+1
post	init'ed(this.currentStep)
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:validate
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:size

void removeLayoutComponent(Component)

Kind	Annotation Text
pre	(soft) this.steps != null
pre	comp != null
pre	this.currentStep <= 2³²-2
presumption	java.awt.Component:getParent(...)@265 != null
post	init'ed(this.currentStep)
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:validate
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:size
test_vector	java.awt.Component:isVisible(...)@262: {0}, {1}

void show(int, Container)

Kind	Annotation Text
pre	(soft) this.steps != null
pre	parent != null
presumption	java.awt.Container:getComponent(...)@202 != null
presumption	java.awt.Container:getComponent(...)@210 != null
presumption	java.util.List:size(...)@194 >= -2³¹+1
post	possibly_updated(this.currentStep)
test_vector	java.awt.Component:isVisible(...)@203: {0}, {1}
test_vector	java.util.List:size(...)@193: {0..2³²-1}, {-2³¹..-1}
test_vector	step: {-2³¹..-2, 0..2³²-1}, {-1}

void show(Step, Container)

Kind	Annotation Text
pre	parent != null
pre	this.steps != null
post	possibly_updated(this.currentStep)
unanalyzed	call on java.awt.Component:isVisible
unanalyzed	call on java.awt.Component:setVisible
unanalyzed	call on java.awt.Container:getComponent
unanalyzed	call on java.awt.Container:getComponentCount
unanalyzed	call on java.awt.Container:getTreeLock
unanalyzed	call on java.awt.Container:validate
unanalyzed	call on java.lang.Throwable:__curr_excep_obj
unanalyzed	call on java.util.List:size

int size()

Kind	Annotation Text
pre	this.steps != null
post	init'ed(return_value)