EtchedLineBorder.java

EtchedLineBorder.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

com.dmdirc.addons.ui_swing.components.EtchedLineBorder$1__static_init

Kind	Annotation Text
pre	(soft) init'ed(com.dmdirc.addons.ui_swing. components.EtchedLineBorder$BorderSide__static_ init.new EtchedLineBorder$BorderSide[](EtchedLineBo rder$BorderSide__static_init#3)[...])
presumption	com.dmdirc.addons.ui_swing.components. EtchedLineBorder_BorderSide:ordinal(...)@70 - values(...).length in range
presumption	com.dmdirc.addons.ui_swing.components. EtchedLineBorder_BorderSide:ordinal(...)@70 in {0,1}
post	new int[](EtchedLineBorder$1__static_init#1) num objects == 1

void com.dmdirc.addons.ui_swing.components.EtchedLineBorder$BorderSide(String, int)

Kind	Annotation Text

com.dmdirc.addons.ui_swing.components.EtchedLineBorder$BorderSide__static_init

Kind	Annotation Text
post	$VALUES == &new EtchedLineBorder$BorderSide[](E tchedLineBorder$BorderSide__static_init#3)
post	$VALUES.length == 2
post	$VALUES[0] == &new EtchedLineBorder$BorderSide( EtchedLineBorder$BorderSide__static_init#1)
post	$VALUES[1] == &new EtchedLineBorder$BorderSide( EtchedLineBorder$BorderSide__static_init#2)
post	BOTTOM == &new EtchedLineBorder$BorderSide(Etch edLineBorder$BorderSide__static_init#2)
post	TOP == &new EtchedLineBorder$BorderSide(EtchedL ineBorder$BorderSide__static_init#1)
post	new EtchedLineBorder$BorderSide(EtchedLineBorder$Bo rderSide__static_init#1) num objects == 1
post	new EtchedLineBorder$BorderSide(EtchedLineBorder$Bo rderSide__static_init#2) num objects == 1
post	new EtchedLineBorder$BorderSide[](EtchedLineBorder$ BorderSide__static_init#3) num objects == 1
unanalyzed	call on java.lang.Enum

void com.dmdirc.addons.ui_swing.components.EtchedLineBorder(int, EtchedLineBorder$BorderSide)

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

com.dmdirc.addons.ui_swing.components.EtchedLineBorder__static_init

Kind	Annotation Text

void paintBorder(Component, Graphics, int, int, int, int)

Kind	Annotation Text
pre	(soft) height >= -2³¹+1
pre	(soft) init'ed(com.dmdirc.addons.ui_swing. components.EtchedLineBorder$1__static_init.new int[](EtchedLineBorder$1__static_init#1)[...])
pre	(soft) width >= -2³¹+2
pre	g != null
pre	init'ed(this.etchType)
pre	this.side != null
pre	x <= 2³¹
pre	y <= 2³¹
presumption	com.dmdirc.addons.ui_swing.components. EtchedLineBorder_BorderSide:ordinal(...)@70 in {0,1}
presumption	com.dmdirc.addons.ui_swing.components. EtchedLineBorder_BorderSide:ordinal(...)@82 in {0,1}
test_vector	com.dmdirc.addons.ui_swing.components. EtchedLineBorder$1__static_init.new int[](EtchedLineBorder$1__static_init#1)[...]: {1}, {2}, {-2³¹..0, 3..2³²-1}
test_vector	this.etchType: {-2³¹..0, 2.. 2³²-1}, {1}

EtchedLineBorder$BorderSide valueOf(String)

Kind	Annotation Text
post	init'ed(return_value)

EtchedLineBorder$BorderSide[] values()

Kind	Annotation Text
pre	(soft) init'ed($VALUES[...])
post	new EtchedLineBorder$BorderSide[](values#1) num objects == 1
post	return_value == &new EtchedLineBorder$BorderSid e[](values#1)
post	return_value.length == 2
post	return_value[...] == One-of{$VALUES[...], undefined}