method

net.sourceforge.pebble.domain.Attachment__static_ init

method

void net.sourceforge.pebble.domain.Attachment()

method	void net.sourceforge.pebble.domain. Attachment(String, long, String)
post	this.size == size
post	init'ed(this.size)
post	this.type == type
post	init'ed(this.type)
post	this.url == url
post	init'ed(this.url)

method	String getUrl()
pre	init'ed(this.url)
post	return_value == this.url
post	init'ed(return_value)

method	void setUrl(String)
post	this.url == url
post	init'ed(this.url)

method	long getSize()
pre	init'ed(this.size)
post	return_value == this.size
post	init'ed(return_value)

method	void setSize(long)
post	this.size == size
post	init'ed(this.size)

method	String getType()
pre	init'ed(this.type)
post	return_value == this.type
post	init'ed(return_value)

method	void setType(String)
post	this.type == type
post	init'ed(this.type)

method	bool equals(Object)
pre	(soft) init'ed(o.url)
pre	(soft) init'ed(this.url)
post	init'ed(return_value)
test_vector	o.url: Addr_Set{null}, Inverse{null}
test_vector	this == o: {0}, {1}
test_vector	this.url: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:length(...)@135: {1.. 232-1}, {0}
test_vector	java.lang.String:length(...)@136: {0}, {1..232-1}

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

method	Object clone()
pre	init'ed(this.size)
pre	init'ed(this.type)
pre	init'ed(this.url)
post	return_value == &new Attachment(clone#1)
post	new Attachment(clone#1) num objects == 1
post	return_value.size == this.size
post	init'ed(return_value.size)
post	return_value.type == this.type
post	init'ed(return_value.type)
post	return_value.url == this.url
post	init'ed(return_value.url)