method

net.sourceforge.pebble.index.IndexedTag__static_ init

method	void net.sourceforge.pebble.index.IndexedTag(Strin g, Blog)
post	this.blog == blog
post	init'ed(this.blog)
post	this.blogEntries == &new ArrayList(IndexedTag#1 )
post	this.name != null
post	new ArrayList(IndexedTag#1) num objects == 1
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.String:replaceAll

method	List getBlogEntries()
pre	init'ed(this.blogEntries)
post	return_value == &new ArrayList(getBlogEntries#1 )
post	new ArrayList(getBlogEntries#1) num objects == 1

method	void addBlogEntry(String)
pre	(soft) this.blogEntries != null
test_vector	blogEntryId: Addr_Set{null}, Inverse{null}
test_vector	java.util.List:contains(...)@77: {1}, {0}

method	void removeBlogEntry(String)
pre	(soft) this.blogEntries != null
test_vector	blogEntryId: Addr_Set{null}, Inverse{null}

method	int getNumberOfBlogEntries()
pre	this.blogEntries != null
post	init'ed(return_value)

method	int getRank()
pre	init'ed(this.rank)
post	return_value == this.rank
post	init'ed(return_value)

method	void calculateRank(int[])
pre	thresholds != null
pre	(soft) this.blogEntries != null
pre	(soft) thresholds.length <= 232-1
pre	(soft) init'ed(thresholds[...])
post	possibly_updated(this.rank)
unanalyzed	call on java.util.List:size