1. INTRODUCCIÓN

• Crear nuevos tipos inductivos con un lenguaje de especificación recursivo bastante sencillo e intuitivo.
• Representar unos tipos empleando otros (e.g. Representar el TAD Cola con el TAD Pila)
• Probar teoremas con respecto a los tipos creados
• Generar código en C, que implementa los tipos especificados

1.1. Nota Legal

1.2. Referencias

[1]     CARDOSO, Rodrigo.  Verificación y Desarrollo de Programas.
        Ediciones Uniandes. 1ra edición. 1993.

[2]     MUÑOZ, Cesar.  ManTa: Un sistema para la implantación certificada y
        automática de Tipos Abstractos de Datos.  Tesis de Magister en Ingeniería de
        Sistemas y Computación. Universidad de los Andes. 1992.

[3]     APONTE, Hernán.  MANTA 3.0: Un sistema para la implantación certificada y
        automática de tipos abstractos de datos.  Tesis de Magister en Ingeniería de
        Sistemas y Computación.   Universidad de los Andes. 1995
 
[4]     Tutorial de Manta

[5]     TORO, Victor Manuel. Organización y documentación de programas grandes en C 
        (ANSI), Memo de investigación 52, Circulación privada Centro de Documentación
        de la Facultad de Ingeniería de la Universidad de los Andes, 1991.

2. INSTALACIÓN DE MANTA

2.1. DOS / Windows 3.1

• DOS de 32 bits o Windows 3.1 s32. Si solo tiene DOS de 16 bits, necesitará un servidor de DPMI. Se recomienda CWSDPMI, que puede obtener en nuestro sitio WEB.
• Pkunzip o Winzip
• 800KB en Disco Duro.

pkunzip -d manta.zip

Continúe consultando las instrucciones en la sección 2.4.

2.2. Windows 95/NT

• Windows 95 o NT
• Pkunzip o Winzip
• 800KB en Disco Duro.

pkunzip -d manta.zip

Continúe consultando las instrucciones en la sección 2.4.

2.3. UNIX/LINUX

• Sistema Operativo Unix o Linux
• Utilidades gzip y tar
• 800KB en Disco
• Si no había disponibles precompilados en nuestro sitio WEB para su plataforma, deberá bajar las fuentes que pueden compilarse con herramientas GNU.

gzip -d manta.tar.gz

Separa los archivos con tar:

tar xvf manta.tar

Continúe consultando las instrucciones en la sección 2.4.

2.4. Directorios

d_manta -                 Ejecutables y archivo de configuración
        |
        -- D_ADT          Archivos con TADs
        |
        -- D_MENSAJ       Mensajes, Palabras Claves y Menús
        |
        -- D_PLANT        Plantillas para generación de código
        |
        -- D_PRNADT       TADs impresos
        |
        -- D_PROT         Prototipos
        |
        -- D_THEO         Teoremas probados y Conjeturas no Probadas

Desde el mismo directorio d_manta puede teclear manta para iniciar una sesión con ManTa. Ya ha completado la instalación.

3. CONFIGURACIÓN

1. Interfaz plana o emacs
2. Editor de texto
3. Opciones del editor de texto
4. Directorios de Trabajo
5. Mensajes presentados al usuario
6. Menús
7. Palabras claves del lenguaje
8. Plantillas para generación de código

3.1. Archivo de Inicio

