Interfaz web para demostradores de teoremas en MAUDE

Abstract

Este proyecto consiste en hacer una interfaz web para poder trabajar con las herramientas CafeInMaude y CITP, las cuales son demostradores de teoremas; implementados en el lenguaje Maude, de forma más intuitiva. CafeInMaude es una herramienta que permite trabajar con el lenguaje CafeOBJ a través de la cual se pueden demostrar teoremas haciendo uso de la sintaxis de CafeOBJ y herramientas desarrolladas explícitamente para este lenguaje. CITP es una herramienta para demostrar que ciertos sistemas de software cumplen con propiedades específicas, utilizando grafos orientados o sistemas de transiciónes basados en constructoras. Nuestra web permite ejecutar estas dos herramientas (CITP y CafeInMaude); y crear una conexión que posibilite al usuario enviar comandos de forma directa a través de esta, estos comandos se introducirán en Maude y las dos herramientas haciendo uso del módulo pexpect de Python, que permite generar aplicaciones hijo, controlarlas y responder a patrones esperados en su salida. Estos patrones serán los prompts correspondientes a cada una de las herramientas usadas (CafeInMaude y CITP). Una vez se haya encontrado dicho prompt, se capturará la salida previa si es que hubiese y se mostrará el resultado por pantalla para que el usuario pueda visualizarlo.This project consists of making a web interface to be able to work with the tools CafeInMaude and CITP, which are theorem provers; implemented in the Maude language, in a more intuitive way. CafeInMaude is a tool that allows working with the CafeOBJ language through which theorems can be proved using the CafeOBJ syntax and tools developed explicitly for this language. CITP is a tool to demonstrate that certain software systems comply with specific properties, using oriented graphs or transition systems (arrow diagrams that show how things change from one state to another). Our website allows us to run these two tools (CITP and CafeInMaude); and create a connection that allows the user to send commands directly through it, these commands will be introduced in Maude and the two tools using the Python pexpect module, which allows us to generate child applications, control them and respond to expected patterns in their output. These patterns will be the prompts corresponding to each of the tools used (CafeInMaude and CITP). Once this prompt has been found, the previous output, if any, will be captured and the result will be displayed on the screen so that the user can view it.