Messages

method | net.sourceforge.pebble.util.Pageable__static_init

method | void net.sourceforge.pebble.util.Pageable(List)
pre | (soft) list != null
post | this.list == list
post | (soft) this.list != null
post | init'ed(this.maxPages)
post | this.page == 1
post | this.pageSize == 10
unanalyzed | call on java.util.List:size

method | void calculatePages()
pre | init'ed(this.pageSize)
pre | (soft) this.list != null
presumption | java.util.List:size(...)@85/this.pageSize in -232+1..232-2
post | possibly_updated(this.maxPages)
test_vector | this.pageSize: {-231..0}, {1..232-1}

method | List getList()
pre | init'ed(this.list)
post | return_value == this.list
post | init'ed(return_value)

method | List getListForPage()
pre | init'ed(this.endingIndex)
pre | this.list != null
pre | init'ed(this.startingIndex)
post | init'ed(return_value)

method | int getPageSize()
pre | init'ed(this.pageSize)
post | return_value == this.pageSize
post | init'ed(return_value)

method | void setPageSize(int)
pre | (soft) this.list != null
post | possibly_updated(this.maxPages)
post | this.pageSize == pageSize
post | init'ed(this.pageSize)
unanalyzed | call on java.util.List:size

method | int getPage()
pre | init'ed(this.page)
post | return_value == this.page
post | init'ed(return_value)

method | void setPage(int)
pre | this.list != null
pre | init'ed(this.maxPages)
pre | init'ed(this.pageSize)
post | init'ed(this.endingIndex)
post | this.page == One-of{this.maxPages, 1, p}
post | init'ed(this.page)
post | this.startingIndex == One-of{this.pageSize*(this. page - 1), 0}
post | this.startingIndex >= 0
post | this.pageSize + this.startingIndex in -231..232-1
post | this.pageSize*(this.page - 1) in -231.. 232-1
test_vector | p: {2..232-2}, {-231..1}
test_vector | this.maxPages - p: {1..232-3}, {-6_442_450_943..0}

method | int getMaxPages()
pre | init'ed(this.maxPages)
post | return_value == this.maxPages
post | init'ed(return_value)

method | int getPreviousPage()
pre | init'ed(this.page)
post | return_value == One-of{this.page - 1, 0}
post | return_value in 0..232-2
test_vector | this.page: {-231..1}, {2..232-1}

method | int getNextPage()
pre | init'ed(this.maxPages)
pre | init'ed(this.page)
post | return_value == One-of{this.page + 1, 0}
post | return_value >= -231+1
test_vector | this.maxPages - this.page: {-6_442_450_943..0}, {1..6_442_450_943}

method | int getMinPageRange()
pre | init'ed(this.page)
post | return_value == One-of{this.page - 10, 1}
post | return_value in 1..232-11
test_vector | this.page: {-231..10}, {11.. 232-1}

method | int getMaxPageRange()
pre | init'ed(this.maxPages)
pre | init'ed(this.page)
post | return_value == One-of{this.page + 10, this.maxPages}
post | init'ed(return_value)
test_vector | this.maxPages - this.page: {-6_442_450_943..10}, {11..6_442_450_943}