Messages

method	net.sourceforge.pebble.index.AuthorIndex__static_ init
post	init'ed(log)

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

method	void net.sourceforge.pebble.index.AuthorIndex(Blog )
pre	blog != null
post	this.authors == &new HashMap(AuthorIndex#1)
post	this.blog == blog
post	this.blog != null
post	new HashMap(AuthorIndex#1) num objects == 1
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.Map:put
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getIndexesDirectory
unanalyzed	call on java.io.File
unanalyzed	call on java.io.File:exists
unanalyzed	call on java.io.FileReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on java.io.BufferedReader:readLine
unanalyzed	call on java.lang.String:split
unanalyzed	call on java.util.List:add
unanalyzed	call on java.io.BufferedReader:close
unanalyzed	call on org.apache.commons.logging.Log:error

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

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.authors != null
pre	(soft) this.blog != null
presumption	blogEntry.state@77 != null
presumption	java.util.Iterator:next(...)@77 != null
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.Map:put
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getIndexesDirectory
unanalyzed	call on java.io.File
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on java.io.FileWriter
unanalyzed	call on java.io.BufferedWriter
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.io.BufferedWriter:write
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.io.BufferedWriter:newLine
unanalyzed	call on java.io.BufferedWriter:flush
unanalyzed	call on java.io.BufferedWriter:close
unanalyzed	call on java.lang.String:equals
test_vector	java.util.Iterator:hasNext(...)@77: {1}, {0}

method	void index(BlogEntry)
pre	blogEntry != null
pre	blogEntry.state != null
pre	(soft) init'ed(blogEntry.author)
pre	(soft) init'ed(blogEntry.id)
pre	(soft) init'ed(blogEntry.state.name)
pre	(soft) net.sourceforge.pebble.domain.State__static_ init.new State(State__static_init#5).name != null
pre	(soft) this.authors != null
pre	(soft) this.blog != null
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.Map:put
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getIndexesDirectory
unanalyzed	call on java.io.File
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on java.io.FileWriter
unanalyzed	call on java.io.BufferedWriter
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.io.BufferedWriter:write
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.io.BufferedWriter:newLine
unanalyzed	call on java.io.BufferedWriter:flush
unanalyzed	call on java.io.BufferedWriter:close
unanalyzed	call on java.lang.String:equals

method	void unindex(BlogEntry)
pre	blogEntry != null
pre	init'ed(blogEntry.author)
pre	this.authors != null
pre	(soft) init'ed(blogEntry.id)
pre	(soft) this.blog != null
unanalyzed	call on java.util.Map:get
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getIndexesDirectory
unanalyzed	call on java.io.File
unanalyzed	call on org.apache.commons.logging.Log:error
unanalyzed	call on java.io.FileWriter
unanalyzed	call on java.io.BufferedWriter
unanalyzed	call on java.util.Map:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.io.BufferedWriter:write
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.io.BufferedWriter:newLine
unanalyzed	call on java.io.BufferedWriter:flush
unanalyzed	call on java.io.BufferedWriter:close
test_vector	java.util.List:isEmpty(...)@113: {0}, {1}
test_vector	java.util.Map:get(...)@109: Addr_Set{null}, Inverse{null}

method	void readIndex()
pre	this.blog != null
pre	(soft) this.authors != null
presumption	blogEntryIds.length@136 <= 2³²-1
presumption	org.apache.commons.logging.LogFactory:getLog(... )@50 != null
presumption	tuple.length@131 >= 1
unanalyzed	call on java.util.Map:get
unanalyzed	call on java.util.LinkedList
unanalyzed	call on java.util.Map:put
test_vector	java.io.File:exists(...)@126: {0}, {1}
test_vector	tuple.length@131: {1}, {2..+Inf}
test_vector	tuple[1]@131: 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.authors != null
pre	(soft) this.blog != null
presumption	java.util.Map:keySet(...)@160 != null
presumption	org.apache.commons.logging.LogFactory:getLog(... )@50 != null
test_vector	java.util.Iterator:hasNext(...)@160: {1}, {0}
test_vector	java.util.Iterator:hasNext(...)@165: {1}, {0}
test_vector	java.util.Map:get(...)@163: 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	List getBlogEntries(String)
pre	this.authors != null
post	return_value != null
post	new LinkedList(getBlogEntries#1) num objects <= 1
test_vector	java.util.Map:get(...)@181: Inverse{null}, Addr_Set{null}

method	List getAuthors()
pre	this.authors != null
post	return_value == &new LinkedList(getAuthors#1)
post	new LinkedList(getAuthors#1) num objects == 1

method	List getRecentBlogEntries(String)
pre	this.authors != null
post	return_value in Addr_Set{&new LinkedList(getRec entBlogEntries#2),&new LinkedList(getRecentBlog Entries#1)}
post	new LinkedList(getRecentBlogEntries#1) num objects <= 1
post	new LinkedList(getRecentBlogEntries#2) num objects <= 1
test_vector	java.util.Map:get(...)@204: Inverse{null}, Addr_Set{null}