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 -231.. 232-1
post | (soft) init'ed(return_value)