ServerState.java

ServerState.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

bool canTransitionTo(ServerState)

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

void com.dmdirc.ServerState(String, int, String[])

Kind	Annotation Text
post	init'ed(this.transitions)

com.dmdirc.ServerState__static_init

Kind	Annotation Text
post	$VALUES == &new ServerState[](ServerState__ static_init#15)
post	$VALUES.length == 7
post	$VALUES[0] == &new ServerState(ServerState__ static_init#1)
post	$VALUES[1] == &new ServerState(ServerState__ static_init#3)
post	$VALUES[2] == &new ServerState(ServerState__ static_init#5)
post	$VALUES[3] == &new ServerState(ServerState__ static_init#7)
post	$VALUES[4] == &new ServerState(ServerState__ static_init#9)
post	$VALUES[5] == &new ServerState(ServerState__ static_init#11)
post	$VALUES[6] == &new ServerState(ServerState__ static_init#13)
post	CLOSING == &new ServerState(ServerState__ static_init#13)
post	CONNECTED == &new ServerState(ServerState__ static_init#3)
post	CONNECTING == &new ServerState(ServerState__ static_init#1)
post	DISCONNECTED == &new ServerState(ServerState__ static_init#7)
post	DISCONNECTING == &new ServerState(ServerState__ static_init#9)
post	RECONNECT_WAIT == &new ServerState(ServerState_ _static_init#11)
post	TRANSIENTLY_DISCONNECTED == &new ServerState(ServerState__static_init#5)
post	init'ed(CLOSING.transitions)
post	init'ed(CONNECTED.transitions)
post	init'ed(CONNECTING.transitions)
post	init'ed(DISCONNECTED.transitions)
post	init'ed(DISCONNECTING.transitions)
post	init'ed(RECONNECT_WAIT.transitions)
post	init'ed(TRANSIENTLY_DISCONNECTED.transitions)
post	new ServerState(ServerState__static_init#1) num objects == 1
post	new ServerState(ServerState__static_init#11) num objects == 1
post	new ServerState(ServerState__static_init#13) num objects == 1
post	new ServerState(ServerState__static_init#3) num objects == 1
post	new ServerState(ServerState__static_init#5) num objects == 1
post	new ServerState(ServerState__static_init#7) num objects == 1
post	new ServerState(ServerState__static_init#9) num objects == 1
post	new ServerState[](ServerState__static_init#15) num objects == 1
unanalyzed	call on java.lang.Enum
unanalyzed	call on java.util.Arrays:asList

bool isDisconnected()

Kind	Annotation Text
post	init'ed(return_value)

ServerState valueOf(String)

Kind	Annotation Text
post	init'ed(return_value)

ServerState[] values()

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