.<Interfaz EMACS>. 0 si desea interfaz plana, 1 si desea interfaz EMACS
.<editor>.         Nombre del editor de texto que se empleará
.<opcion1>.        Opción del editor para ir a una línea del archivo 
.<opcion2>.        Opción del editor para editar en modo solo-lectura
.<dir_mensaje>.    Directorio de mensajes del sistema
.<dir_plant>.      Directorio de plantillas de código
.<dir_tads>.       Directorio para guardar archivos con TADs
.<dir_reps>.       Directorio para guardar archivos con Representaciones
.<dir_tads_impr>.  Directorio para guardar TADs impresos
.<dir_rep_impr>.   Directorio para guardar representaciones impresas
.<dir_conj>.       Directorio para guardar conjeturas y teoremas
.<dir_prot>.       Directorio para guardar prototipos
.. Línea en blanco
.<archivo_pal_claves>. Archivo con palabras clave
.<archivo_menus>.      Archivo con definición de menús
.<archivo_mensajes>.   Archivo de mensajes
.<enc_func.i>.         Archivo con la plantilla de encabezado de funciones
.<tad.c>.              Archivo con plantilla de las selectoras
.<tad.h>.              Archivo con plantilla de encabezado de selectoras
.<tad.mak>.            Archivo con plantilla del makefile
.<tad_cons.inc>.       Archivo con plantilla para constructoras
.<tad_defs.h>.         Archivo con plantilla para definición de datos
.<tad_inter.c>.        Archivo con plantilla para funciones de interfaz
.<tad_inter.h>.        Archivo con plantilla para encabezados de funciones de interfaz
.<tad_main.c>.         Archivo con plantilla para el programa principal

• mantaeng.ini: Menús, mensajes, plantillas y palabras clave en inglés.
• mandos.ini: Configurado para emplear archivo en español y el editor edit de DOS (este editor no cuenta con opciones para ir a una línea ni para abrir un archivo como sólo lectura).
• manunix.ini: Configurado para emplear archivos en español y el editor vi de unix.

3.2. Mensajes

# .<mensaje>.

El número # que aparece en cada línea es el código interno del mensaje, es requerido un espacio después del código. Los puntos que aparecen a los lados de cada cadena son requeridos. El mensaje puede contener caracteres de control como \n, \t, %d, %s e incluso el carácter punto.

ManTa se distribuye con dos archivos de mensajes, ubicados en el directorio D_MENSAJ (Ver 2.4):

• messaesp.msg mensajes en español
• messaeng.msg mensajes en inglés

3.3. Menús

• menusesp.msg menús en español
• menuseng.msg menús en inglés

3.4. Palabras Clave

.<TAD>. Palabra que indica comienzo de un TAD
.<INICIALIZADORAS>. Palabra que indica comienzo de inicializadoras. 
.<CONSTRUCTORAS>. Palabra que indica comienzo de constructoras. 
.<SELECTORAS>. Palabra que indica comienzo de funciones selectoras
.<AXIOMAS>. Palabra que indica comienzo de axiomas
.<REP_ADT>. Palabra que indica TAD que representa
.<OPERACION_AUXILIAR>. Directorio para guardar archivos con Representaciones
.<PROGRAMAS>. Directorio para guardar TADs impresos
.<IF>. Directorio para guardar representaciones impresas
.<THEN>. Directorio para guardar conjeturas y teoremas
.<ELSE>. Directorio para guardar prototipos
.<THEN>. Directorio para guardar prototipos
.<ERROR>. Directorio para guardar prototipos
.<EQUAL>. Directorio para guardar prototipos
.<C>. Directorio para guardar prototipos
.<I>. Directorio para guardar prototipos
.<FI>. Directorio para guardar prototipos

• claves.msg palabras clave en español
• keywords.msg palabras clave en inglés

3.5. Plantillas

Las plantillas incluidas en la distribución de la versión 3.1 de ManTa, se crearon según los Estándares de Documentación de Código Fuente en C de Victor Toro [5].

Hay versiones en ingles de las plantillas, en el directorio D_PLANT (Ver 2.4).

4. INTERFAZ

4.1. Inicio de una sesión con ManTa

manta [-i <archivo>]

[-i <NomArc>] Indica que debe usarse el archivo cuyo nombre es <NomArc> como archivo de configuración del sistema. Si el programa se invoca sin esta opción el archivo de configuración será manta.ini. Una vez haya comenzado una sesión debe aparecer en pantalla:

4.2. Menús y Edición

Es indispensable un editor de texto para realizar muchas operaciones en ManTa como crear, editar o ver tanto tipos como representaciones y teoremas. El editor empleado se indica en el archivo de configuración (Ver 3.1)

4.3. Uso de ManTa

El menú principal tiene las opciones: Tipos, Representaciones, Teoremas, Prototipos y Salir, que se explican en detalle a continuación.

4.3.1. Tipos

