Messages

Last Msg First Msg

method

net.sourceforge.pebble.domain.Year__static_init

method	void net.sourceforge.pebble.domain.Year(Blog, int)
pre	blog != null
post	this.blog != null
post	init'ed(this.date)
post	this.months == &new Month[](init#1)
post	this.year == year
post	init'ed(this.year)
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)
post	new Day[](Month#1) num objects == 12
post	init'ed(new Day[](Month#1).length)
post	init'ed(new Day[](Month#1)[...])
post	new Month(init#2) num objects == 12
post	new Month(init#2).blog != null
post	new Month(init#2).dailyBlogs != null
post	init'ed(new Month(init#2).date)
post	init'ed(new Month(init#2).lastDayInMonth)
post	new Month(init#2).month == 13
post	new Month(init#2).year != null
post	new Month[](init#1) num objects == 1
post	this.months.length == 12
post	init'ed(this.months[...])
unanalyzed	call on getMonth
unanalyzed	call on getBlog
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on java.util.Calendar:set
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on setDate
unanalyzed	call on net.sourceforge.pebble.domain.Month
unanalyzed	call on net.sourceforge.pebble.domain.TimePeriod
unanalyzed	call on java.util.Calendar:setTime
unanalyzed	call on java.util.Calendar:getActualMaximum
unanalyzed	call on getYear
unanalyzed	call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed	call on java.util.ArrayList

method	void init()
pre	this.blog != null
pre	init'ed(this.year)
post	init'ed(this.date)
post	this.months == &new Month[](init#1)
post	init'ed(this.months[...])
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)
post	new Day[](Month#1) num objects == 12
post	init'ed(new Day[](Month#1).length)
post	init'ed(new Day[](Month#1)[...])
post	new Month(init#2) num objects == 12
post	new Month(init#2).blog != null
post	new Month(init#2).dailyBlogs != null
post	init'ed(new Month(init#2).date)
post	init'ed(new Month(init#2).lastDayInMonth)
post	new Month(init#2).month == 13
post	new Month(init#2).year != null
post	new Month[](init#1) num objects == 1
post	this.months.length == 12
post	init'ed(this.months[...])
unanalyzed	call on getBlog
unanalyzed	call on getMonth
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on java.util.Calendar:set
unanalyzed	call on setDate
unanalyzed	call on net.sourceforge.pebble.domain.TimePeriod
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on java.util.Calendar:setTime
unanalyzed	call on java.util.Calendar:getActualMaximum
unanalyzed	call on getYear
unanalyzed	call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed	call on java.util.ArrayList

method	Calendar getCalendar()
pre	this.blog != null
pre	init'ed(this.year)
presumption	net.sourceforge.pebble.domain.Blog:getCalendar(... )@78 != null
post	(soft) return_value != null

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

method	int getYear()
pre	init'ed(this.year)
post	return_value == this.year
post	init'ed(return_value)

method	Month getBlogForMonth(int)
pre	month in 1..12
pre	this.months != null
pre	this.months.length >= 1
pre	month <= this.months.length
pre	(soft) init'ed(this.months[...])
post	return_value == this.months[...]
post	init'ed(return_value)

method	Month getBlogForPreviousMonth(Month)
pre	month != null
pre	month.month <= 13
pre	(soft) month.month <= this.months.length + 1
pre	(soft) this.blog != null
pre	(soft) this.months != null
pre	(soft) init'ed(this.months[...])
post	init'ed(return_value)
unanalyzed	call on java.lang.IllegalArgumentException
test_vector	month.month: {-2³¹..1}, {2..13}
pre	(soft) this.blog.years != null
pre	(soft) this.year >= -2³¹+1
presumption	getBlogForPreviousYear(...).months.length@127 >= 12
presumption	getBlogForPreviousYear(...).months@127 != null
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)
post	new Day[](Month#1) num objects in {0, 12}
post	init'ed(new Day[](Month#1).length)
post	init'ed(new Day[](Month#1)[...])
post	new Month(init#2) num objects in {0, 12}
post	new Month(init#2).blog != null
post	new Month(init#2).dailyBlogs != null
post	init'ed(new Month(init#2).date)
post	init'ed(new Month(init#2).lastDayInMonth)
post	new Month(init#2).month == 13
post	new Month(init#2).year != null
unanalyzed	call on getMonth
unanalyzed	call on getBlog
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on java.util.Calendar:set
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on setDate
unanalyzed	call on net.sourceforge.pebble.domain.Month
unanalyzed	call on net.sourceforge.pebble.domain.TimePeriod
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
unanalyzed	call on getYear
unanalyzed	call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed	call on java.util.ArrayList

method	Month getBlogForNextMonth(Month)
pre	month != null
pre	month.month >= 0
pre	(soft) month.month - this.months.length in {-Inf..-1, 12..2³²-1}
pre	(soft) this.blog != null
pre	(soft) this.months != null
pre	(soft) init'ed(this.months[...])
post	init'ed(return_value)
unanalyzed	call on java.lang.IllegalArgumentException
test_vector	month.month: {12..2³²-1}, {0..11}
pre	(soft) this.blog.years != null
pre	(soft) this.year <= 2³²-2
presumption	getBlogForNextYear(...).months.length@142 >= 1
presumption	getBlogForNextYear(...).months@142 != null
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)
post	new Day[](Month#1) num objects in {0, 12}
post	init'ed(new Day[](Month#1).length)
post	init'ed(new Day[](Month#1)[...])
post	new Month(init#2) num objects in {0, 12}
post	new Month(init#2).blog != null
post	new Month(init#2).dailyBlogs != null
post	init'ed(new Month(init#2).date)
post	init'ed(new Month(init#2).lastDayInMonth)
post	new Month(init#2).month == 13
post	new Month(init#2).year != null
unanalyzed	call on getMonth
unanalyzed	call on getBlog
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on java.util.Calendar:set
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on setDate
unanalyzed	call on net.sourceforge.pebble.domain.Month
unanalyzed	call on net.sourceforge.pebble.domain.TimePeriod
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
unanalyzed	call on getYear
unanalyzed	call on net.sourceforge.pebble.domain. Month:getBlog
unanalyzed	call on java.util.ArrayList

method	Month getBlogForFirstMonth()
pre	this.months != null
pre	this.months.length >= 1
pre	(soft) init'ed(this.months[...])
post	return_value == this.months[...]
post	init'ed(return_value)
unanalyzed	call on java.lang.IllegalArgumentException

method	Month[] getMonths()
pre	(soft) this.months != null
pre	(soft) this.months.length >= 1
pre	(soft) init'ed(this.months[...])
post	return_value == &new Month[](getMonths#1)
post	new Month[](getMonths#1) num objects == 1
post	return_value.length == 12
post	return_value[...] == null
unanalyzed	call on java.lang.IllegalArgumentException

Prev Msg Next Msg

click for all messages in this file low

precondition failure net/sourceforge/pebble/domain/Year.getBlogForMonth: month <= this.months.length

Prev Msg Next Msg

method	List getArchives()
pre	this.blog != null
pre	(soft) this.months != null
pre	(soft) this.months.length >= 1
pre	(soft) this.months[...] != null
pre	(soft) this.months[...].date != null
post	return_value == &new LinkedList(getArchives#1)
post	new LinkedList(getArchives#1) num objects == 1
unanalyzed	call on java.lang.IllegalArgumentException
unanalyzed	call on java.util.Date:after
unanalyzed	call on java.util.Date:before
test_vector	java.util.Date:after(...)@267: {1}, {0}
test_vector	java.util.Date:before(...)@256: {1}, {0}
pre	init'ed(this.blog.blogEntryIndex)
pre	this.blog.properties != null
pre	this.blog.years != null
pre	(soft) init'ed(this.blog.blogEntryIndex. indexEntries)
unanalyzed	call on getMonth
unanalyzed	call on getBlog
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on java.util.Calendar:set
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on setDate
unanalyzed	call on net.sourceforge.pebble.domain.Month
unanalyzed	call on net.sourceforge.pebble.domain.TimePeriod
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.Properties:getProperty
unanalyzed	call on getTimeZone
unanalyzed	call on getLocale
unanalyzed	call on java.util.Calendar:getInstance
unanalyzed	call on java.util.Locale
unanalyzed	call on java.util.TimeZone:getTimeZone
unanalyzed	call on java.util.Calendar:get
unanalyzed	call on getBlogForMonth
unanalyzed	call on java.util.List:size
unanalyzed	call on java.util.List:get
unanalyzed	call on java.util.Date
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:isEmpty
unanalyzed	call on java.lang.Long:parseLong
unanalyzed	call on getBlogForDay
unanalyzed	call on java.util.Calendar:setTime
unanalyzed	call on java.util.Calendar:getActualMaximum
unanalyzed	call on getYear
unanalyzed	call on net.sourceforge.pebble.domain. Month:getBlog

Prev Msg Next Msg

click for all messages in this file low

precondition failure net/sourceforge/pebble/domain/Year.getBlogForMonth: month <= this.months.length

Prev Msg Next Msg

Prev Msg Next Msg

+

click for all messages in this file medium

precondition failure net/sourceforge/pebble/domain/Month.after: month != null

+

medium

precondition failure net/sourceforge/pebble/domain/Month.before: month != null

Prev Msg Next Msg

method	int compareTo(Object)
pre	o != null
pre	init'ed(o.year)
pre	o.year - this.year in -2³²+1.. 2³¹
pre	init'ed(this.year)
post	return_value == -(o.year - this.year)
post	init'ed(return_value)

method	String toString()
pre	init'ed(this.year)
post	return_value != null