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}