Package components.queue
Interface QueueKernel<T>
- Type Parameters:
T
- type ofQueueKernel
entries
- All Known Subinterfaces:
Queue<T>
- All Known Implementing Classes:
Queue1L
,Queue2
,Queue3
,QueueSecondary
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
Methods inherited from interface java.lang.Iterable
forEach, iterator, spliterator
Methods inherited from interface components.standard.Standard
clear, newInstance, transferFrom
-
Method Details
-
enqueue
Addsx
to the end ofthis
.- Parameters:
x
- the entry to be added- Aliases:
- reference
x
- Updates:
this
- Ensures:
this = #this * <x>
-
dequeue
Removes and returns the entry at the front ofthis
.- Returns:
- the entry removed
- Updates:
this
- Requires:
this /= <>
- Ensures:
#this = <dequeue> * this
-
length
int length()Reports length ofthis
.- Returns:
- the length of
this
- Ensures:
length = |this|
-