Messages

method

net.sourceforge.pebble.domain.Day__static_init

method	void net.sourceforge.pebble.domain.Day(Month, int)
pre	month != null
pre	month.month >= -2³¹+1
pre	month.year != null
pre	init'ed(month.year.year)
presumption	net.sourceforge.pebble.domain.Month:getBlog(... )@63 != null
post	(soft) this.blog != null
post	this.blogEntries == &new ArrayList(Day#1)
post	init'ed(this.date)
post	this.day == day
post	init'ed(this.day)
post	this.month == month
post	this.month != null
post	this.publishedBlogEntries == &new ArrayList(Day#2)
post	this.unpublishedBlogEntries == &new ArrayList(Day#3)
post	new ArrayList(Day#1) num objects == 1
post	new ArrayList(Day#2) num objects == 1
post	new ArrayList(Day#3) num objects == 1
unanalyzed	call on java.util.Calendar:set
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on getBlog
unanalyzed	call on getYear
unanalyzed	call on getMonth

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

method	Calendar getCalendar()
pre	this.blog != null
pre	init'ed(this.day)
pre	this.month != null
pre	this.month.month >= -2³¹+1
pre	this.month.year != null
pre	init'ed(this.month.year.year)
presumption	net.sourceforge.pebble.domain.Blog:getCalendar(... )@127 != null
post	(soft) return_value != null

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

method	Month getMonth()
pre	init'ed(this.month)
post	return_value == this.month
post	init'ed(return_value)

method	int getDay()
pre	init'ed(this.day)
post	return_value == this.day
post	init'ed(return_value)

method	String getPermalink()
pre	this.blog != null
post	return_value != null
pre	this.blog.permalinkProvider != null
pre	(soft) net/sourceforge/pebble/domain/BlogManager. instance != null
pre	(soft) init'ed(net/sourceforge/pebble/domain/BlogMa nager.instance.multiBlog)
pre	(soft) init'ed(this.blog.id)
test_vector	java.lang.String:length(...)@164: {0}, {1..2³²-1}
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on net.sourceforge.pebble.PebbleContext:getIns tance
unanalyzed	call on net.sourceforge.pebble.PebbleContext:getCon figuration
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:substring
test_vector	getPermalink(...)@163: Addr_Set{null}, Inverse{null}

info method not available -- call on String getPermalink(Day)

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

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

method	void addPublishedBlogEntry(String)
pre	this.blogEntries != null
pre	this.publishedBlogEntries != null
pre	this.unpublishedBlogEntries != null
test_vector	java.util.List:contains(...)@185: {1}, {0}
test_vector	java.util.List:contains(...)@191: {1}, {0}

method	void addUnpublishedBlogEntry(String)
pre	this.blogEntries != null
pre	this.publishedBlogEntries != null
pre	this.unpublishedBlogEntries != null
test_vector	java.util.List:contains(...)@199: {1}, {0}
test_vector	java.util.List:contains(...)@205: {1}, {0}

method	void removeBlogEntry(BlogEntry)
pre	blogEntry != null
pre	this.blogEntries != null
pre	this.publishedBlogEntries != null
pre	this.unpublishedBlogEntries != null

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

method	bool hasBlogEntries()
pre	this.publishedBlogEntries != null
post	init'ed(return_value)

method	Day getPreviousDay()
pre	init'ed(this.day)
pre	this.month != null
pre	(soft) this.day <= this.month.dailyBlogs.length + 1
pre	(soft) this.month.dailyBlogs != null
pre	(soft) this.month.dailyBlogs.length >= 1
pre	(soft) init'ed(this.month.dailyBlogs[...])
pre	(soft) init'ed(this.month.lastDayInMonth)
pre	(soft) this.month.year != null
pre	(soft) this.month.year.blog != null
pre	(soft) this.month.year.months != null
post	init'ed(return_value)
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on getMonth
unanalyzed	call on getBlog
unanalyzed	call on getBlogForPreviousYear
pre	(soft) this.month.month <= 13
pre	(soft) this.month.month <= this.month.year.months. length + 1
pre	(soft) this.month.year.blog.years != null
pre	(soft) init'ed(this.month.year.months[...])
pre	(soft) this.month.year.year >= -2³¹+1
post	init'ed(new ArrayList(Day#1) num objects)
post	init'ed(new ArrayList(Day#2) num objects)
post	init'ed(new ArrayList(Day#3) num objects)
post	init'ed(new Day(Month#2) num objects)
post	init'ed(new Day(Month#2).blog)
post	init'ed(new Day(Month#2).blogEntries)
post	init'ed(new Day(Month#2).date)
post	init'ed(new Day(Month#2).day)
post	init'ed(new Day(Month#2).month)
post	init'ed(new Day(Month#2).publishedBlogEntries)
post	init'ed(new Day(Month#2).unpublishedBlogEntries)
unanalyzed	call on java.util.Calendar:set
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on getYear
unanalyzed	call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed	call on net.sourceforge.pebble.domain.TimePeriod
unanalyzed	call on java.util.ArrayList
unanalyzed	call on setDate
unanalyzed	call on net.sourceforge.pebble.domain.Month
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.util.Calendar:setTime
unanalyzed	call on java.util.Calendar:getActualMaximum

method	Day getNextDay()
pre	init'ed(this.day)
pre	this.day - this.month.lastDayInMonth in -2³²+1..6_442_450_943
pre	this.month != null
pre	init'ed(this.month.lastDayInMonth)
pre	(soft) this.day < this.month.dailyBlogs.length
pre	(soft) this.month.dailyBlogs != null
pre	(soft) this.month.dailyBlogs.length >= 1
pre	(soft) init'ed(this.month.dailyBlogs[...])
pre	(soft) this.month.month - this.month.year.months. length in {-Inf..-1, 12..2³²-1}
pre	(soft) this.month.year != null
pre	(soft) this.month.year.blog != null
pre	(soft) this.month.year.months != null
post	init'ed(return_value)
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on getMonth
unanalyzed	call on getBlog
unanalyzed	call on getBlogForNextYear
unanalyzed	call on getBlogForFirstDay
pre	(soft) this.month.month >= 0
pre	(soft) this.month.year.blog.years != null
pre	(soft) init'ed(this.month.year.months[...])
pre	(soft) this.month.year.year <= 2³²-2
post	init'ed(new ArrayList(Day#1) num objects)
post	init'ed(new ArrayList(Day#2) num objects)
post	init'ed(new ArrayList(Day#3) num objects)
post	init'ed(new Day(Month#2) num objects)
post	init'ed(new Day(Month#2).blog)
post	init'ed(new Day(Month#2).blogEntries)
post	init'ed(new Day(Month#2).date)
post	init'ed(new Day(Month#2).day)
post	init'ed(new Day(Month#2).month)
post	init'ed(new Day(Month#2).publishedBlogEntries)
post	init'ed(new Day(Month#2).unpublishedBlogEntries)
unanalyzed	call on java.util.Calendar:set
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on getYear
unanalyzed	call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed	call on net.sourceforge.pebble.domain.TimePeriod
unanalyzed	call on java.util.ArrayList
unanalyzed	call on setDate
unanalyzed	call on net.sourceforge.pebble.domain.Month
unanalyzed	call on java.util.List:iterator
unanalyzed	call on java.util.List:add
unanalyzed	call on java.util.Collections:sort
unanalyzed	call on java.util.Calendar:setTime
unanalyzed	call on java.util.Calendar:getActualMaximum

method	String getPreviousBlogEntry(String)
pre	this.publishedBlogEntries != null
post	init'ed(return_value)
test_vector	java.util.List:indexOf(...)@360: {-2³¹.. -1}, {0..2³²-3}

method	String getFirstBlogEntry()
pre	this.publishedBlogEntries != null
presumption	java.util.List:size(...)@375 >= -2³¹+1
post	init'ed(return_value)
test_vector	java.util.List:isEmpty(...)@374: {1}, {0}

method	String getLastBlogEntry()
pre	this.publishedBlogEntries != null
post	init'ed(return_value)
test_vector	java.util.List:isEmpty(...)@387: {1}, {0}

method	String getNextBlogEntry(String)
pre	this.publishedBlogEntries != null
post	init'ed(return_value)
test_vector	java.util.List:lastIndexOf(...)@401: {-2³¹..0}, {1..2³²-1}

method	Date getStartOfDay()
pre	this.blog != null
pre	init'ed(this.day)
pre	this.month != null
pre	this.month.month >= -2³¹+1
pre	this.month.year != null
pre	init'ed(this.month.year.year)
post	init'ed(return_value)
unanalyzed	call on java.util.Calendar:set
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on getBlog
unanalyzed	call on getYear
unanalyzed	call on getMonth

method	Date getEndOfDay()
pre	this.blog != null
pre	init'ed(this.day)
pre	this.month != null
pre	this.month.month >= -2³¹+1
pre	this.month.year != null
pre	init'ed(this.month.year.year)
post	init'ed(return_value)
unanalyzed	call on java.util.Calendar:set
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on getBlog
unanalyzed	call on getYear
unanalyzed	call on getMonth

method	bool before(Day)
pre	day != null
pre	init'ed(day.date)
pre	this.date != null
post	init'ed(return_value)