Messages

method | net.sourceforge.pebble.domain.Day__static_init

method | void net.sourceforge.pebble.domain.Day(Month, int)
pre | month != null
pre | month.month >= -231+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 >= -231+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..232-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()

| 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()

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 >= -231+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 -232+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..232-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 <= 232-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: {-231.. -1}, {0..232-3}

method | String getFirstBlogEntry()
pre | this.publishedBlogEntries != null
presumption | java.util.List:size(...)@375 >= -231+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: {-231..0}, {1..232-1}

method | Date getStartOfDay()
pre | this.blog != null
pre | init'ed(this.day)
pre | this.month != null
pre | this.month.month >= -231+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 >= -231+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)