• Inductiva: El usuario debe editar la signatura y los axiomas del TAD. El sistema genera plantillas de edición para que sean completadas en el editor configurado. Terminada la edición el sistema verifica la sintaxis de las definiciones
• Instanciación: El sistema pide el TAD genérico, el parámetro que se desa instnaicar y el TAD con el cual se instancia
• Copia: El sistema pide el TAD que se desea copiar
• Producto Cartesiano: El sistema pide los TADs para hacer el producto cartesiano
• Restricción: El sistema pide el TAD sobre el cual se hace la restricción y la definición del predicado de restricción
• Extensión: Se presenta un menú con las opciones:
• Suma directa: El sistema pide los TAD para hace la suma directa
• Completación: El sistema pide el TAD que se desea completar, y el nombre del elemento de la completación
• Variación: El sistema pide los TAD para hacer la variación
• Salir: Retorna al menú de Definición de Tipo
• Salir: Retorna al menú de tipos

• Signatura: Permite la edición de la signatura del TAD. El sistema verifica la corrección sintáctica de la signatura.
• Axiomas: Permite la edición de los axiomas del TAD. El sistema despliega un menú para permitir al usuario elegir el axioma que desea editar.
• Estado: Permite cambiar el estado del TAD de modificable a inmodificable o viceversa.
• Todo: Despliega toda la información de la definición del TAD
• Salir: Retorna al menú de tipos

4.3.2. Representaciones

Opción	Descripción
Directorio	Despliega el directorio de representaciones en disco. Están ubicadas en el directorio indicado por <dir_reps> del archivo de configuración (Ver 3.1)
Nuevo	Entra a un Menú donde podrá definir una nueva Representación, que queda como Representación actual. Esta opción se explica en detalle más adelante Si Ud. es usuario de DOS sin soporte para nombres largos, tanto el TAD fuente como el TAD destino deben tener menos de 3 caracteres de longitud. Así mismo el nombre de la función de representación no debe exceder 3 caracteres.
Editar	Permite consultar o modificar una Representación del ambiente. La representación editada queda como actual. Esta opción se explica en detalle más adelante
Cargar	Permite cargar en el ambiente una representación del directorio de definiciones, para esto despliega un menú vertical que contiene todas las representaciones conocidas por el sistema.
Salvar	Salva la representación actual.
Probar	Verifica la corrección de la representación actual. El sistema informa cuantas conjeturas pudo probar y cuantas no. Finalmente despliega el archivo con las demostraciones de las conjeturas probadas y no probadas.
Imprimir	Guarda la representación actual en el directorio de archivos de impresión de representaciones.
Borrar	Borra la representación actual del ambiente y del disco
Salir	Retorna al menú principal

• Inductiva: Debe editar los programas de la representación y los axiomas de las funciones auxiliares. El sistema genera plantillas de edición que el usuario debe completar. Terminada la edición, el sistema verifica la sintaxis de las definiciones.
• Composición: El sistema pide, en orden, las representaciones que se van a componer.
• Salir: Retorna al menú de tipos

• Programas: Permite la edición de los programas de la representación. El sistema verifica la corrección sintáctica de estos.
• Operaciones Auxiliares: Muestra la signatura de las operaciones auxiliares de la representación
• Axiomas: Permite la edición de los axiomas de las operaciones auxiliares de la representación. El sistema despliega un menú que le permitirá escoger el axioma de una operación auxiliar a editar.
• Todo: Despliega toda la información de la definición de la representación
• Salir: Retorna al menú de representaciones

4.3.3. Teoremas

4.3.4. Prototipos

5. CODIGO GENERADO

5.1. Archivos Generados

• X_de.h Definición de constantes, macros y tipos del TAD
• X.h: Declaración de los encabezados de las funciones externas del TAD
• X_co.inc: Implantación de las funciones constructoras del TAD
• X.c: Implantación de las funciones selectoras del TAD
• X_in.h: Declaración de los encabezados de las funciones de interfaz externas del TAD.
• X_in.c: Implantación de las funciones de interfaz del TAD
• X_ma.c: Banco de pruebas del TAD
• X.mak: Archivo make para compilar el prototipo

