Messages

Last Msg First Msg

method

com.dmdirc.parser.irc.IRCStringConverter__static_ init

method	void com.dmdirc.parser.irc.IRCStringConverter()
post	this.limit == 4
post	this.lowercase == &new char[](IRCStringConverte r#1)
post	this.uppercase == &new char[](IRCStringConverte r#2)
post	new char[](IRCStringConverter#1) num objects == 1
post	new char[](IRCStringConverter#2) num objects == 1
post	new char[](IRCStringConverter#1).length == 127
post	new char[](IRCStringConverter#2).length == 127
post	possibly_updated(new char[](IRCStringConverter#1)[...])
post	possibly_updated(new char[](IRCStringConverter#2)[...])

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

method	int getLimit()
post	return_value == this.limit
post	return_value in {-128..255}

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

Prev Msg Next Msg

test always goes same way

click for all messages in this file Low Prob.

Test predetermined because init'ed(result[i])

Prev Msg Next Msg

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

Prev Msg Next Msg

test always goes same way

click for all messages in this file Low Prob.

Test predetermined because init'ed(result[i])

Prev Msg Next Msg

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