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: {-231..1}, {2..13}
pre | (soft) this.blog.years != null
pre | (soft) this.year >= -231+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..232-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..232-1}, {0..11}
pre | (soft) this.blog.years != null
pre | (soft) this.year <= 232-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

| 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

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

Prev Msg Next Msg

Prev Msg Next Msg

+ |
| 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 -232+1.. 231
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