Messages

method

net.sourceforge.pebble.domain.Message__static_ init

method	void net.sourceforge.pebble.domain. Message(MessageType, String)
post	this.date == &new Date(Message#1)
post	init'ed(this.text)
post	this.type == type
post	init'ed(this.type)
post	new Date(Message#1) num objects == 1
unanalyzed	call on net.sourceforge.pebble.util. SecurityUtils:getUsername

method	Date getDate()
pre	init'ed(this.date)
post	return_value == this.date
post	init'ed(return_value)

method	String getText()
pre	init'ed(this.text)
post	return_value == this.text
post	init'ed(return_value)

method	void setText(String)
post	init'ed(this.text)
test_vector	net.sourceforge.pebble.util.SecurityUtils:getUserna me(...)@64: Addr_Set{null}, Inverse{null}

info method not available -- call on String net.sourceforge.pebble.util. SecurityUtils:getUsername()

method	MessageType getType()
pre	init'ed(this.type)
post	return_value == this.type
post	init'ed(return_value)

method	bool equals(Object)
pre	(soft) init'ed(o.date)
pre	(soft) init'ed(o.text)
pre	(soft) this.date != null
pre	(soft) init'ed(this.text)
post	init'ed(return_value)
test_vector	o: Inverse{null}, Addr_Set{null}
test_vector	o.text: Addr_Set{null}, Inverse{null}
test_vector	this == o: {0}, {1}
test_vector	this.text: Inverse{null}, Addr_Set{null}
test_vector	java.util.Date:equals(...)@82: {1}, {0}

method	int hashCode()
pre	this.date != null
pre	init'ed(this.text)
presumption	java.util.Date:hashCode(...)@90 in -222_153_480.. 222_153_480
presumption	java.util.Date:hashCode(...)@90*29 + java.lang.String:hashCode(...) in -2³¹.. 2³²-1
post	(soft) init'ed(return_value)