Package components.list

Interface List<T>

Type Parameters:
T - type of List entries
All Superinterfaces:
Iterable<T>, ListKernel<T>, Standard<List<T>>
All Known Implementing Classes:
List1L, List2, List3, ListSecondary
public interface List<T> extends ListKernel<T>
ListKernel enhanced with secondary methods.

  • Method Details

    • rightFront

      T rightFront()
      Reports the front of this.right.
      Returns:
      the front entry of this.right
      Aliases:
      reference returned by rightFront
      Requires:
      this.right /= <>
      Ensures:
      <rightFront> is prefix of this.right

    • replaceRightFront

      T replaceRightFront(T x)
      Replaces the entry at the front of this.right with x, and returns the old entry.
      Parameters:
      x - the new entry
      Returns:
      the old front entry of this.right
      Aliases:
      reference x
      Updates:
      this.right
      Requires:
      this.right /= <>
      Ensures:
      <replaceRightFront> is prefix of #this.right  and
this.right = <x> * #this.right[1, |#this.right|)

    • moveToFinish

      void moveToFinish()
      Moves the position in this to the end.
      Updates:
      this
      Ensures:
      this.left = #this.left * #this.right and |this.right| = 0

    • retreat

      void retreat()
      Retreats the position in this by one.
      Updates:
      this
      Requires:
      this.left /= <>
      Ensures:
      this.left * this.right = #this.left * #this.right  and
|this.left| = |#this.left| - 1

    • swapRights

      void swapRights(List<T> list)
      Swaps the right strings of this and list.
      Parameters:
      list - the List whose right string is to be swapped with the right string of this
      Updates:
      this.right, list.right
      Ensures:
      this.left = #this.left  and  list.left = #list.left  and
this.right = #list.right  and  list.right = #this.right