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(SwingStep)

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

void addLayoutComponent(Component, Object)

Kind	Annotation Text
pre	comp != null
pre	this.steps != null
unanalyzed	call on com.dmdirc.installer.ui.SwingStep:getTreeLo ck
unanalyzed	call on com.dmdirc.installer.ui.SwingStep:setVisibl e
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.installer.ui.SwingStep:getTreeLo ck
unanalyzed	call on com.dmdirc.installer.ui.SwingStep:setVisibl e
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.installer.ui.StepLayout()

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

void com.dmdirc.installer.ui.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.parent == null
post	this.steps == &new ArrayList(StepLayout#1)
post	this.vGap == vGap
unanalyzed	call on java.util.ArrayList

void com.dmdirc.installer.ui.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.installer.ui.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.installer.ui.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

Step getCurrentStep()

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

int getCurrentStepIndex()

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

String getCurrentStepName()

Kind	Annotation Text
pre	init'ed(this.currentStep)
pre	this.steps != null
presumption	java.util.List:get(...)@152 != null
post	init'ed(return_value)

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(...)@179 >= -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(...)@410 != null
presumption	java.awt.Container:getComponent(...)@422 != null
presumption	java.awt.Container:getHeight(...)@411 - (this.vGap*2 + insets.top@404 + insets. bottom@404) in {-2³¹..2³²-1}
presumption	java.awt.Container:getInsets(...)@404 != null
presumption	java.awt.Container:getWidth(...)@411 - (this.hGap*2 + insets.left@404 + insets. right@404) in {-2³¹..2³²-1}
presumption	this.hGap + insets.left@404 in {-2³¹.. 2³²-1}
presumption	this.hGap*2 + insets.left@404 + insets.right@404 in {-6_442_450_943..6_442_450_943}
presumption	this.hGap*2 + insets.left@404 in {-2³².. 8_589_934_590}
presumption	this.vGap + insets.top@404 in {-2³¹.. 2³²-1}
presumption	this.vGap*2 + insets.top@404 + insets.bottom@404 in {-6_442_450_943..6_442_450_943}
presumption	this.vGap*2 + insets.top@404 in {-2³².. 8_589_934_590}
test_vector	java.awt.Component:isVisible(...)@416: {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(...)@341 != null
presumption	java.awt.Container:getComponent(...)@340 != null
presumption	java.awt.Container:getInsets(...)@334 != 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(...)@313 != null
presumption	java.awt.Container:getComponent(...)@312 != null
presumption	java.awt.Container:getInsets(...)@306 != 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(...)@293 != 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(...)@290: {0}, {1}

void show(int, Container)

Kind	Annotation Text
pre	(soft) this.steps != null
pre	parent != null
presumption	java.awt.Container:getComponent(...)@228 != null
presumption	java.awt.Container:getComponent(...)@236 != null
presumption	java.util.List:size(...)@220 >= -2³¹+1
post	possibly_updated(this.currentStep)
test_vector	java.awt.Component:isVisible(...)@229: {0}, {1}
test_vector	java.util.List:size(...)@219: {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)