IRCStringConverter.java

IRCStringConverter.java

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

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

void com.dmdirc.parser.irc.IRCStringConverter()

Kind	Annotation Text
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2) num objects == 1
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])
post	this.limit == 4
post	this.lowercase == &new char[](IRCStringConverte r#1)
post	this.uppercase == &new char[](IRCStringConverte r#2)

void com.dmdirc.parser.irc.IRCStringConverter(byte)

Kind	Annotation Text
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#2) num objects == 1
post	this.limit == One-of{4, limit}
post	this.limit in {0..4}
post	this.lowercase == &new char[](IRCStringConverte r#1)
post	this.lowercase.length == 127
post	this.lowercase[...] == One-of{VN37:[...] + 32, this.lowercase[...]}
post	this.uppercase == &new char[](IRCStringConverte r#2)
post	this.uppercase.length == 127
post	this.uppercase[...] == One-of{VN42:[...] - 32, this.uppercase[...]}
test_vector	limit: {5..255}, {0..4}, {-128..-1}

com.dmdirc.parser.irc.IRCStringConverter__static_init

Kind	Annotation Text

bool equalsIgnoreCase(String, String)

Kind	Annotation Text
pre	(soft) init'ed(this.lowercase[...])
pre	(soft) this.lowercase != null
pre	(soft) this.lowercase.length >= 1
presumption	firstChar[i]@127 < this.lowercase.length
presumption	java.lang.String:length(...)@129 <= firstChar.length@127
presumption	java.lang.String:length(...)@129 <= secondChar.length@128
presumption	secondChar.length@128 >= 1
presumption	secondChar[i]@128 < this.lowercase.length
post	init'ed(return_value)
test_vector	first: Inverse{null}, Addr_Set{null}
test_vector	firstChar[i]@127 - this.lowercase.length: {0..2¹⁶-2}, {-2¹⁶+1..-1}
test_vector	second: Inverse{null}, Addr_Set{null}
test_vector	secondChar[i]@128 - this.lowercase.length: {0..2¹⁶-2}, {-Inf..-1}

Kind	Annotation Text
post	return_value == this.limit
post	return_value in {-128..255}

String toLowerCase(String)

Kind	Annotation Text
pre	(soft) init'ed(this.lowercase[...])
pre	(soft) this.lowercase != null
pre	input != null
presumption	java.lang.String:length(...)@87 <= result. length@86
presumption	result.length@86 >= 1
post	new String(toLowerCase#1) num objects == 1
post	return_value == &new String(toLowerCase#1)

String toUpperCase(String)

Kind	Annotation Text
pre	(soft) init'ed(this.uppercase[...])
pre	(soft) this.uppercase != null
pre	input != null
presumption	java.lang.String:length(...)@105 <= result.length@104
presumption	result.length@104 >= 1
post	new String(toUpperCase#1) num objects == 1
post	return_value == &new String(toUpperCase#1)