• Para modificar manualmente las selectoras del TAD X se debe editar el archivo X.c.
• Para modificar la representación física de los datos se deben editar los archivo X_defs.h y X_cons.inc.
• Para modificar las funciones de interfaz (salvar, cargar, imprimir, borrar, copiar) se debe editar el archivo X_inter.c.
• Para modificar el banco de pruebas se debe editar el archivo X_main.c.
• Para cambiar de compilador, o las opciones de compilación, se debe editar el archivo X.mak.

5.2. El Banco de Pruebas

Al ejecutarlo despliega un menú que contiene:

• Una opción para manejar el ambiente de objetos
• Una opción con el nombre del TAD principal
• Una opción por cada TAD nombrado en la signatura del TAD principal

5.2.1.Ambiente

Se muestra un menú con las opciones:

• Salvar: Salva los objetos del ambiente en un archivo, cuyo nombre digita el usuario
• Cargar: Carga en el ambiente un archivo de objetos, cuyo nombre digita el usuario
• Borrar: Borra toda la lista de objetos

5.2.2. Tipos

Las otras opciones corresponden a tipos que se han implantado con el banco de pruebas. Estas opciones despliegan en menús que contienen:

• Una opción por cada función generadora o selectora del TAD. Para estas funciones se piden los parámetros correspondientes y se muestra en pantalla el resultado de la operación. Los parámetros pueden ser:
• De tipo NAT: En este caso se debe digita un número
• De tipo BOOL: En este caso se debe digita TRUE o FALSE
• De otro tipo: En este caso el usuario debe digitar el nombre de un objeto del ambiente que corresponda con el tipo solicitado.
Cuando el resultado es de un tipo no básico, el sistema pide un nombre para guardar el objeto en el ambiente. El usuario puede:
• Cancelar la entrada (presionando ENTER con una cadena vacía), en cuyo caso no se guarda en el ambiente.
• Digitar un nombre que no existe, en cuyo caso se crea un nuevo objeto en el ambiente y su valor será el resultado
• Digitar un nombre que exista en la lista (y que corresponda en tipo), y en tal caso se asigna al nombre el valor del resultado.

• Una opción para las funciones de interfaz. Se despliega un menú con las opciones
• Imprimir: Pide el nombre de un objeto del ambiente y lo imprime en pantalla
• Salvar: Pide el nombre de un objeto del ambiente y lo salva en un archivo
• Cargar: Pide el nombre de un archivo y carga el objeto guardado en este
• Copiar: Pide el nombre de un objeto del ambiente y el nombre del objeto donde se quiere copiar
• Borrar: Pide el nombre del objeto que se quiere borrar del ambiente
• Una opción de salir del banco de pruebas.

APENDICE A. TADs PRIMITIVOS

A.1. TAD BOOL

TAD BOOL [  ]

INICIALES
TRUE        :                                  -> BOOL
FALSE       :                                  -> BOOL

CONSTRUCTORAS

SELECTORAS
AND      (c): BOOL * BOOL(i)                   -> BOOL
OR       (c): BOOL * BOOL(i)                   -> BOOL
NOT      (c): BOOL(i)                          -> BOOL
IMP      (c): BOOL(i) * BOOL(i)                -> BOOL
EQ_BOOL  (c): BOOL(i) * BOOL(i)                -> BOOL

AXIOMAS

AND(B1,TRUE) = B1
AND(B1,FALSE) = FALSE

OR(B1,TRUE) = TRUE
OR(B1,FALSE) = B1

NOT(TRUE) = FALSE
NOT(FALSE) = TRUE

IMP(TRUE,TRUE) = TRUE
IMP(TRUE,FALSE) = FALSE
IMP(FALSE,TRUE) = TRUE
IMP(FALSE,FALSE) = TRUE

EQ_BOOL(TRUE,TRUE) = TRUE
EQ_BOOL(TRUE,FALSE) = FALSE
EQ_BOOL(FALSE,TRUE) = FALSE
EQ_BOOL(FALSE,FALSE) = TRUE

A.2. TAD NAT

TAD NAT [  ]

INICIALES
ZERO        :                                  -> NAT

CONSTRUCTORAS
SUC         : NAT                              -> NAT

