CLIParam.java

CLIParam.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void com.dmdirc.installer.cliparser.CLIParam(char, String, String)

Kind	Annotation Text
post	init'ed(this.charFlag)
post	init'ed(this.description)
post	init'ed(this.stringFlag)
post	this.charFlag == chr
post	this.description == desc
post	this.stringFlag == str

com.dmdirc.installer.cliparser.CLIParam__static_init

Kind	Annotation Text

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

String getDescription()

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

int getNumber()

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

String getString()

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

void incNumber()

Kind	Annotation Text
pre	this.number <= 2³²-2
post	this.number == old this.number + 1
post	this.number >= -2³¹+1