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

method	void setName(String)
post	this.name == name
post	init'ed(this.name)

method	int getCount()
pre	init'ed(this.count)
post	return_value == this.count
post	init'ed(return_value)

method	void setCount(int)
post	this.count == count
post	init'ed(this.count)

method	String toString()
pre	init'ed(this.count)
pre	init'ed(this.name)
post	java.lang.StringBuffer:toString(...)._tainted == 0
post	return_value == &java.lang.StringBuffer:toStrin g(...)

method	int getIntensity()
pre	init'ed(this.intensity)
post	return_value == this.intensity
post	init'ed(return_value)

method	void setIntensity(int)
post	this.intensity == intensity
post	init'ed(this.intensity)