//# 2 errors, 193 messages
//#
/*
    //#pageable.java:1:1: class: net.sourceforge.pebble.util.Pageable
    //#pageable.java:1:1: method: net.sourceforge.pebble.util.Pageable.net.sourceforge.pebble.util.Pageable__static_init
 * Copyright (c) 2003-2006, Simon Brown
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   - Redistributions of source code must retain the above copyright
 *     notice, this list of conditions and the following disclaimer.
 *
 *   - Redistributions in binary form must reproduce the above copyright
 *     notice, this list of conditions and the following disclaimer in
 *     the documentation and/or other materials provided with the
 *     distribution.
 *
 *   - Neither the name of Pebble nor the names of its contributors may
 *     be used to endorse or promote products derived from this software
 *     without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 */
package net.sourceforge.pebble.util;

import java.util.List;

/**
 * Helper class that implements paging over a collection.
 *
 * @author    Simon Brown
 */
public class Pageable<T> {

  /** the default page size */
  public static final int DEFAULT_PAGE_SIZE = 10;

  private static final int PAGE_WINDOW = 10;

  /** the list over which this class is paging */
  private List<T> list;

  /** the page size */
  private int pageSize = DEFAULT_PAGE_SIZE;

  /** the current page */
  private int page;

  /** the starting index */
  private int startingIndex;

  /** the ending index */
  private int endingIndex;

  /** the maximum number of pages */
  private int maxPages;

  /**
   * Creates a new instance with the specified list.
   *
   * @param list    a List
   */
  public Pageable(List<T> list) {
    //#pageable.java:71: method: void net.sourceforge.pebble.util.Pageable.net.sourceforge.pebble.util.Pageable(List)
    //#input(void net.sourceforge.pebble.util.Pageable(List)): list
    //#input(void net.sourceforge.pebble.util.Pageable(List)): this
    //#output(void net.sourceforge.pebble.util.Pageable(List)): this.list
    //#output(void net.sourceforge.pebble.util.Pageable(List)): this.maxPages
    //#output(void net.sourceforge.pebble.util.Pageable(List)): this.page
    //#output(void net.sourceforge.pebble.util.Pageable(List)): this.pageSize
    //#pre[1] (void net.sourceforge.pebble.util.Pageable(List)): (soft) list != null
    //#post(void net.sourceforge.pebble.util.Pageable(List)): this.list == list
    //#post(void net.sourceforge.pebble.util.Pageable(List)): (soft) this.list != null
    //#post(void net.sourceforge.pebble.util.Pageable(List)): init'ed(this.maxPages)
    //#post(void net.sourceforge.pebble.util.Pageable(List)): this.page == 1
    //#post(void net.sourceforge.pebble.util.Pageable(List)): this.pageSize == 10
    //#unanalyzed(void net.sourceforge.pebble.util.Pageable(List)): Effects-of-calling:java.util.List:size
    this.list = list;
    this.page = 1;
    this.maxPages = 1;

    calculatePages();
  }
    //#pageable.java:77: end of method: void net.sourceforge.pebble.util.Pageable.net.sourceforge.pebble.util.Pageable(List)

  private void calculatePages() {
    if (pageSize > 0) {
    //#pageable.java:80: method: void net.sourceforge.pebble.util.Pageable.calculatePages()
    //#input(void calculatePages()): this
    //#input(void calculatePages()): this.list
    //#input(void calculatePages()): this.pageSize
    //#output(void calculatePages()): this.maxPages
    //#pre[4] (void calculatePages()): init'ed(this.pageSize)
    //#pre[3] (void calculatePages()): (soft) this.list != null
    //#presumption(void calculatePages()): java.util.List:size(...)@85/this.pageSize in -4_294_967_295..4_294_967_294
    //#post(void calculatePages()): possibly_updated(this.maxPages)
    //#test_vector(void calculatePages()): this.pageSize: {-2_147_483_648..0}, {1..4_294_967_295}
      // calculate how many pages there are
      if (list.size() % pageSize == 0) {
        maxPages = list.size() / pageSize;
      } else {
        maxPages = (list.size() / pageSize) + 1;
      }
    }
  }
    //#pageable.java:88: end of method: void net.sourceforge.pebble.util.Pageable.calculatePages()

