method

net.sourceforge.pebble.aggregator.NewsFeed__ static_init

method	void net.sourceforge.pebble.aggregator. NewsFeed(String)
post	this.entries == &new LinkedList(NewsFeed#1)
post	init'ed(this.timestamp)
post	this.url == url
post	init'ed(this.url)
post	new LinkedList(NewsFeed#1) num objects == 1

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

method	String getTitle()
pre	init'ed(this.title)
post	return_value == this.title
post	init'ed(return_value)

method	void setTitle(String)
post	this.title == title
post	init'ed(this.title)

method	String getLink()
pre	init'ed(this.link)
post	return_value == this.link
post	init'ed(return_value)

method	void setLink(String)
post	this.link == link
post	init'ed(this.link)

method	void add(NewsFeedEntry)
pre	(soft) this.entries != null
post	entry.feed == One-of{old entry.feed, this}
test_vector	entry: Addr_Set{null}, Inverse{null}
test_vector	java.util.List:contains(...)@76: {1}, {0}

method	List getEntries()
pre	init'ed(this.entries)
post	return_value == this.entries
post	init'ed(return_value)

method	long getTimestamp()
pre	init'ed(this.timestamp)
post	return_value == this.timestamp
post	init'ed(return_value)