method	MessageType[] values()
post	return_value == &new MessageType[](values#1)
post	new MessageType[](values#1) num objects == 1
post	return_value.length == 3
post	return_value[...] == ENUM$VALUES[...]

method	MessageType valueOf(String)
post	init'ed(return_value)

method	net.sourceforge.pebble.domain.MessageType__static_ init
post	ENUM$VALUES == &new MessageType[](MessageType__ static_init#4)
post	ERROR == &new MessageType(MessageType__static_ init#3)
post	ENUM$VALUES[2] == &new MessageType(MessageType_ _static_init#3)
post	INFO == &new MessageType(MessageType__static_ init#1)
post	ENUM$VALUES[0] == &new MessageType(MessageType_ _static_init#1)
post	WARN == &new MessageType(MessageType__static_ init#2)
post	ENUM$VALUES[1] == &new MessageType(MessageType_ _static_init#2)
post	new MessageType(MessageType__static_init#1) num objects == 1
post	new MessageType(MessageType__static_init#2) num objects == 1
post	new MessageType(MessageType__static_init#3) num objects == 1
post	new MessageType[](MessageType__static_init#4) num objects == 1
post	INFO.id == &"info"
post	INFO.name == &"Info"
post	WARN.id == &"warning"
post	WARN.name == &"Warning"
post	ERROR.id == &"error"
post	ERROR.name == &"Error"
post	ENUM$VALUES.length == 3
unanalyzed	call on java.lang.Enum

method	void net.sourceforge.pebble.domain. MessageType(String, int, String, String)
post	this.id == id
post	init'ed(this.id)
post	this.name == name
post	init'ed(this.name)

method	String getId()
pre	init'ed(this.id)
post	return_value == this.id
post	init'ed(return_value)

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