Gu´ıa rápida sobre ejecución de especificaciones algebraicas en
Contents
1. nombre del m dulo entre llaves Aparece en primer lugar el nombre dado al par metro en el m dulo A continuaci n entre blancos y por ltimo el nombre de la teor a que define el par metro La teor a TRIV la proporciona el sistema Maude y consiste en la definici n de un tipo denominado Elt Si se quiere definir m s de un par metro estos se separan con comas tanto en la cabecera como cada vez que nos referimos al tipo de datos Cada vez que nos referimos en la especificaci n al tipo Pila debemos anotar a continuaci n entre llaves el nombre del par metro Cuando nos referimos en la especificaci n a los datos del par metro escribiremos el nombre del par metro seguido del signo y del nombre del tipo de datos del par metro Por ejemplo X E1 t Una vez definido el m dulo param trico debe definirse una vista que relacione el par metro con una especificaci n e La definici n de una vista comienza con la palabra reservada view a continuaci n se escribe el nombre de la vista la palabra reservada from el nombre de la teor a dada como par metro la palabra to el nombre de la especificaci n que queremos asociar al par metro y la palabra is e La l nea siguiente relaciona el tipo del par metro en nuestro caso Elt con el tipo de la especi ficaci n en nuestro caso Int e Si la teor a que estamos utilizando define operaciones es necesario relacionar en la vista las operaciones del par metro con las operaciones de la2. palabra ceq el identificador y los dos puntos a continuaci n la ecuaci n y la palabra if seguida de la condici n Las condiciones se escriben comprobando si dos t rminos son iguales diferentes y uniendo t rminos booleanos con las conectivas and or y not El identificador de las ecuaciones debe ser nico en el m dulo El m dulo termina con la palabra fmod Los m dulos van entre par ntesis para indicar al sistema que est n escritos en Full Maude 5 2 Parametrizaci n La especificaci n de un m dulo parametrizado es muy similar a la de los m dulos sin par metros La siguiente especificaci n define el TAD de las pilas fmod PILAXX TRIV is sort PilafX op op op op errorPila gt Pila X errorElemPila gt X Elt pila vacia gt PilatfX ctor apilar X Elt Pila X gt Pila X ctor op desapilar Pila X gt Pila X op cima Pila X gt X Elt op es pila vacia Pila X gt Bool var P PilatX var E X Elt eq desapilaril desapilar pila vacia errorPila eq desapilar2 desapilar apilar E P P eq cima1 cima pila vacia errorElemPila eq cima2 cimal apilar E P sE eq pilaVacial es pila vacia pila vacia true eq pilaVacia2 es pila vacia apilar E P false endfm view vInt from TRIV to INT is fmod PILA ENTEROS is sort Elt to Int including PILA vInt endy endfm El par metro se define a continuaci n del
3. teor a Esto se hace de forma similar a la relaci n entre los tipos op suma to _ _ e La vista acaba con la palabra endv Por ltimo se define el m dulo instanciado que es el que utilizaremos para reducir t rminos Se declara un m dulo funcional y se incluye la especificaci n de las pilas instanciada con el nombre de la vista 5 3 M dulos predefinidos Los m dulos predefinidos se encuentran en el fichero prelude maude que se proporciona con el sistema Para poder utilizar los tipos definidos en estos m dulos excepto BOOL debe importarse el m dulo correspondiente Tenemos entre otros BOOL define los valores true y false y las operaciones _and or_ xor not implies NAT define los n meros naturales Estos n meros pueden utilizarse en notaci n decimal Algunas de las operaciones que proporciona son _ sd Nat Nat Nat para la diferencia y _ a INT define los n meros enteros Estos n meros pueden utilizarse en notaci n decimal Algunas de las operaciones que proporciona son _ _ _ quo calcula el cociente de la divisi n entera _rem calcula el resto de la divisi n entera STRING En este m dulo se definen los tipos String y Char Tanto las cadenas de caracteres como los caracteres se escriben entre comillas dobles p e a o Hola Algunas de las operaciones que proporciona este m dulo son _ para la concatenaci n y lenght para calcular la longitud de una ca
4. 3 y el uso del lenguaje Full Maude en lugar del Core Maude La principal diferencia entre ambos lenguajes es que en Full Maude los m dulos deben escribirse entre par ntesis y se a ade un identificador a las ecuaciones El manual para ejecutar la herramienta de testing Manual para realizar testing de TADs especificados en Maude e implementados en C se proporciona por el Campus Virtual 2 Instalar Maude Para ejecutar Maude desde Linux y Mac se puede descargar el sistema gratuitamente desde la p gina principal de Maude http maude cs uiuc edu en el apartado download latest version of Maude 2 Para especificar tipos abstractos de datos es suficiente con descargar el sistema Core Maude 2 5 Las facilidades proporcionadas por Full Maude se utilizan en la generaci n de casos de prueba pero no es necesario bajarlas de este sitio web En esta p gina se encuentra tambi n disponible el manual completo del sistema un tutorial y otra documentaci n sobre el lenguaje Maude Para instalar Maude bajo Windows se recomienda utilizar el instalador desarrollado en la Univer sidad de Valencia dentro del proyecto MOMENT Se puede descargar gratuitamente desde la p gina http moment dsic upv es dentro del apartado Maude for Windows Descargad la versi n Maude for Windows 2 5 utilizando el bot n download Al realizar la instalaci n modificar la ruta en la que se insta lar el ejecutable para que no se utilicen directorios cuyo nombre tenga espacios
5. Gu a r pida sobre ejecuci n de especificaciones algebraicas en Maude bajo el entorno Eclipse para estudiantes de Estructuras de Datos Actualizado para poder utilizar la herramienta de testing Isabel Pita Dept Sistemas Inform ticos y Computaci n Universidad Complutense de Madrid ltima modificaci n 15 01 2011 1 Introducci n El presente manual es una gu a para ayudar a los estudiantes de la asignatura de Estructuras de Datos y de la Informaci n de segundo curso de Ingenier a Superior en Inform tica e Ingenier a T cnica en Inform tica de Sistemas de la UCM a ejecutar especificaciones algebraicas en lenguaje Maude El lenguaje Maude est disponible para Windows Linux y Mac Bajo Linux y Mac lo m s c modo es ejecutar Maude desde la l nea de comandos y utilizar un editor de texto para modificar los ficheros Para ejecutar Maude en Windows se han creado unos plugins que permiten ejecutar Maude bajo el entorno Eclipse El manual se compone de 1 Como instalar Maude bajo Linux Mac y Windows 2 Como instalar Eclipse para ejecutar Maude en Windows 3 Como definir una especificaci n algebraica sencilla y como ejecutarla 4 Conceptos b sicos de Maude Este manual ha sido actualizado para poder utilizar la herramienta de testing para probar imple mentaciones en C de los tipos de datos con las especificaciones realizadas Los principales cambios respecto a la versi n anterior son el entorno Eclipse utilizado sec
6. a activa por ello hay que asegurarse de que la ventana activa es la del editor en la que se encuentra la especificaci n que queremos ejecutar Si hemos cometido alg n error al escribir el m dulo y este no se ajusta a la sintaxis de Maude aparecer un mensaje en la consola donde se nos dice mas o menos en que consiste el error Arregladlo y volved a introducir el m dulo Cuando el m dulo se carga en el sistema sin problemas el sistema lo indica Cuando se introduce un m dulo que ya estaba en el sistema por haberse introducido anteriormente se produce un mensaje indicando que el m dulo ha sido redefinido Ahora podemos reducir t rminos en esta especificaci n Escribid por ejemplo el t rmino suma C 3 4 C 7 2 en el editor precedido por el comando red y acabado en todo ello entre par ntesis En Full Maude los comandos deben escribirse entre par ntesis red suma C 3 4 C 7 2 A continuaci n se leccionar la l nea y darle al bot n Send selection to Maude del men Maude En la consola aparece la respuesta del sistema Si el t rmino es correcto el sistema contestar result Complejo C 10 6 Cada vez que se cargue el m dulo en el sistema se reducir n todos los t rminos que aparezcan en el mismo precedidos de la palabra reservada red Para evitarlo se pueden comentar estas l neas Los comentarios est n precedidos por tres guiones Los guiones no deben seleccionarse al reducir los t rminos Otra forma de re
7. araci n acaba en un blanco seguido de un punto Cada operaci n se definir en una l nea y siguiendo esta sintaxis Las constructoras llevan el identificador ctor antes del punto final Las operaciones se pueden escribir en forma prefija o infija Para escribir una operaci n en for ma prefija escribimos unicamente su nombre Por ejemplo op sumar Int Int Complejo Los t rminos que utilizan esta operaci n la escriben como sumar A B Para escribir una operaci n en forma infija se escribe el s mbolo subrayado en el lugar donde deben aparecer los argumentos Por ejemplo op _ Int Int Complejo Los t rminos que utilizan esta operaci n la escriben como A B Las variables se separan del s mbolo de operaci n con un blanco Como se indic an teriormente este curso solo se utilizar n operaciones en notaci n prefija Si en la definici n de las ecuaciones hacen falta variables estas aparecen precedidas de la palabra var o vars si se definen varias variables del mismo tipo Si se declaran varias variables estas van separadas por blancos A continuaci n se escriben dos puntos el tipo de las variables y un punto Todo ello separado por uno o mas blancos Por ltimo se escriben las ecuaciones Van precedidas de la palabra eq seguida de un identificador entre corchetes y dos puntos A continuaci n los dos t rminos separados por el signo y finalizan con un blanco y un punto Las ecuaciones condicionales van precedidas de la
8. dena El resto de los m dulo predefinidos y las operaciones que no se han nombrado aqu pueden consultarse en el manual 5 4 Teor as predefinidas Existen varias teor as definidas por defecto en el fichero prelude maude Estas teor as pueden utilizarse sin necesidad de hacer ninguna declaraci n 1 TRIV declara un tipo Elt 2 STRICT WEAK ORDER declara el tipo Elt y una operaci n lt _ 3 TOTAL PREORDER declara el tipo Elt y una operaci n _ lt _ 4 DEFAULT declara un tipo Elt y una constante 0 Aunque existen muchas vistas predefinidas en el archivo prelude maude es preferible durante este curso que cada alumno defina las vistas que necesite
9. ducir t rminos es introducir el comando en la caja existente en la parte inferior de la consola Los t rminos se reducen en el ltimo m dulo que se carg en el sistema m dulo activo Para saber que m dulo se encuentra activo cuando queremos reducir un t rmino se puede introducir el comando show module que nos mostrar el m dulo activo a Si al cargar un m dulo o reducir un t rmino aparece la palabra executing en la parte superior de la consola es que el sistema est esperando alg n s mbolo que no se ha introducido o bien que se est realizando una reducci n infinita Para finalizar el programa pulsar el bot n de abandonar Maude Quit 5 Conceptos b sicos de Maude En este apartado solo se introducen los conceptos y la sintaxis de Maude necesarios para poder definir especificaciones de tipos de datos sencillos El lenguaje proporciona muchas mas facilidades de las que aqu se van a introducir Los estudiantes interesados en escribir especificaciones mas complejas o en utilizar una sintaxis mas completa pueden consultar el manual del lenguaje Para comentar una l nea de un fichero Maude se escriben tres guiones al iniciar la l nea 5 1 M dulos funcionales no parametrizados Las especificaciones algebraicas se escriben en Maude en m dulos funcionales Un ejemplo de m dulo funcional es el que se ha escrito en el apartado anterior para los n meros complejos Los m dulos funcionales empiezan con la palabra res
10. e Maude que se ha cargado en el punto 2 1 y a adirlo en el apartado Maude binary file se puede utilizar el browser que hay en la ventana e Indicar el path del fichero dd maude en el apartado de Full Maude File El fichero debe encon trarse en el mismo directorio que el ejecutable de Maude e Hay que indicar un directorio donde guardar los ficheros temporales log Como en el caso del workspace no utilizar directorios cuyo nombre tenga espacios Si se est n utilizando los ordenadores de la Facultad utilizad un directorio con permiso de escritura e Marcar la opci n de Run Full Maude e En la opcion Advance marcar Other en Operating System y escribir el siguiente comando cmd exe C bash c echo exec maudebin fullmaude Y interactive no tecla no wrap Sobre el valor por defecto nicamente se ha a adido la opci n no wrap al final e No es necesario modificar nada mas Pulsar Apply y Ok Ahora ya tenemos el espacio de trabajo preparado para escribir especificaciones y ejecutarlas 4 Como definir una especificaci n algebraica y ejecutarla En este apartado vamos a aprender a definir una especificaci n y ejecutarla Para ello utilizaremos como ejemplo una especificaci n de los n meros complejos con las operaciones de suma y resta Para poder definir una especificaci n Ejecutar Eclipse Seleccionar un espacio de trabajo directorio en el que se guardan los proyectos que se realicen Primero hay qu
11. e crear un proyecto En la opci n file seleccionar new y a continuaci n other Desplegar General y elegir Project Elegir un nombre para el proyecto si se va a utilizar el testing el proyecto se debe denominar Testing Atencion a las may sculas si no se va a utilizar el testing el nombre del proyecto es indiferente p e COMPLEJOS Pulsar Finish Observad que aparece el nombre del proyecto en la ventana Package En este momento si tenemos el fichero en formato texto ya creado podemos seleccionar en el men File la opci n de import En el desplegable seleccionar Archive File y pulsar Next Seleccionar el archivo a importar y el proyecto en el que se debe importar Un inconveniente de esta forma de a adir archivos a proyectos es que solo se admiten ficheros comprimidos Otra forma de a adir un fichero ya creado es crear un nuevo fichero en el proyecto como se explica a continuaci n y copiar el contenido del que ya existe Si no tenemos el archivo ya creado creamos un fichero Maude en el proyecto Para ello seleccionar en el men File la opci n Other y aqu en la opci n Maude elegir Maude file En el apartado Container debe seleccionarse el proyecto al que queremos que pertenezca este archivo En este caso seleccionad el proyecto Testing o COMPLEJOS Escribid un nombre para el archivo por ejemplo Complejos La extensi n del archivo debe ser maude Si el nombre del archivo no lleva la extensi n no se interpretar como un archiv
12. ervada fmod el nombre del m dulo y la palabra reservada is continuaci n aparecen otros m dulos que se necesitan en la definici n de esta especificaci n El nombre del m dulo que se importa va precedido de la palabra including Existen otras formas de importar m dulos para las que se utilizan las palabras reservadas protecting y extending La diferencia entre ellas est fuera del mbito del curso Los valores booleanos est n incluidos por defecto y no es necesario importarlos expl citamente A continuaci n precedido de la palabra sort aparece el nombre del tipo de datos que se va a definir seguido de un blanco y un punto En caso de definirse varios tipos de datos se dar an de uno en uno precedidos cada uno por la palabra sort Cuando existe una relaci n de subtipo todos los valores de un tipo pertenecen al otro tipo entre dos tipos se indica con la palabra reservada subsort Por ejemplo subsort Nat lt Int La definici n de cada operaci n va precedida de la palabra op A continuaci n aparece el nombre de la operaci n en forma prefija o infija dos puntos entre blancos y los tipos de los argumentos En el ejemplo el tipo Int que aparece en el m dulo de los n meros complejos esta definido en el m dulo INT que hemos importado ver los m dulos predefinidos en la Sec 5 4 Despu s de los argumentos se escribe una flecha gt consistente en un gui n y un signo mayor y el tipo del resultado de la operaci n La decl
13. estos pueden dar problemas al ejecutar Maude desde Eclipse y el testing Si ya se ten a una versi n instalada de Maude para Windows debe desinstalarse con el programa que se proporcionaba con la instalaci n antes de proceder a la nueva instalaci n Copiar el fichero dd maude que se proporciona a trav s del Campus Virtual en el directorio donde se encuentre el ejecutable de Maude Este fichero es necesario para ejecutar las especificaciones con la sintaxis de Full Maude y poder generar los casos de prueba La sintaxis de Full Maude es muy semejante a la de Maude y ser la utilizada en todas las especificaciones que se realicen este curso En caso de no tener acceso al Campus Virtual el alumno debe ponerse en contacto con la profesora de la asignatura para que le proporcione el fichero 3 Instalar Eclipse IDE for C C Developers con la opci n de ejecutar Maude y los casos de prueba En cursos anteriores se ha utilizado Eclipse Classic 3 5 0 como entorno de trabajo para Maude Este curso se utiliza el entorno Eclipse IDE for C C para tener un entorno integrado de ejecuci n de especificaciones Maude e implementaciones en C Este nuevo entorno se puede utilizar tanto para ejecutar especificaciones Maude como para hacer el testing Si se quiere seguir utilizando el entorno anterior solo se podr n ejecutar especificaciones Maude En este caso es preferible utilizar el manual del curso anterior A continuaci n nos centramos en la instalac
14. i n de Eclipse para el entorno integrado Para poder ejecutar Maude desde Eclipse es necesario tener instalado el JDK de Java version 6 0 Si no se tiene instalada se puede descargar gratuitamente desde la p gina http www java com El entorno Eclipse IDE for C C Developers se puede descargar desde la p gina http www eclipse org downloads Se debe seleccionar el sistema operativo que se vaya a utilizar Una vez descargado Eclipse para poder ejecutar Maude deben descargarse las herramientas de de sarrollo para Maude del proyecto MOMENT Para ello a ejecutar Eclipse desde el directorio en que se ha cargado a seleccionar un espacio de trabajo donde se guardar n los proyectos conjunto de m dulos de una especificaci n implementaciones en C y ficheros de texto que se realicen Si estas utilizando Windows no debes usar un path cuyos directorios tengan blancos seleccionar en el men Help la opci n Install new software En el apartado work with pulsar el bot n Add Seleccionar un nuevo sitio con el nombre que se desee p e MOMENT Public Update Site y direcci n http moment dsic upv es updates Seleccionar MDT e instalarlo Este proceso est explicado en detalle en el manual de instalaci n desarrollado por el proyecto MO MENT aunque la explicaci n anterior deber a ser suficiente para la mayor parte de los sistemas P gina http moment dsic upv es seleccionar Maude development tools seguir el hiperlink I
15. nfoCenter se leccionar Maude Development Tools seleccionar Installation Process A continuaci n se debe seleccionar el entorno de ejecuci n para Maude En el men Window de Eclipse seleccionar Show View a continuaci n en Other seleccionar Maude y a continuaci n Maude Console La ventana de Eclipse se encuentra ahora dividida en varias partes Si no lo est cerrar la consola que se acaba de abrir y aparecer Las siguientes veces que se abra Eclipse bastar con teclear en la ventana de bienvenida y ya se cargar n las ventanas Las ventanas que se van a utilizar son e Una ventana denominada Project Explorer En esta ventana se muestran los proyectos exis tentes en el espacio de trabajo seleccionado al abrir Eclipse y los archivos de cada proyecto e El editor donde se escribe el contenido de los m dulos e La consola de Maude con los botones para ejecutar y detener el programa Si se ha mini mizado volver a abrirla desde Show View Other Maude y colocarla debajo de la ventana del Editor Tambien se podr abrir la consola cuando se cree un fichero maude utilizando un bot n de la barra de herramientas e La consola de C El resto de las ventanas pueden minimizarse Para poder ejecutar Maude hay que indicar al sistema donde se encuentra el ejecutable Para ello seleccionar en el men Window de Eclipse la opci n Preferences y aqu la l nea Maude Preferences e Buscar el path en el que se encuentra el ejecutable d
16. o de Maude Pulsar Finish En el fichero Complejos escribid la especificaci n utilizando el editor situado en la ventana central fmod COMPLEJOS is including INT sort Complejo op C Int Int gt Complejo ctor op suma Complejo Complejo gt Complejo op resta Complejo Complejo gt Complejo vars A1 A2 A3 A4 Int eq suma suma C A1 A2 C A3 A4 C A1 A3 A2 A4 eq resta resta C A1 A2 C A3 A44 C A1 A3 A2 A4 endfm Al escribir la especificaci n hay que tener cuidado con los espacios en blanco los puntos y las may sculas y min sculas ya que en Maude tienen significado Con esta especificaci n los n meros complejos se representan con la constructora C Las operaciones de suma y resta se denominan suma y resta respectivamente Este curso no se utilizar n operaciones con notaci n infija debido a las restricciones de la herramienta de testing Salvad la especificaci n al terminar de escribirla utilizando el men File de Eclipse o el icono de la barra de herramientas Ejecutad Maude pulsando en el bot n de la consola Vereis que os sale un mensaje Welcome to Maude en la consola y que aparece una l nea de comandos Ahora hay que cargar el m dulo que hemos escrito en el sistema Para ello se puede utilizar la opci n Maude del men con Send to Maude o bien el bot n de la la barra de herramientas Lo que se env a al sistema Maude con esta opci n es lo que se encuentra en la ventan
Download Pdf Manuals
Related Search