Messages

Last Msg First Msg

method

void net.sourceforge.pebble.permalink. Latin1SeoPermalinkProvider()

method	Blog getBlog()
pre	init'ed(this.blog)
post	return_value == this.blog
post	init'ed(return_value)

method	void setBlog(Blog)
post	this.blog == blog
post	init'ed(this.blog)

method	String getPermalink(BlogEntry)
presumption	net.sourceforge.pebble.domain.Blog:getBlogEntries(. ..)@66 != null
presumption	net.sourceforge.pebble.domain.BlogEntry:getTitle(.. .)@62 != null
presumption	net.sourceforge.pebble.domain.BlogEntry:getTitle(.. .)@71 != null
presumption	net.sourceforge.pebble.domain.BlogService:getBlogEn try(...)@70 != null
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:getTitle
pre	blogEntry != null
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:getId
pre	(soft) this.blog != null
presumption	java.util.List:get(...)@70 != null
presumption	java.util.List:indexOf(...)@68 - java.util. List:size(...)@68 in -2³²..6_442_450_942
presumption	java.util.List:size(...)@68 >= -2³¹+1
post	return_value != null
test_vector	net.sourceforge.pebble.domain.BlogEntry:getTitle(.. .)@62: Addr_Set{null}, Inverse{null}
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:toLowerCase
unanalyzed	call on java.lang.String:replaceAll
unanalyzed	call on java.util.HashMap:keySet
unanalyzed	call on java.util.Set:iterator
unanalyzed	call on java.util.HashMap:get
test_vector	java.lang.String:equals(...)@71: {0}, {1}
test_vector	java.lang.String:length(...)@62: {1.. 2³²-1}, {0}

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

info method not available -- call on void net.sourceforge.pebble.domain. BlogService()

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

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

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

info method not available -- call on BlogEntry net.sourceforge.pebble.domain. BlogService:getBlogEntry(Blog, String)

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

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

method	String buildPermalink(BlogEntry)
test_vector	net.sourceforge.pebble.domain.BlogEntry:getTitle(.. .)@88: Addr_Set{null}, Inverse{null}
pre	blogEntry != null
post	return_value != null
test_vector	java.lang.String:length(...)@104: {1.. 2³²-1}, {0}
test_vector	java.lang.String:length(...)@89: {1.. 2³²-1}, {0}
test_vector	java.util.Iterator:hasNext(...)@94: {1}, {0}

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

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

Prev Msg Next Msg

click for all messages in this file warning

test always goes same way test predetermined because title != null

Prev Msg Next Msg

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

method	bool isBlogEntryPermalink(String)
post	init'ed(return_value)
test_vector	uri: Addr_Set{null}, Inverse{null}

method	BlogEntry getBlogEntry(String)
presumption	net.sourceforge.pebble.domain.Blog:getBlogEntries(. ..)@122 != null
presumption	net.sourceforge.pebble.domain.BlogEntry:getLocalPer malink(...)@128 != null
presumption	net.sourceforge.pebble.domain.BlogService:getBlogEn try(...)@125 != null
pre	this.blog != null
presumption	java.util.Iterator:next(...)@125 != null
post	init'ed(return_value)
test_vector	java.lang.String:endsWith(...)@128: {0}, {1}
test_vector	java.util.Iterator:hasNext(...)@123: {1}, {0}

info method not available -- call on void net.sourceforge.pebble.domain. BlogService()

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

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

method	String getPermalink(Month)
pre	month != null
pre	this.blog != null
post	init'ed(return_value)

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

info method not available -- call on Date net.sourceforge.pebble.domain. Month:getDate()

method	bool isMonthPermalink(String)
post	init'ed(return_value)
test_vector	uri: Addr_Set{null}, Inverse{null}

method	Month getMonth(String)
post	init'ed(return_value)
pre	this.blog != null
pre	uri != null

info method not available -- call on Month net.sourceforge.pebble.domain. Blog:getBlogForMonth(int, int)

method	String getPermalink(Day)
pre	day != null
pre	this.blog != null
post	init'ed(return_value)

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

info method not available -- call on Date net.sourceforge.pebble.domain. Day:getDate()

method	bool isDayPermalink(String)
post	init'ed(return_value)
test_vector	uri: Addr_Set{null}, Inverse{null}

method	Day getDay(String)
post	init'ed(return_value)
pre	this.blog != null
pre	uri != null

info method not available -- call on Day net.sourceforge.pebble.domain. Blog:getBlogForDay(int, int, int)

method	net.sourceforge.pebble.permalink.Latin1SeoPermalin kProvider__static_init
post	characterSubstitutions == &new HashMap(Latin1Se oPermalinkProvider__static_init#1)
post	new HashMap(Latin1SeoPermalinkProvider__static_ init#1) num objects == 1

	info	method not available	-- call on String net.sourceforge.pebble.domain. BlogEntry:getId()
	info	method not available	-- call on BlogEntry net.sourceforge.pebble.domain. BlogService:getBlogEntry(Blog, String)