Package components.list

Interface ListKernel<T>

Type Parameters:

T - type of ListKernel entries

All Superinterfaces:

Iterable<T>, Standard<List<T>>

All Known Subinterfaces:

List<T>

All Known Implementing Classes:

List1L, List2, List3, ListSecondary

public interface ListKernel<T>
extends Standard<List<T>>, Iterable<T>

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 Type	Method	Description
void	addRightFront(T x)	Adds x to the beginning of this.right.
void	advance()	Advances the position in this by one.
int	leftLength()	Reports length of this.left.
void	moveToStart()	Moves the position in this to the beginning.
T	removeRightFront()	Removes and returns the entry at the front of this.right.
int	rightLength()	Reports length of this.right.

Methods inherited from interface java.lang.Iterable

forEach, iterator, spliterator

Methods inherited from interface components.standard.Standard

clear, newInstance, transferFrom

Method Details

addRightFront

void addRightFront(T x)

Adds x to the beginning of this.right.

Parameters:

x - the entry to be added

Aliases:

reference x

Updates:

this.right

Ensures:

this.right = <x> * #this.right

removeRightFront

T removeRightFront()

Removes and returns the entry at the front of this.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 in this 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 in this to the beginning.

Updates:

this

Ensures:

this.right = #this.left * #this.right and |this.left| = 0

leftLength

int leftLength()

Reports length of this.left.

Returns:

the length of this.left

Ensures:

leftLength = |this.left|

rightLength

int rightLength()

Reports length of this.right.

Returns:

the length of this.right

Ensures:

rightLength = |this.right|