  /**
   * Gets the list that this instance is paging over.
   *
   * @return  a List
   */
  public List<T> getList() {
    return this.list;
    //#pageable.java:96: method: List net.sourceforge.pebble.util.Pageable.getList()
    //#input(List getList()): this
    //#input(List getList()): this.list
    //#output(List getList()): return_value
    //#pre[2] (List getList()): init'ed(this.list)
    //#post(List getList()): return_value == this.list
    //#post(List getList()): init'ed(return_value)
    //#pageable.java:96: end of method: List net.sourceforge.pebble.util.Pageable.getList()
  }

  /**
   * Gets the subset of the list for the current page.
   *
   * @return  a List
   */
  public List<T> getListForPage() {
    return list.subList(startingIndex, endingIndex);
    //#pageable.java:105: method: List net.sourceforge.pebble.util.Pageable.getListForPage()
    //#input(List getListForPage()): this
    //#input(List getListForPage()): this.endingIndex
    //#input(List getListForPage()): this.list
    //#input(List getListForPage()): this.startingIndex
    //#output(List getListForPage()): return_value
    //#pre[2] (List getListForPage()): init'ed(this.endingIndex)
    //#pre[3] (List getListForPage()): this.list != null
    //#pre[4] (List getListForPage()): init'ed(this.startingIndex)
    //#post(List getListForPage()): init'ed(return_value)
    //#pageable.java:105: end of method: List net.sourceforge.pebble.util.Pageable.getListForPage()
  }

  /**
   * Gets the page size.
   *
   * @return  the page size as an int
   */
  public int getPageSize() {
    return this.pageSize;
    //#pageable.java:114: method: int net.sourceforge.pebble.util.Pageable.getPageSize()
    //#input(int getPageSize()): this
    //#input(int getPageSize()): this.pageSize
    //#output(int getPageSize()): return_value
    //#pre[2] (int getPageSize()): init'ed(this.pageSize)
    //#post(int getPageSize()): return_value == this.pageSize
    //#post(int getPageSize()): init'ed(return_value)
    //#pageable.java:114: end of method: int net.sourceforge.pebble.util.Pageable.getPageSize()
  }

  /**
   * Sets the page size.
   *
   * @param pageSize   the page size as an int
   */
  public void setPageSize(int pageSize) {
    this.pageSize = pageSize;
    //#pageable.java:123: method: void net.sourceforge.pebble.util.Pageable.setPageSize(int)
    //#input(void setPageSize(int)): pageSize
    //#input(void setPageSize(int)): this
    //#input(void setPageSize(int)): this.list
    //#output(void setPageSize(int)): this.maxPages
    //#output(void setPageSize(int)): this.pageSize
    //#pre[4] (void setPageSize(int)): (soft) this.list != null
    //#post(void setPageSize(int)): possibly_updated(this.maxPages)
    //#post(void setPageSize(int)): this.pageSize == pageSize
    //#post(void setPageSize(int)): init'ed(this.pageSize)
    //#unanalyzed(void setPageSize(int)): Effects-of-calling:java.util.List:size
    calculatePages();
  }
    //#pageable.java:125: end of method: void net.sourceforge.pebble.util.Pageable.setPageSize(int)

  /**
   * Gets the page.
   *
   * @return  the page as an int
   */
  public int getPage() {
    return this.page;
    //#pageable.java:133: method: int net.sourceforge.pebble.util.Pageable.getPage()
    //#input(int getPage()): this
    //#input(int getPage()): this.page
    //#output(int getPage()): return_value
    //#pre[2] (int getPage()): init'ed(this.page)
    //#post(int getPage()): return_value == this.page
    //#post(int getPage()): init'ed(return_value)
    //#pageable.java:133: end of method: int net.sourceforge.pebble.util.Pageable.getPage()
  }

