Interface Queue<T>

Type Parameters:
T - type of Queue entries
All Superinterfaces:
Iterable<T>, QueueKernel<T>, Standard<Queue<T>>
All Known Implementing Classes:
Queue1L, Queue2, Queue3, QueueSecondary
public interface Queue<T> extends QueueKernel<T>
QueueKernel enhanced with secondary methods.
Mathematical Definitions:
IS_TOTAL_PREORDER (
 r: binary relation on T
) : boolean is
for all x, y, z: T
 ((r(x, y) or r(y, x))  and
  (if (r(x, y) and r(y, z)) then r(x, z)))

IS_SORTED (
 s: string of T,
 r: binary relation on T
) : boolean is
for all x, y: T where (<x, y> is substring of s) (r(x, y))

  • Method Details

    • front

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

    • replaceFront

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

    • append

      void append(Queue<T> q)
      Concatenates ("appends") q to the end of this.
      Parameters:
      q - the Queue to be appended to the end of this
      Updates:
      this
      Clears:
      q
      Ensures:
      this = #this * #q

    • flip

      void flip()
      Reverses ("flips") this.
      Updates:
      this
      Ensures:
      this = rev(#this)

    • sort

      void sort(Comparator<T> order)
      Sorts this according to the ordering provided by the compare method from order.
      Parameters:
      order - ordering by which to sort
      Updates:
      this
      Requires:
      IS_TOTAL_PREORDER([relation computed by order.compare method])
      Ensures:
      perms(this, #this)  and
IS_SORTED(this, [relation computed by order.compare method])

    • rotate

      void rotate(int distance)
      Rotates this.
      Parameters:
      distance - distance by which to rotate
      Updates:
      this
      Ensures:
      if #this = <> then
this = #this
else
this = #this[distance mod |#this|, |#this|) * #this[0, distance mod |#this|)