SELECTORAS
ADD         : NAT * NAT(i)                     -> NAT
ISZERO      : NAT(i)                           -> BOOL
MULT        : NAT(i) * NAT                     -> NAT
PRED        : NAT(i)                           -> NAT
MAX         : NAT(i) * NAT(i)                  -> NAT
MIN         : NAT(i) * NAT(i)                  -> NAT
GT          : NAT(i) * NAT(i)                  -> BOOL
LT          : NAT(i) * NAT(i)                  -> BOOL
GE          : NAT * NAT                        -> BOOL
LE          : NAT * NAT                        -> BOOL
FACT        : NAT(i)                           -> NAT
EXP         : NAT * NAT(i)                     -> NAT
EVEN        : NAT(i)                           -> BOOL
ODD         : NAT(i)                           -> BOOL
DIV         : NAT * NAT                        -> NAT
MOD         : NAT * NAT                        -> NAT
DIVIDES     : NAT * NAT                        -> BOOL
SUBS        : NAT * NAT(i)                     -> NAT
EQ_NAT   (c): NAT(i) * NAT(i)                  -> BOOL

AXIOMAS

ADD(N1,ZERO) = N1
ADD(N1,SUC(N2)) = SUC(ADD(N1,N2))

ISZERO(ZERO) = TRUE
ISZERO(SUC(N1)) = FALSE

MULT(ZERO,N1) = ZERO
MULT(SUC(N1),N2) = ADD(MULT(N1,N2),N2)

PRED(ZERO) = ZERO
PRED(SUC(N1)) = N1

MAX(ZERO,ZERO) = ZERO
MAX(ZERO,SUC(N1)) = SUC(N1)
MAX(SUC(N1),ZERO) = SUC(N1)
MAX(SUC(N1),SUC(N2)) = SUC(MAX(N1,N2))

MIN(ZERO,ZERO) = ZERO
MIN(ZERO,SUC(N1)) = ZERO
MIN(SUC(N1),ZERO) = ZERO
MIN(SUC(N1),SUC(N2)) = SUC(MIN(N1,N2))

GT(ZERO,ZERO) = FALSE
GT(ZERO,SUC(N1)) = FALSE
GT(SUC(N1),ZERO) = TRUE
GT(SUC(N1),SUC(N2)) = GT(N1,N2)

LT(ZERO,ZERO) = FALSE
LT(ZERO,SUC(N1)) = TRUE
LT(SUC(N1),ZERO) = FALSE
LT(SUC(N1),SUC(N2)) = LT(N1,N2)

GE(N1,N2) = OR(EQ_NAT(N1,N2),GT(N1,N2))

LE(N1,N2) = OR(EQ_NAT(N1,N2),LT(N1,N2))

FACT(ZERO) = SUC(ZERO)
FACT(SUC(N1)) = MULT(SUC(N1),FACT(N1))

EXP(N1,ZERO) = SUC(ZERO)
EXP(N1,SUC(N2)) = MULT(EXP(N1,N2),N1)

EVEN(ZERO) = TRUE
EVEN(SUC(ZERO)) = FALSE
EVEN(SUC(SUC(N1))) = EVEN(N1)

ODD(ZERO) = FALSE
ODD(SUC(ZERO)) = TRUE
ODD(SUC(SUC(N1))) = ODD(N1)

DIV(N1,N2) = IF(ISZERO(N2),ERROR,IF(GE(N1,N2),SUC(DIV(SUBS(N1,N2),N2)),ZERO))

MOD(N1,N2) = IF(ISZERO(N2),ERROR,IF(GE(N1,N2),MOD(SUBS(N1,N2),N2),N1))

DIVIDES(N1,N2) = ISZERO(MOD(N2,N1))

SUBS(N1,ZERO) = N1
SUBS(N1,SUC(N2)) = PRED(SUBS(N1,N2))

EQ_NAT(ZERO,ZERO) = TRUE
EQ_NAT(ZERO,SUC(N1)) = FALSE
EQ_NAT(SUC(N1),ZERO) = FALSE
EQ_NAT(SUC(N1),SUC(N2)) = EQ_NAT(N1,N2)