  /**
   * Sets the page size.
   *
   * @param p    the page as an int
   */
  public void setPage(int p) {
    if (p >= maxPages) {
    //#pageable.java:142: method: void net.sourceforge.pebble.util.Pageable.setPage(int)
    //#input(void setPage(int)): p
    //#input(void setPage(int)): this
    //#input(void setPage(int)): this.list
    //#input(void setPage(int)): this.maxPages
    //#input(void setPage(int)): this.pageSize
    //#output(void setPage(int)): this.endingIndex
    //#output(void setPage(int)): this.page
    //#output(void setPage(int)): this.startingIndex
    //#pre[5] (void setPage(int)): this.list != null
    //#pre[6] (void setPage(int)): init'ed(this.maxPages)
    //#pre[8] (void setPage(int)): init'ed(this.pageSize)
    //#post(void setPage(int)): init'ed(this.endingIndex)
    //#post(void setPage(int)): this.page == One-of{this.maxPages, 1, p}
    //#post(void setPage(int)): init'ed(this.page)
    //#post(void setPage(int)): this.startingIndex == One-of{this.pageSize*(this.page - 1), 0}
    //#post(void setPage(int)): this.startingIndex >= 0
    //#post(void setPage(int)): this.pageSize + this.startingIndex in -2_147_483_648..4_294_967_295
    //#post(void setPage(int)): this.pageSize*(this.page - 1) in -2_147_483_648..4_294_967_295
    //#test_vector(void setPage(int)): p: {2..4_294_967_294}, {-2_147_483_648..1}
    //#test_vector(void setPage(int)): this.maxPages - p: {1..4_294_967_293}, {-6_442_450_943..0}
      this.page = maxPages;
    } else if (p <= 1) {
      this.page = 1;
    } else {
      this.page = p;
    }

    // now work out where the sub-list should start and end
    startingIndex = pageSize * (page-1);
    //#pageable.java:151: ?overflow
    //#    this.pageSize*(this.page - 1) in -2_147_483_648..4_294_967_295
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.util.Pageable
    //#    method: void setPage(int)
    //#    basic block: bb_6
    //#    assertion: this.pageSize*(this.page - 1) in -2_147_483_648..4_294_967_295
    //#    VN: this.pageSize*(this.page - 1)
    //#    Expected: {-2_147_483_648..4_294_967_295, Invalid}
    //#    Bad: {-9_223_372_039_002_259_455..-2_147_483_649, 4_294_967_296..18_446_744_060_824_649_730}
    //#    Attribs:  Int  Bad < Exp  Bad > Exp
    if (startingIndex < 0) {
      startingIndex = 0;
    }
    endingIndex = startingIndex + pageSize;
    //#pageable.java:155: ?overflow
    //#    this.startingIndex + this.pageSize in -2_147_483_648..4_294_967_295
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.util.Pageable
    //#    method: void setPage(int)
    //#    basic block: bb_8
    //#    assertion: this.startingIndex + this.pageSize in -2_147_483_648..4_294_967_295
    //#    VN: this.pageSize + this.startingIndex
    //#    Expected: {-2_147_483_648..4_294_967_295, Invalid}
    //#    Bad: {4_294_967_296..8_589_934_590}
    //#    Attribs:  Int  Bad > Exp
    if (endingIndex > list.size()) {
      endingIndex = list.size();
    }
  }
    //#pageable.java:159: end of method: void net.sourceforge.pebble.util.Pageable.setPage(int)

  /**
   * Gets the maximum number of pages.
   *
   * @return  the maximum number of pages as an int
   */
  public int getMaxPages() {
    return this.maxPages;
    //#pageable.java:167: method: int net.sourceforge.pebble.util.Pageable.getMaxPages()
    //#input(int getMaxPages()): this
    //#input(int getMaxPages()): this.maxPages
    //#output(int getMaxPages()): return_value
    //#pre[2] (int getMaxPages()): init'ed(this.maxPages)
    //#post(int getMaxPages()): return_value == this.maxPages
    //#post(int getMaxPages()): init'ed(return_value)
    //#pageable.java:167: end of method: int net.sourceforge.pebble.util.Pageable.getMaxPages()
  }

