Interface QueueKernel<T>

Type Parameters:

T - type of QueueKernel entries

All Superinterfaces:

Iterable<T>, Standard<Queue<T>>

All Known Subinterfaces:

Queue<T>

All Known Implementing Classes:

Queue1L, Queue2, Queue3, QueueSecondary

public interface QueueKernel<T>
extends Standard<Queue<T>>, Iterable<T>

First-in-first-out (FIFO) queue 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 QueueKernel 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
T	dequeue()	Removes and returns the entry at the front of this.
void	enqueue(T x)	Adds x to the end of this.
int	length()	Reports length of this.

Methods inherited from interface Iterable

forEach, iterator, spliterator

Methods inherited from interface Standard

clear, newInstance, transferFrom

Method Details

enqueue

void enqueue(T x)

Adds x to the end of this.

Parameters:

x - the entry to be added

Aliases:

reference x

Updates:

this

Ensures:

this = #this * <x>

dequeue

T dequeue()

Removes and returns the entry at the front of this.

Returns:

the entry removed

Updates:

this

Requires:

this /= <>

Ensures:

#this = <dequeue> * this

length

int length()

Reports length of this.

Returns:

the length of this

Ensures:

length = |this|