Support |
|
|
|
TOOLS
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 (http://maude.sip.ucm.es/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 (http://maude.sip.ucm.es/mova/): Herramienta de modelado y
verificación en UML con restricciones OCL.
- TOY (http://toy.sourceforge.net): 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 (http://gpd.sip.ucm.es/jaime/oops/oops.tar.gz): 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 (http://des.sourceforge.net): 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 (http://gpd.sip.ucm.es/rafa/systems/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.
La versión actual de la herramienta (0.3.1) se puede descargar en:
http://babel.ls.fi.upm.es/software/slam
- Sloth (http://babel.ls.fi.upm.es/research/Sloth):
Sloth es la implementación realizada por el grupo Babel del lenguaje
lógico-funcional Curry. Se distribuye bajo licencia GPL.
- McErlang (http://babel.ls.fi.upm.es/~fred/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 (http://babel.ls.fi.upm.es/software/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 (https://babel.ls.fi.upm.es/research/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 (http://www.clip.dia.fi.upm.es/Software/Ciao/): 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 Prolog.
- Fuzzy-Prolog (http://www.clip.dia.fi.upm.es/Software/Ciao/):
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 d
de la liga RoboCup.
- 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. El cuestionario puede encontrarse en:
https://babel.ls.fi.upm.es/services/ggcc_questionnaire
- CiaoJVM: Implementación de una especificación formal de la
máquina abstracta de Java en programación lógica (en Ciao,
http://www.clip.dia.fi.upm.es/Software/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 (http://www.clip.dia.fi.upm.es/Software/Ciao/).
- LProlog: implementación de un traductor de Lambda Prolog a Ciao
(http://www.clip.dia.fi.upm.es/Software/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. (http://www.clip.dia.fi.upm.es/Software/Ciao/).
- 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 (http://www.clip.dia.fi.upm.es/Software/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 (http://www.clip.dia.fi.upm.es/Software/Ciao/): 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.
- 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 (http://www.clip.dia.fi.upm.es/Software/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
(http://www.clip.dia.fi.upm.es/Software/Ciao/).
- Entorno integrado en el sistema Ciao (http://www.clip.dia.fi.upm.es/Software/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 (http://www.clip.dia.fi.upm.es/Software/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.
- Librería de encaje de patrones de texto utilizando expresiones
regulares.
- Prototipo de librería de ejecución de Ciao (http://www.clip.dia.fi.upm.es/Software/Ciao/) con
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 (http://www.clip.dia.fi.upm.es/Software/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
(http://www.clip.dia.fi.upm.es/Software/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 (http://www.clip.dia.fi.upm.es/Software/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 (http://www.clip.dia.fi.upm.es/Software/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 (http://www.clip.dia.fi.upm.es/Software/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 (http://www.clip.dia.fi.upm.es/Software/Ciao/), que ha visto incrementada su robustez.
|