Interface SequenceKernel<T>

Type Parameters:

T - type of SequenceKernel entries

All Superinterfaces:

Iterable<T>, Standard<Sequence<T>>

All Known Subinterfaces:

Sequence<T>

All Known Implementing Classes:

Sequence1L, Sequence2L, Sequence3, SequenceSecondary

public interface SequenceKernel<T>
extends Standard<Sequence<T>>, Iterable<T>

Sequence kernel component with primary methods. (Note: by package-wide convention, all references are non-null.)

Mathematical Model (abstract value and abstract invariant of this):

type SequenceKernel is modeled by string of T

Constructor(s) (initial abstract value(s) of this):

():
ensures
 this = <>

Iterator String (abstract value of ~this):

~this.seen * ~this.unseen = this

Method Summary

Modifier and Type	Method	Description
void	add(int pos, T x)	Adds the entry x at position pos of this.
int	length()	Reports the length of this.
T	remove(int pos)	Removes and returns the entry at position pos of this .

Methods inherited from interface Iterable

forEach, iterator, spliterator

Methods inherited from interface Standard

clear, newInstance, transferFrom

Method Details

add

void add(int pos,
 T x)

Adds the entry x at position pos of this.

Parameters:

pos - the position at which to add an entry

x - the entry to be added

Aliases:

reference x

Updates:

this

Requires:

0 <= pos and pos <= |this|

Ensures:

this = #this[0, pos) * <x> * #this[pos, |#this|)

remove

T remove(int pos)

Removes and returns the entry at position pos of this .

Parameters:

pos - the position at which to remove an entry

Returns:

the entry removed

Updates:

this

Requires:

0 <= pos and pos < |this|

Ensures:

this = #this[0, pos) * #this[pos+1, |#this|)  and
<remove> = #this[pos, pos+1)

length

int length()

Reports the length of this.

Returns:

the length

Ensures:

length = |this|