En conclusión para definir un TAD basta:
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) -> BOOLGuarde 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.