Messages

method | net.sourceforge.pebble.domain.State__static_init
post | APPROVED == &new State(State__static_init#1)
post | PENDING == &new State(State__static_init#3)
post | PUBLISHED == &new State(State__static_init#5)
post | REJECTED == &new State(State__static_init#2)
post | UNPUBLISHED == &new State(State__static_ init#4)
post | new State(State__static_init#1) num objects == 1
post | new State(State__static_init#2) num objects == 1
post | new State(State__static_init#3) num objects == 1
post | new State(State__static_init#4) num objects == 1
post | new State(State__static_init#5) num objects == 1
post | APPROVED.name == &"approved"
post | REJECTED.name == &"rejected"
post | PENDING.name == &"pending"
post | UNPUBLISHED.name == &"unpublished"
post | PUBLISHED.name == &"published"

method | State getState(String)
post | return_value in Addr_Set{null,&new State(State__static_init#1),&new State(State__static_init#2),&new State(State__static_init#3),&new State(State__static_init#4),&new State(State__static_init#5)}
test_vector | name: Inverse{null}, Addr_Set{null}
test_vector | java.lang.String:equals(...)@53: {0}, {1}
test_vector | java.lang.String:equals(...)@55: {0}, {1}
test_vector | java.lang.String:equals(...)@57: {0}, {1}
test_vector | java.lang.String:equals(...)@59: {0}, {1}
test_vector | java.lang.String:equals(...)@61: {0}, {1}

method | void net.sourceforge.pebble.domain.State(String)
post | this.name == name
post | init'ed(this.name)

method | String getName()
pre | init'ed(this.name)
post | return_value == this.name
post | init'ed(return_value)

method | int hashCode()
pre | this.name != null
post | init'ed(return_value)

method | bool equals(Object)
pre | (soft) o.name != null
pre | (soft) init'ed(this.name)
post | init'ed(return_value)

method | String toString()
pre | init'ed(this.name)
post | return_value == this.name
post | init'ed(return_value)