Package components.stack

Interface StackKernel<T>

Type Parameters:

T - type of StackKernel entries

All Superinterfaces:

Iterable<T>, Standard<Stack<T>>

All Known Subinterfaces:

Stack<T>

All Known Implementing Classes:

Stack1L, Stack2, Stack3, StackSecondary

public interface StackKernel<T>
extends Standard<Stack<T>>, Iterable<T>

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

Modifier and Type	Method	Description
int	length()	Reports length of this.
T	pop()	Removes and returns the entry at the top of this.
void	push(T x)	Adds x to the top of this.

Methods inherited from interface java.lang.Iterable

forEach, iterator, spliterator

Methods inherited from interface components.standard.Standard

clear, newInstance, transferFrom

Method Details

push

void push(T x)

Adds x to the top of this.

Parameters:

x - the entry to be added

Aliases:

reference x

Updates:

this

Ensures:

this = <x> * #this

pop

T pop()

Removes and returns the entry at the top of this.

Returns:

the entry removed

Updates:

this

Requires:

this /= <>

Ensures:

#this = <pop> * this

length

int length()

Reports length of this.

Returns:

the length of this

Ensures:

length = |this|