Package components.list
Interface ListKernel<T>
- Type Parameters:
T
- type ofListKernel
entries
- All Known Subinterfaces:
List<T>
- All Known Implementing Classes:
List1L
,List2
,List3
,ListSecondary
List kernel component with primary methods. (Note: by package-wide
convention, all references are non-null.)
- Mathematical Subtypes:
LIST_MODEL is ( left: string of T, right: string of T )
- Mathematical Model (abstract value and abstract invariant of this):
type ListKernel is modeled by LIST_MODEL
- Constructor(s) (initial abstract value(s) of this):
(): ensures this = (<>, <>)
- Iterator String (abstract value of ~this):
~this.seen * ~this.unseen = this.left * this.right
-
Method Summary
Modifier and TypeMethodDescriptionvoid
addRightFront
(T x) Addsx
to the beginning ofthis.right
.void
advance()
Advances the position inthis
by one.int
Reports length ofthis.left
.void
Moves the position inthis
to the beginning.Removes and returns the entry at the front ofthis.right
.int
Reports length ofthis.right
.Methods inherited from interface java.lang.Iterable
forEach, iterator, spliterator
Methods inherited from interface components.standard.Standard
clear, newInstance, transferFrom
-
Method Details
-
addRightFront
Addsx
to the beginning ofthis.right
.- Parameters:
x
- the entry to be added- Aliases:
- reference
x
- Updates:
this.right
- Ensures:
this.right = <x> * #this.right
-
removeRightFront
Removes and returns the entry at the front ofthis.right
.- Returns:
- the front entry of
this.right
- Updates:
this.right
- Requires:
this.right /= <>
- Ensures:
#this.right = <removeRightFront> * this.right
-
advance
void advance()Advances the position inthis
by one.- Updates:
this
- Requires:
this.right /= <>
- Ensures:
this.left * this.right = #this.left * #this.right and |this.left| = |#this.left| + 1
-
moveToStart
void moveToStart()Moves the position inthis
to the beginning.- Updates:
this
- Ensures:
this.right = #this.left * #this.right and |this.left| = 0
-
leftLength
int leftLength()Reports length ofthis.left
.- Returns:
- the length of
this.left
- Ensures:
leftLength = |this.left|
-
rightLength
int rightLength()Reports length ofthis.right
.- Returns:
- the length of
this.right
- Ensures:
rightLength = |this.right|
-