  /**
   * Determines whether there is a previous page and gets the page number.
   *
   * @return  the previous page number, or zero
   */
  public int getPreviousPage() {
    if (page > 1) {
    //#pageable.java:176: method: int net.sourceforge.pebble.util.Pageable.getPreviousPage()
    //#input(int getPreviousPage()): this
    //#input(int getPreviousPage()): this.page
    //#output(int getPreviousPage()): return_value
    //#pre[2] (int getPreviousPage()): init'ed(this.page)
    //#post(int getPreviousPage()): return_value == One-of{this.page - 1, 0}
    //#post(int getPreviousPage()): return_value in 0..4_294_967_294
    //#test_vector(int getPreviousPage()): this.page: {-2_147_483_648..1}, {2..4_294_967_295}
      return page-1;
    } else {
      return 0;
    //#pageable.java:179: end of method: int net.sourceforge.pebble.util.Pageable.getPreviousPage()
    }
  }

  /**
   * Determines whether there is a next page and gets the page number.
   *
   * @return  the next page number, or 0
   */
  public int getNextPage() {
    if (page < maxPages) {
    //#pageable.java:189: method: int net.sourceforge.pebble.util.Pageable.getNextPage()
    //#input(int getNextPage()): this
    //#input(int getNextPage()): this.maxPages
    //#input(int getNextPage()): this.page
    //#output(int getNextPage()): return_value
    //#pre[2] (int getNextPage()): init'ed(this.maxPages)
    //#pre[4] (int getNextPage()): init'ed(this.page)
    //#post(int getNextPage()): return_value == One-of{this.page + 1, 0}
    //#post(int getNextPage()): return_value >= -2_147_483_647
    //#test_vector(int getNextPage()): this.maxPages - this.page: {-6_442_450_943..0}, {1..6_442_450_943}
      return page+1;
    } else {
      return 0;
    //#pageable.java:192: end of method: int net.sourceforge.pebble.util.Pageable.getNextPage()
    }
  }

  /**
   * Gets the minimum page in the window.
   *
   * @return  the page number
   */
  public int getMinPageRange() {
    if (getPage() > PAGE_WINDOW) {
    //#pageable.java:202: method: int net.sourceforge.pebble.util.Pageable.getMinPageRange()
    //#pageable.java:202: Warning: suspicious precondition
    //#    the precondition for this.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.util.Pageable
    //#    method: int getMinPageRange()
    //#    suspicious precondition index: [2]
    //#input(int getMinPageRange()): __Descendant_Table[net/sourceforge/pebble/util/Pageable]
    //#input(int getMinPageRange()): __Descendant_Table[net/sourceforge/pebble/web/action/ViewResponsesAction$1]
    //#input(int getMinPageRange()): __Descendant_Table[others]
    //#input(int getMinPageRange()): __Dispatch_Table.getPage()I
    //#input(int getMinPageRange()): net/sourceforge/pebble/web/action/ViewResponsesAction$1.__Dispatch_Table.getPage()I
    //#input(int getMinPageRange()): this
    //#input(int getMinPageRange()): this.__Tag
    //#input(int getMinPageRange()): this.page
    //#output(int getMinPageRange()): return_value
    //#pre[2] (int getMinPageRange()): this.__Tag in {net/sourceforge/pebble/util/Pageable, net/sourceforge/pebble/web/action/ViewResponsesAction$1}
    //#pre[3] (int getMinPageRange()): init'ed(this.page)
    //#post(int getMinPageRange()): return_value == One-of{this.page - 10, 1}
    //#post(int getMinPageRange()): return_value in 1..4_294_967_285
    //#test_vector(int getMinPageRange()): this.page: {-2_147_483_648..10}, {11..4_294_967_295}
      return getPage() - PAGE_WINDOW;
    } else {
      return 1;
    //#pageable.java:205: end of method: int net.sourceforge.pebble.util.Pageable.getMinPageRange()
    }
  }

