Package components.sortingmachine

Interface SortingMachineKernel<T>

Type Parameters:
T - type of SortingMachineKernel entries
All Superinterfaces:
Iterable<T>, Standard<SortingMachine<T>>
All Known Subinterfaces:
SortingMachine<T>
All Known Implementing Classes:
SortingMachine1L, SortingMachine2, SortingMachine3, SortingMachine4, SortingMachine5, SortingMachineSecondary
public interface SortingMachineKernel<T> extends Standard<SortingMachine<T>>, Iterable<T>
Sorting machine kernel component with primary methods. (Note: by package-wide convention, all references are non-null.)
Mathematical Subtypes:
SORTING_MACHINE_MODEL is (
  insertion_mode: boolean,
  ordering: binary relation on T,
  contents: finite multiset of T
 )
 exemplar m
 constraint
  IS_TOTAL_PREORDER(m.ordering)
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)))
Mathematical Model (abstract value and abstract invariant of this):
type SortingMachineKernel is modeled by SORTING_MACHINE_MODEL
Constructor(s) (initial abstract value(s) of this):
(Comparator<T> order):
 aliases reference {@code order}
 requires
  IS_TOTAL_PREORDER(order)
 ensures
  this = (true, order, {})
Iterator String (abstract value of ~this):
multiset_entries(~this.seen * ~this.unseen) = this.contents

  • Method Details

    • add

      void add(T x)
      Adds x to the contents of this.
      Parameters:
      x - the element to be added
      Aliases:
      reference x
      Updates:
      this.contents
      Requires:
      this.insertion_mode
      Ensures:
      this.contents = #this.contents union {x}

    • changeToExtractionMode

      void changeToExtractionMode()
      Changes the mode of this from insertion to extraction.
      Updates:
      this.insertion_mode
      Requires:
      this.insertion_mode
      Ensures:
      not this.insertion_mode

    • removeFirst

      T removeFirst()
      Removes and returns some "first" ("smallest") entry from the contents of this.
      Returns:
      the entry removed
      Updates:
      this.contents
      Requires:
      not this.insertion_mode  and
this.contents /= {}
      Ensures:
      removeFirst is in #this.contents  and
for all x: T where (x is in #this.contents)
 (this.ordering(removeFirst, x))  and
this.contents = #this.contents \ {removeFirst}

    • isInInsertionMode

      boolean isInInsertionMode()
      Reports whether this is in insertion mode.
      Returns:
      true iff this is in insertion mode
      Ensures:
      isInInsertionMode = this.insertion_mode

    • order

      Comparator<T> order()
      Reports Comparator being used for sorting by this.
      Returns:
      Comparator used for sorting
      Aliases:
      reference returned by order
      Ensures:
      order = [Comparator used in the constructor call that created this]

    • size

      int size()
      Reports the number of entries in this.
      Returns:
      the (multiset) size of this.contents
      Ensures:
      size = |this.contents|