Package components.stack
Interface StackKernel<T>
- Type Parameters:
T
- type ofStackKernel
entries
- All Known Subinterfaces:
Stack<T>
- All Known Implementing Classes:
Stack1L
,Stack2
,Stack3
,StackSecondary
Last-in-first-out (LIFO) stack 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 StackKernel 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
-
push
Addsx
to the top ofthis
.- Parameters:
x
- the entry to be added- Aliases:
- reference
x
- Updates:
this
- Ensures:
this = <x> * #this
-
pop
Removesx
from the top ofthis
.- Returns:
- the entry removed
- Updates:
this
- Requires:
this /= <>
- Ensures:
#this = <pop> * this
-
length
int length()Reports length ofthis
.- Returns:
- the length of
this
- Ensures:
length = |this|
-