  /**
   * Gets the maximum page in the window.
   *
   * @return  the page number
   */
  public int getMaxPageRange() {
    if (getPage() < (getMaxPages() - PAGE_WINDOW)) {
    //#pageable.java:215: method: int net.sourceforge.pebble.util.Pageable.getMaxPageRange()
    //#pageable.java:215: Warning: suspicious precondition
    //#    the precondition for this.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.util.Pageable
    //#    method: int getMaxPageRange()
    //#    suspicious precondition index: [2]
    //#input(int getMaxPageRange()): __Descendant_Table[net/sourceforge/pebble/util/Pageable]
    //#input(int getMaxPageRange()): __Descendant_Table[net/sourceforge/pebble/web/action/ViewResponsesAction$1]
    //#input(int getMaxPageRange()): __Descendant_Table[others]
    //#input(int getMaxPageRange()): __Dispatch_Table.getMaxPages()I
    //#input(int getMaxPageRange()): __Dispatch_Table.getPage()I
    //#input(int getMaxPageRange()): net/sourceforge/pebble/web/action/ViewResponsesAction$1.__Dispatch_Table.getMaxPages()I
    //#input(int getMaxPageRange()): net/sourceforge/pebble/web/action/ViewResponsesAction$1.__Dispatch_Table.getPage()I
    //#input(int getMaxPageRange()): this
    //#input(int getMaxPageRange()): this.__Tag
    //#input(int getMaxPageRange()): this.maxPages
    //#input(int getMaxPageRange()): this.page
    //#output(int getMaxPageRange()): return_value
    //#pre[2] (int getMaxPageRange()): this.__Tag in {net/sourceforge/pebble/util/Pageable, net/sourceforge/pebble/web/action/ViewResponsesAction$1}
    //#pre[3] (int getMaxPageRange()): init'ed(this.maxPages)
    //#pre[5] (int getMaxPageRange()): init'ed(this.page)
    //#post(int getMaxPageRange()): return_value == One-of{this.page + 10, this.maxPages}
    //#post(int getMaxPageRange()): init'ed(return_value)
    //#test_vector(int getMaxPageRange()): this.maxPages - this.page: {-6_442_450_943..10}, {11..6_442_450_943}
      return getPage() + PAGE_WINDOW;
    } else {
      return getMaxPages();
    //#pageable.java:218: end of method: int net.sourceforge.pebble.util.Pageable.getMaxPageRange()
    }
  }

}    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Descendant_Table[net/sourceforge/pebble/util/Pageable]
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.calculatePages()V
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getList()Ljava/util/List;
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getListForPage()Ljava/util/List;
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getMaxPageRange()I
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getMaxPages()I
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getMinPageRange()I
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getNextPage()I
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getPage()I
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getPageSize()I
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getPreviousPage()I
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.setPage(I)V
    //#output(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.setPageSize(I)V
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Descendant_Table[net/sourceforge/pebble/util/Pageable] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.calculatePages()V == &calculatePages
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getList()Ljava/util/List; == &getList
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getListForPage()Ljava/util/List; == &getListForPage
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getMaxPageRange()I == &getMaxPageRange
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getMaxPages()I == &getMaxPages
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getMinPageRange()I == &getMinPageRange
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getNextPage()I == &getNextPage
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getPage()I == &getPage
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getPageSize()I == &getPageSize
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.getPreviousPage()I == &getPreviousPage
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.setPage(I)V == &setPage
    //#post(net.sourceforge.pebble.util.Pageable__static_init): __Dispatch_Table.setPageSize(I)V == &setPageSize
    //#pageable.java:: end of method: net.sourceforge.pebble.util.Pageable.net.sourceforge.pebble.util.Pageable__static_init
    //#pageable.java:: end of class: net.sourceforge.pebble.util.Pageable
