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)