Herramientas desarrolladas

El trabajo teórico de las diferentes líneas de investigación ha tenido su reflejo en una serie de herramientas que se han desarrollado (o mejorado) en el seno del Programa; todas ellas se distribuyen como software libre y se pueden obtener a través de Internet.

• ITP: Demostrador inductivo de teoremas para la lógica de pertenencia. Se han añadido nuevos procedimientos de decisión y ahora se ofrece también como herramienta web.
• MOVA: Herramienta de modelado y verificación en UML con restricciones OCL.
• TOY: Sistema de programación lógico-funcional. La última versión (julio 2006) incluye como mejoras: un depurador declarativo (herramienta DDT); ejecución optimizada: incorporación de corte dinámico; combinación de resolutores de restricciones: CFLP(H+R+FD).
• OOPS: Sistema de programación lógico-funcional; único sistema lógico-funcional conocido con capacidad de fallo finito constructivo. Además, proporciona la generación automática de traza postscript de los cómputos.
• DES: Sistema educacional de bases de datos, implementado sobre Prolog. Se trata de de una base de datos deductiva con negación estratificada que utiliza Datalog como lenguaje de consulta. Permite el uso de recursión completa y técnicas de memoization.
• JDD: Prototipo de depurador declarativo de programas Java. Transfiere técnicas formales clásicas de la programación declarativa a programación orientada a objetos. Los alumnos que han colaborado en su implementación fueron galardonados con el segundo premio de la primera edición de los Premios Sun Microsystems.
• SLAM: Existen dos herramientas. La implementada en Java permite: Sintetización de código (legible y eficiente) a partir de especificaciones, con la posibilidad de poder optimizar a mano las especificaciones originales, depuración visual para validar las especificaciones, generación de código para diversos lenguajes orientados a objetos (C++, Java, C#, etc.). La implementada en Haskell incluye, además de la funcionalidad anterior: Análisis de especificaciones, generación de información de depuración y desarrollo a partir de ese análisis y generación de semi-esqueletos en Java.
• Sloth: Sloth es la implementación realizada por el grupo Babel del lenguaje lógico-funcional Curry. Se distribuye bajo licencia GPL.
• McErlang: Se trata de una herramienta de model-checking para Erlang que permite validar propiedades de los programas Erlang distribuidos. La herramienta se ha usado en aplicaciones reales no triviales.
• MTP Se trata de una herramienta generadora de compilador de compiladores. Se ha liberado una nueva versión, la 0.3.3, que está incorporada a repositorios oficiales de Gentoo Linux.
• RAM: Compilador de Prolog con restricciones relacionales a un lenguaje relacional basado en alegorías. Es usable como herramienta experimental y soporta varios tipos de unificación, SLD completo, varios sistemas de ejecución y mejoras en la visualización de resultados.
• Módulos de negación para Prolog: Se trata de una serie de módulos Prolog que permiten la ejecución eficiente de objetivos negados en Prolog. Todas ellas se encuentran disponibles para el compilador Ciao.
• Fuzzy-Prolog: Lenguaje que permite desarrollar programas lógicos que representen el conocimiento difuso de forma continua y discreta. Se distribuye como extensión del compilador Ciao Prolog. Además se ha desarrollado un interfaz java para la utilización del razonador fuzzy con simuladores de la liga RoboCup. (c.f. Ciao.)
• Cuestionario interactivo GCC: El proyecto GCC consiste en la mejora del compilador GNU GCC para incorporar detección de errores y malas prácticas en tiempo de compilación. La tecnología utilizada proviene de avances del proyecto en tecnología declarativa. La principal aportación hasta la fecha tiene una considerable importancia pues implica el desarrollo de una propuesta de reglas de codificación y su validación por medio de un cuestionario on-line que está siendo contestado por cientos de empresas europeas.
• CiaoJVM: Implementación de una especificación formal de la máquina abstracta de Java en programación lógica (en Ciao).
• Dos analizadores de propiedades de programas Java y código de byte de Java mediante su traducción a código Prolog y posterior análisis del mismo, heredando así todas las capacidades desarrolladas para lenguajes lógicos y de restricciones. La traducción se realiza en un caso directamente y en el otro por evaluación parcial del intérprete CiaoJVM respecto al código de byte. (c.f. Ciao).
• LProlog: implementación de un traductor de Lambda Prolog a Ciao, incluyendo unificación de orden superior, realizado en colaboración con las U. de Minnesota (Gopalan Nadathur) y Nuevo México (Amadeo Casas) en E.E.U.U.
• FLazy: librería para permitir el uso de sintaxis funcional en la escritura de programas lógicos e integración de programación funcional perezosa no fuertemente tipada en Ciao mediante una traducción y uso de técnicas específicas de implementación.
• Nueva implementación de paralelismo conjuntivo en lenguajes lógicos: analizadores, anotadores automáticos y mecanismos de ejecución para utilizar paralelismo conjuntivo en la ejecución de lenguajes lógicos, especialmente adaptado a procesadores multicore. La implementación es novedosa en el sentido de que se hace en gran parte a nivel fuente, en lugar de en la máquina abstracta, simplificando así su desarrollo y mantenimiento (en Ciao).
• DHT: módulo genérico de creación y acceso a tablas hash distribuidas, utilizando un algoritmo eficiente de enrutamiento y distribución de claves (en Ciao).
• Sistema de predicción del tiempo real de ejecución de programas mediante el uso combinado de una herramienta de perfilado de la ejecución (que averigua el tiempo de ejecución instrucciones y construcciones básicas) con la utilización de técnicas de análisis estático para averiguar la complejidad de fragmentos de programa.
• Entorno integrado en el sistema Ciao para distribuir y comprobar de modo sencillo certificaciones de propiedades de programas utilizando interpretación abstracta como base del probador (Abstraction Carrying Code, ACC).
• Diseño e implementación de un mecanismo para insertar de modo automático código de comprobación de propiedades no verificadas (debido a su dificultad) en tiempo de ejecución. La violación de dichas propiedades da lugar a un aviso (con formato programable) al programador o usuarios del sistema.
• Evaluador parcial multivariante de programas Ciao con consciencia de los recursos, que intenta buscar la mejor evaluación parcial con respecto al consumo de algún tipo de recurso específico utilizando técnicas de búsqueda guiada por funciones de coste y con deriva genética. (Abstraction Carrying Code,ACC).
• Librería de encaje de patrones de texto utilizando expresiones regulares.
• Prototipo de librería de ejecución de Ciaocon tabulación (que mejora la estrategia habitual de ejecución, pasando en algunos casos muy relevantes de la no terminación a la terminación de programas), utilizando un método novedoso modular por una combinación de transformación de programa y código externo portátil (compartido con el sistema YAP, en colaboración con la U. de Porto).
• Librería de Ciao para facilitar la escritura y ejecución de Unit Tests: pruebas de un sistema software que se especializan en la comprobación de la corrección de fragmentos habitualmente pequeños de un programa o librería. Los tests son parte integral del lenguaje de aserciones de Ciao.
• Mejora del entorno de programación y depuración para Ciao basado en el editor programable de texto Emacs. Desarrollo de entornos específicos para VIM(en colaboración con la U. de Nuevo México, E.E.U.U.) y eclipse. Sistema automático de generación de menús de usuario para la herramienta de análisis CiaoPP.
• ciaocc : prototipo de un compilador de Ciao optimizante, que traduce código Ciao a ensamblador via C, utilizando información de tipos, modos y determinismo. Dicha información puede ser generada por la herramienta de análisis y transformación de programas CiaoPP, o ser insertada manualmente.
• Inclusión en Ciao de un compilador y sistema de tiempo de ejecución para el lenguaje CHR (Constraint Handling Rules), en colaboración con la U. de Lovaina. CHR permite expresar fácilmente a alto nivel resolutores de sistemas de restricciones o usarse para programar como un lenguaje de programación de propósito general.
• Sistema automático de generación de menús de usuario para la herramienta de análisis CiaoPP.
• Diseño e implementación en Ciao de un entorno para el análisis incremental modular de programas, necesario para realizar de modo suficientemente eficiente como para ser práctico análisis no triviales de programas.
• Mejoras substanciales al generador automático de documentación del sistema Ciao, que ha visto incrementada su robustez.