QueryEvents.java

QueryEvents.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	$VALUES == &new QueryEvents[](QueryEvents__ static_init#7)
post	$VALUES.length == 2
post	$VALUES[0] == &new QueryEvents(QueryEvents__ static_init#1)
post	$VALUES[1] == &new QueryEvents(QueryEvents__ static_init#4)
post	QUERY_EVENT == &new QueryEvents(QueryEvents__ static_init#1)
post	QUERY_EVENT.argNames == &new String[](QueryEven ts__static_init#2)
post	QUERY_EVENT.argNames.length == 1
post	QUERY_EVENT.argNames[0] == &"query"
post	QUERY_EVENT.argTypes == &new Class[](QueryEvent s__static_init#3)
post	QUERY_EVENT.argTypes.length == 1
post	QUERY_EVENT_WITH_ARG == &new QueryEvents(QueryE vents__static_init#4)
post	QUERY_EVENT_WITH_ARG.argNames == &new String[](QueryEvents__static_init#5)
post	QUERY_EVENT_WITH_ARG.argNames.length == 2
post	QUERY_EVENT_WITH_ARG.argNames[0] == &"query"
post	QUERY_EVENT_WITH_ARG.argNames[1] == &"message"
post	QUERY_EVENT_WITH_ARG.argTypes == &new Class[](QueryEvents__static_init#6)
post	QUERY_EVENT_WITH_ARG.argTypes.length == 2
post	new Class[](QueryEvents__static_init#3) num objects == 1
post	new Class[](QueryEvents__static_init#6) num objects == 1
post	new QueryEvents(QueryEvents__static_init#1) num objects == 1
post	new QueryEvents(QueryEvents__static_init#4) num objects == 1
post	new QueryEvents[](QueryEvents__static_init#7) num objects == 1
post	new String[](QueryEvents__static_init#2) num objects == 1
post	new String[](QueryEvents__static_init#5) num objects == 1
unanalyzed	call on java.lang.Enum

Kind	Annotation Text
pre	this.argNames != null
pre	this.argNames.length <= 2³²-1
post	return_value == this.argNames.length
post	return_value >= 0

Kind	Annotation Text
post	return_value == &"Query Events"

Kind	Annotation Text
post	init'ed(return_value)

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