Especificación e implementación de pilas en Pascal: TAD Pila con ejemplos

Especificación de Pilas

Parámetros genéricos

Tipos

TipoElemento

Fin parámetros genéricos

Tipos

TipoPila

Operaciones

Constructoras generadoras

CrearPilaVacia : → TipoPila

Apilar : TipoElemento × TipoPila → TipoPila

Observadoras selectoras

parcial Cima : TipoPila → TipoElemento

Observadoras no selectoras

EsPilaVacia : TipoPila → booleano

IgualPila : TipoPila × TipoPila → booleano

Constructoras no generadoras

parcial Desapilar : TipoPila → TipoPila

CopiarPila : TipoPila → TipoPila

Variables

pila, pila2, pila3 : TipoPila;
elemento, elem : TipoElemento;

Ecuaciones de definitud

Def(Cima(Apilar(elemento, pila)))
Def(Desapilar(Apilar(elemento, pila)))

Ecuaciones

EsPilaVacia(CrearPilaVacia) = CIERTO
EsPilaVacia(Apilar(elemento, pila)) = FALSO
Cima(Apilar(elemento, pila)) = elemento
Desapilar(Apilar(elemento, pila)) = pila
CopiarPila(CrearPilaVacia) = CrearPilaVacia
CopiarPila(Apilar(elemento, pila)) = Apilar(elemento, CopiarPila(pila))
IgualPila(CrearPilaVacia, pila2) = EsPilaVacia(pila2)
IgualPila(Apilar(elemento, pila), pila2) = SI EsPilaVacia(pila2) → FALSO | SI pila2 = Apilar(elem, pila3) → (elemento = elem) Y IgualPila(pila, pila3)

Implementación en Pascal

Interface

USES TElemento;

TYPE
TipoPila = ^TipoNodo;
TipoNodo = RECORD
dato: TipoElemento;
siguiente: TipoPila
END; (* registro *)

PROCEDURE CrearPilaVacia(VAR pila: TipoPila);
(* POST: