Messages

info method not available -- call on Log org.apache.commons.logging. LogFactory:getLog(Class)

method	void clear()
pre	(soft) this.blog != null
post	this.tags == &new HashMap(clear#1)
post	new HashMap(clear#1) num objects == 1
unanalyzed	call on java.util.Map:values
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on getName
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getBlogEntries
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getIndexesDirectory
unanalyzed	call on java.io.File
unanalyzed	call on java.io.FileWriter
unanalyzed	call on java.io.BufferedWriter
unanalyzed	call on java.io.BufferedWriter:write
unanalyzed	call on java.io.BufferedWriter:newLine
unanalyzed	call on java.io.BufferedWriter:flush
unanalyzed	call on java.io.BufferedWriter:close
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on java.util.ArrayList

method	void index(Collection)
pre	blogEntries != null
pre	(soft) net.sourceforge.pebble.domain.State__static_ init.new State(State__static_init#5).name != null
pre	(soft) this.blog != null
pre	(soft) this.tags != null
presumption	blogEntry.blog@82 != null
presumption	blogEntry.state@81 != null
presumption	blogEntry.blog.rootCategory@82 != null
presumption	blogEntry.tagsAsList@82 != null
presumption	java.util.Iterator:next(...)@81 != null
presumption	java.util.Iterator:next(...)@83 != null
presumption	t.blogEntries@84 != null
post	this.orderedTags == One-of{old this.orderedTags, &new ArrayList(recalculateTagRankings#2)}
post	new ArrayList(recalculateTagRankings#2) num objects <= 1
unanalyzed	call on encode
unanalyzed	call on java.util.Map:get
unanalyzed	call on net.sourceforge.pebble.index.IndexedTag
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:values
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on getName
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getBlogEntries
unanalyzed	call on java.util.Map:size
unanalyzed	call on getNumberOfBlogEntries
unanalyzed	call on java.lang.Math:round
unanalyzed	call on java.util.ArrayList
unanalyzed	call on calculateRank
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getIndexesDirectory
unanalyzed	call on java.io.File
unanalyzed	call on java.io.FileWriter
unanalyzed	call on java.io.BufferedWriter
unanalyzed	call on java.io.BufferedWriter:write
unanalyzed	call on java.io.BufferedWriter:newLine
unanalyzed	call on java.io.BufferedWriter:flush
unanalyzed	call on java.io.BufferedWriter:close
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.String:replaceAll
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.util.Set:size
unanalyzed	call on java.util.Collections:reverse
unanalyzed	call on getRootCategory
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:addAll
test_vector	java.util.Iterator:hasNext(...)@81: {1}, {0}
test_vector	java.util.Iterator:hasNext(...)@83: {1}, {0}

method	void index(BlogEntry)
pre	blogEntry != null
pre	blogEntry.state != null
pre	(soft) blogEntry.blog != null
pre	(soft) init'ed(blogEntry.categories)
pre	(soft) init'ed(blogEntry.id)
pre	(soft) init'ed(blogEntry.state.name)
pre	(soft) blogEntry.tagsAsList != null
pre	(soft) net.sourceforge.pebble.domain.State__static_ init.new State(State__static_init#5).name != null
pre	(soft) this.blog != null
pre	(soft) this.tags != null
pre	(soft) blogEntry.blog.rootCategory != null
presumption	java.util.Iterator:next(...)@101 != null
presumption	t.blogEntries@102 != null
pre	(soft) init'ed(blogEntry.blog.rootCategory... parent)
pre	(soft) init'ed(blogEntry.blog.rootCategory... tagsAsList)
post	this.orderedTags == One-of{old this.orderedTags, &new ArrayList(recalculateTagRankings#2)}
post	new ArrayList(recalculateTagRankings#2) num objects <= 1
pre	(soft) init'ed(blogEntry.blog.rootCategory.parent)
unanalyzed	call on encode
unanalyzed	call on java.util.Map:get
pre	(soft) init'ed(blogEntry.blog.rootCategory. tagsAsList)
unanalyzed	call on net.sourceforge.pebble.index.IndexedTag
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:values
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on getName
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getBlogEntries
unanalyzed	call on java.util.Map:size
unanalyzed	call on getNumberOfBlogEntries
unanalyzed	call on java.lang.Math:round
unanalyzed	call on java.util.ArrayList
unanalyzed	call on calculateRank
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getIndexesDirectory
unanalyzed	call on java.io.File
unanalyzed	call on java.io.FileWriter
unanalyzed	call on java.io.BufferedWriter
unanalyzed	call on java.io.BufferedWriter:write
unanalyzed	call on java.io.BufferedWriter:newLine
unanalyzed	call on java.io.BufferedWriter:flush
unanalyzed	call on java.io.BufferedWriter:close
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.String:replaceAll
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.HashSet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.util.Set:size
unanalyzed	call on java.util.Collections:reverse
unanalyzed	call on getRootCategory
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:addAll
test_vector	java.util.Iterator:hasNext(...)@101: {1}, {0}

method	void unindex(BlogEntry)
pre	this.tags != null
pre	(soft) blogEntry != null
pre	(soft) init'ed(blogEntry.id)
pre	(soft) this.blog != null
presumption	java.util.Iterator:next(...)@117 != null
presumption	java.util.Map:values(...)@117 != null
presumption	t.blogEntries@118 != null
post	this.orderedTags == One-of{old this.orderedTags, &new ArrayList(recalculateTagRankings#2)}
post	new ArrayList(recalculateTagRankings#2) num objects <= 1
unanalyzed	call on encode
unanalyzed	call on java.util.Map:get
unanalyzed	call on net.sourceforge.pebble.index.IndexedTag
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.util.Map:values
unanalyzed	call on java.util.Collection:iterator
unanalyzed	call on getName
unanalyzed	call on java.util.List:iterator
unanalyzed	call on getBlogEntries
unanalyzed	call on java.util.Map:size
unanalyzed	call on getNumberOfBlogEntries
unanalyzed	call on java.lang.Math:round
unanalyzed	call on java.util.ArrayList
unanalyzed	call on calculateRank
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getIndexesDirectory
unanalyzed	call on java.io.File
unanalyzed	call on java.io.FileWriter
unanalyzed	call on java.io.BufferedWriter
unanalyzed	call on java.io.BufferedWriter:write
unanalyzed	call on java.io.BufferedWriter:newLine
unanalyzed	call on java.io.BufferedWriter:flush
unanalyzed	call on java.io.BufferedWriter:close
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.String:replaceAll
unanalyzed	call on java.util.List:remove
unanalyzed	call on java.util.List:size
test_vector	java.util.Iterator:hasNext(...)@117: {1}, {0}

method	void readIndex()
pre	this.blog != null
pre	(soft) this.tags != null
presumption	blogEntries.length@140 <= 2³²-1
presumption	org.apache.commons.logging.LogFactory:getLog(... )@50 != null
presumption	tag.blogEntries@137 != null
presumption	tuple.length@136 >= 1
unanalyzed	call on encode
unanalyzed	call on java.util.Map:get
unanalyzed	call on net.sourceforge.pebble.index.IndexedTag
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.String:replaceAll
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Collections:sort
test_vector	java.io.File:exists(...)@131: {0}, {1}
test_vector	tuple.length@136: {1}, {2..+Inf}
test_vector	tuple[1]@136: Addr_Set{null}, Inverse{null}

info method not available -- call on String net.sourceforge.pebble.domain. Blog:getIndexesDirectory()

info method not available -- call on void org.apache.commons.logging. Log:error(Object, Throwable)

method	void writeIndex()
pre	(soft) this.blog != null
pre	(soft) this.tags != null
presumption	java.util.Iterator:next(...)@164 != null
presumption	java.util.Map:values(...)@164 != null
presumption	org.apache.commons.logging.LogFactory:getLog(... )@50 != null
unanalyzed	call on java.util.ArrayList
test_vector	java.util.Iterator:hasNext(...)@164: {1}, {0}
test_vector	java.util.Iterator:hasNext(...)@167: {1}, {0}

info method not available -- call on String net.sourceforge.pebble.domain. Blog:getIndexesDirectory()

info method not available -- call on void org.apache.commons.logging. Log:error(Object, Throwable)

method	IndexedTag getTag(String)
pre	this.tags != null
pre	(soft) init'ed(this.blog)
post	return_value != null
post	new ArrayList(IndexedTag#1) num objects <= 1
post	new IndexedTag(getTag#1) num objects <= 1
post	new IndexedTag(getTag#1).blog == this.blog
post	(soft) init'ed(new IndexedTag(getTag#1).blog)
post	new IndexedTag(getTag#1).blogEntries == &new ArrayList(IndexedTag#1)
post	new IndexedTag(getTag#1).name != null
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.String:replaceAll
unanalyzed	call on java.util.ArrayList
test_vector	java.util.Map:get(...)@189: Inverse{null}, Addr_Set{null}

method	void recalculateTagRankings()
pre	this.tags != null
presumption	java.lang.Math:round(...)@209 in -2³¹.. 2³²-1
presumption	java.util.Iterator:next(...)@201 != null
presumption	java.util.Iterator:next(...)@215 != null
presumption	java.util.Map:values(...)@201 != null
presumption	java.util.Map:values(...)@215 != null
presumption	tag.blogEntries@201 != null
presumption	tag.blogEntries@202 != null
presumption	tag.blogEntries@215 != null
presumption	tag.blogEntries@216 != null
post	this.orderedTags == One-of{old this.orderedTags, &new ArrayList(recalculateTagRankings#2)}
post	new ArrayList(recalculateTagRankings#2) num objects <= 1
unanalyzed	call on java.util.List:size
test_vector	java.util.Iterator:hasNext(...)@201: {1}, {0}
test_vector	java.util.Iterator:hasNext(...)@215: {1}, {0}
test_vector	java.util.List:size(...)@100: {-2³¹..0}, {1..2³²-1}
test_vector	java.util.Map:size(...)@198: {-2³¹..0}, {1..2³²-1}

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

method	List getRecentBlogEntries(Tag)
pre	tag != null
pre	init'ed(tag.name)
pre	this.tags != null
pre	(soft) init'ed(this.blog)
post	return_value == &new ArrayList(getRecentBlogEnt ries#1)
post	new ArrayList(getRecentBlogEntries#1) num objects == 1
unanalyzed	call on encode
unanalyzed	call on java.util.Map:get
unanalyzed	call on net.sourceforge.pebble.index.IndexedTag
unanalyzed	call on java.util.Map:put
unanalyzed	call on java.lang.String:trim
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.String:replaceAll
unanalyzed	call on java.util.ArrayList