SiguienteAnteriorContenido

1.1. Definición del TAD Pila 

A una descripción de un TAD como la presentada en la introducción de este capítulo, le llamamos la signatura del TAD. Ahora podemos escribir los axiomas o reglas que cumplen las funciones Selectoras. Estos axiomas simplemente dicen como actúan las selectoras sobre las inicializadoras y constructoras. No se escriben axiomas para inicializadoras ni constructoras. Así hemos completado la definición del TAD Pila. Note que se emplean los símbolos ERROR (que se puede emplear en todo TAD), y TRUE, FALSE que hacen parte del TAD BOOL.
 

En conclusión para definir un TAD basta:

  1. Escribir la signatura del TAD, es decir definir funciones inicializadoras, constructoras y selectoras y el dominio y codominio de cada una.
  2. Escribir axiomas para las funciones selectoras, o en otras palabras escribir como se comportan las funciones selectoras con las constructoras e inicializadoras.
Escribir un TAD en ManTa definido como se acaba de explicar es realmente sencillo:
 
 
Primero ejecute ManTa tecleando manta, en el directorio donde lo instaló. 
Entre al menú Tipos. Basta que teclee T (ManTa completara el resto del comando), después elija Nuevo 

Probablemente ya exista el TAD Pila en su directorio de TADs así que llame PIL al nuevo TAD. Cuando se crea un nuevo TAD que no se construye de otros existentes se llamará Inductivo. Elija Inductivo en el menú de Nuevos, ManTa lo dejara en el Editor que tenga configurado.  

Deberá editar primero la signatura del TAD, escriba la signatura guiándose con la plantilla que  queda abierta: 

  TAD PIL [X]
  INICIALES
    inicPIL: ->PIL
  CONSTRUCTORAS
    adicPIL:PIL*X->PIL
  SELECTORAS
    elimPIL:PIL (i) -> PIL
    infoPIL: PIL (i) -> X
    esPILVacia: PIL(i) -> BOOL
    EQ_PIL (c) : PIL (i) * PIL(i) -> BOOL
Guarde el archivo y salga del editor. Como notara las selectoras tienen una (i) junto a sus parámetros, esto indica a ManTa que el parámetro marcado con (i) podrá servir para hacer inducción en las demostraciones. Pronto se dará cuenta como escoger a que parámetros poner (i). Si tecleó bien la signatura, podrá empezar a definir los axiomas de las selectoras. Si cometió algún error ManTa le permitirá volver a editar el archivo y corregir los errores que tenga. 

Para cada selectora ManTa creará un archivo e invocará al editor de texto para que edite el axioma. Cada vez que complete un axioma guarde el archivo y salga del editor. Además de las selectoras que definimos ManTa siempre incluye una selectora para decidir igualdad entre  dos instancias de un mismo TAD (se llama EQ_PIL en nuestro caso) 

  elimPIL(inicPIL)=ERROR
  elimPIL(adicPIL(P1,X2))=P1

  infoPIL(inicPIL) = ERROR
  infoPIL(adicPIL(P1,X2))=X2

  esPILVacia(inicPIL)=TRUE
  esPILVacia(adicPIL(P1,X2))=FALSE

  EQ_PIL(inicPIL, inicPIL) = TRUE
  EQ_PIL(inicPIL,adicPIL(P1,X2))=FALSE
  EQ_PIL(adicPIL(P1,X2),inicPIL)=FALSE
  EQ_PIL(adicPIL(P1,X2),adicPIL(P3,X4))=AND(EQUAL(X2,X4),EQ_PIL(P1,P3))
Si comete algún error al teclear los axiomas el analizador de ManTa lo detectará, le informará el problema y le permitirá volver a escribir el axioma incorrecto. Una vez haya ingresado todos los axiomas, debe especificar el Estado del TAD, es decir si es Modificable o Inmodificable. Por ahora elija Modificable, vuelva al menú Tipos y salve el tipo recién creado. 
 

Si ha seguido bien las instrucciones ha logrado definir el TAD Pila.   Ya hizo su parte del trabajo, ahora el resto le corresponde a ManTa.  En la siguiente sección emplearemos el Demostrador de Teoremas de ManTa para verificar algunas propiedades del TAD recién creado.


SiguienteAnteriorContenido