MANUAL DEL USUARIO
Documento por Vladimir Támara.
Porciones debidas a Cesar Muñoz y Hernán Aponte
Mayo de 1997, Santafé de Bogotá D.C. COLOMBIA
Universidad de los Andes, Derechos Reservados 1985 - 1997
Este documento está disponible en formato HTML como comprimido ZIP (35K) o tar.gz (35K)
|
|
1.2. Referencias |
|---|---|
|
|
2.2. Windows 95/NT 2.3. UNIX/LINUX |
|
|
3.2. Mensajes 3.3. Menús 3.4. Palabras Clave 3.5. Plantillas |
|
|
4.2. Menús y Editor 4.3. Trabajando con ManTa
|
| 5. CÓDIGO GENERADO | 5.1. Archivos Generados 5.2. Banco de Pruebas |
|
|
|
ManTa es un sistema para la manipulación de Tipos Abstractos de Datos (TADs), que permite:
En este manual se describe la operación de la versión 3.1 de este sistema. Se asume que el lector tiene familiaridad con la teoría de TADs. Si no la tiene puede consultar el Tutorial o los documentos de nuestro sitio WEB.
ManTa es un sistema desarrollado en la Universidad de los Andes bajo asesoría del profesor Rodrigo Cardoso. Los ejecutables y las fuentes están disponibles al público bajo la GNU General Public License.
[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.
Requerimientos:
Descomprima los precompilados con pkunzip en DOS o Winzip en Windows. Asegurese de activar la opción para crear subdirectorios:
pkunzip -d manta.zip
Continúe consultando las instrucciones en la sección 2.4.
Requerimientos:
Empleando pkunzip o Winzip descomprima los precompilados. En nuestro sitio WEB encontrará un PkUnzip que le permite manejar nombres largos. Asegúrese de activar la opción para crear subdirectorios
pkunzip -d manta.zip
Continúe consultando las instrucciones en la sección 2.4.
Requerimientos:
Descomprima los precompilados con gzip:
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.
La estructura de directorios que obtendrá será algo como:
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
Cámbiese al directorio d_manta, ahora puede editar el archivo de configuración para ajustarlo a sus preferencias y a su sistema operativo. Es particularmente importante que configure bien el editor de texto que ManTa empleará. Si quiere comenzar rápidamente sin leer el capítulo 3 edite el archivo manta.ini y modifique la segunda línea, coloque allí el nombre del editor de texto que planee usar (e.g. edit en DOS, vi, pico o emacs en UNIX) entre puntos (e.g: .edit.). Además asegúrese de que la primera línea sea .0.
Desde el mismo directorio d_manta puede teclear manta para iniciar una sesión con ManTa. Ya ha completado la instalación.
Los siguientes aspectos pueden configurarse en ManTa 3.1:
Todos los archivos de configuración tienen el mismo formato, las cadenas de caracteres siempre deben colocarse entre puntos. Cadenas que no aparezcan entre puntos se consideran comentarios dentro del archivo. Los números los archivos al comienzo de cada línea deben ir seguidos de un espacio en blanco.
El archivo principal de configuración es manta.ini, que se debe encontrar en el directorio d_manta. El formato de este archivo se presenta a continuación.
.<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
Por defecto manta emplea archivos de menús, palabras clave, plantillas y mensajes en español, aunque también hay versiones de estos archivos en ingles. Puede reemplazar el archivo manta.ini o emplear la opción -p al iniciar ManTa (ver Cap. 4), con otros archivos de configuración. En el directorio d_manta podrá encontrar los siguientes archivos de configuración además de manta.ini:
En el archivo manta.ini (Ver 3.1), las cadenas <archivo_mensajes> y <dir_mensaje> especifican el archivo de mensajes. Este es un archivo tipo texto y cada una de sus líneas tiene el siguiente formato:
# .<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 caracter punto.
ManTa se distribuye con dos archivos de mensajes, ubicados en el directorio D_MENSAJ (Ver 2.4):
En el archivo manta.ini (Ver 3.1), las cadenas <archivo_menus> y <dir_mensaje> especifican el archivo de menús. Este es un archivo tipo texto
En el archivo manta.ini (Ver 3.1), las cadenas <archivo_pal_clave> y <dir_mensaje> especifican el archivo de palabras clave del lenguaje. Estas palabras pueden ser cambiadas a gusto del usuario, aunque se recomienda no hacerlo para evitar problemas de portabilidad o con futuras versiones de Manta. Este archivo tipo texto tiene el siguiente formato:
.<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
ManTa se distribuye con dos archivos de palabras clave, ubicados en el directorio D_MENSAJ (Ver 2.4):
En el archivo manta.ini (Ver 3.1), las cadenas .<enc_func.i>,<tad.c>,<tad.h>, <tad.mak>,<tad_cons.inc>,<tad_defs.h>,<tad_inter.c>,.<tad_inter.h> y <tad_main.c> junto con <dir_mensaje> especifican los archivos con plantillas que se emplearán al generar código en ANSI C.
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).
La sintaxis de invocación es:
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:
Toda la interacción en esta versión se hace por medio de Menús. Puede elegir la opción que desee tecleándola, o tecleando algunas letras iniciales y después presionando ENTER. Si varias opciones de un mismo menú comienzan con las mismas letras digitadas, se escoge la primera de izquierda a derecha. (e.g. En el menú inicial tanto Tipos como Teoremas comienzan con T, si escribe T entrara al menú de Tipos, porque está primero). Todo menú tiene la opción Salir, para regresar al menú anterior (o al sistema en el caso del menú principal). Presionar ENTER sin escribir opción alguna equivale a escoger Salir.
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)
En ManTa los TADs y las representaciones pueden estar en el ambiente (memoria) o en disco. Siempre que se inicia una sesión con ManTa se cargan los TADs BOOL y NAT en el ambiente, a estos tipos se les llama básicos y no es posible modificarlos ni borrarlos. En ManTa existen los conceptos de TAD actual y Representación actual, el nombre del TAD actual aparece en todo menú. Al iniciar ManTa el TAD actual es BOOL.
El menú principal tiene las opciones: Tipos, Representaciones, Teoremas, Prototipos y Salir, que se explican en detalle a continuación.
|
Opción |
Descripción |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Opción Nuevo: Al escoger esta opción aparece una ventana con los nombres de todos los TADs conocidos y se piede al usuario el nombre del nuevo TAD. Después aparece el menu de Definición de Tipo.
Opción editar: El sistema pide el TAD que se desea editar. Luego aparece un menú de edición.
Para trabajar con representaciones es necesario cargarlas antes del disco. En el ambiente (memoria) siempre hay una Representación activa. Sobre esta actúan varias operaciones como editar y salvar.
|
Opción |
Descripción |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Salir | Retorna al menú principal |
Opción Nuevo: Al escoger esta opción se le solicitarán los nombres de los TAD fuente y destino, después vera el Menú de Definición de Representación.
Opción editar: El sistema pide la Representación que se desea editar. Luego aparece un menú de edición.
En el ambiente existe una lista con las conjeturas probadas y otra con las conjeturas no probadas. Estas listas se colocan en vacío siempre que se entre al menú de teoremas.
|
Opción |
Descripción |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Opción |
Descripción |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Los archivos que se generan para implantar un TAD de nombre X son:
Todos estos archivos se generan totalmente documentados con las plantillas del directorio de plantillas.
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.
El banco de pruebas tiene una lista con todos los objetos que se han creado en su ejecución (ambiente). Esta lista de objetos se despliega en la parte derecha de la pantalla. Al iniciar la ejecución la lista está vacía.
Al ejecutarlo despliega un menú que contiene:
Se muestra un menú con las opciones:
Las otras opciones corresponden a tipos que se han implantado con el banco de pruebas. Estas opciones despliegan menús que contienen:
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:
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
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)
Si Ud.
es usuario de DOS sin soporte para nombres largos se recomienda emplear
nombres de menos de 5 caracteres de longitud.