Herramientas

• Maude. El sistema Maude está basado en lógica ecuacional y de reescritura, y tiene acreditada una extensa gama de aplicaciones.
  Desde el comienzo del programa, el sistema Maude ha sido actualizado en dos ocasiones, en junio de 2010 y en enero de 2011, siendo la versión actual la número 2.6. Para cada una de estas versiones, hemos actualizado el manual del sistema con las nuevas características de la herramienta; mientras que en la versión 2.5 las modificaciones tuvieron que ver fundamentalmente con la corrección de bugs, optimizaciones y notación sintáctica, la 2.6 continúa con la implementación de métodos de unificación, estrechamiento y alcanzabilidad simbólica.
• Ciao. El sistema Ciao es un potente entorno multiparadigma que extiende ISO-Prolog en numerosas direcciones e incluye un sofisticado sistema de depuración y verificación estática y dinámica de propiedades funcionales y no funcionales (CiaoPP).
  Durante la primera fase del programa se ha avanzado en la implementación de la variante ImProlog, que tiene la potencia suficiente para poder escribir una máquina virtual completa de Prolog y compilarla a C/código máquina, produciendo un resultado idéntico al realizado con una codificación manual. Asimismo se ha trabajado en la adición de características de orientación a objetos a ImProlog. Por otro lado, se ha trabajado en añadir a Ciao la capacidad de ejecución tabulada (que, aunque robusta, no está todavía disponible en la distribución general) y se ha enriquecido notablemente el lenguaje de definición de recursos y los análisis relacionados.
• McErlang. El sistema McErlang es un comprobador de modelos para verificación de programas Erlang.
  Para facilitar la adopción de McErlang y su integración dentro de metodologías de validación y testing, en esta primera fase del programa hemos integrado dentro de McErlang la herramienta de testing comercial QuickCheck de Quviq. McErlang aún debe ser descargado por separado de QuickCheck, pero una vez que la herramienta se descarga, el uso de McErlang para comprobar máquinas de estados secuenciales y paralelas de QuickCheck es sencillo.
• COSTA. El sistema COSTA es un prototipo, de éxito en ámbitos investigadores, que realiza automáticamente análisis de consumo de recursos y terminación de programas de código de bytes de Java.
  
• CRISP. El sistema CRISP, desarrollado originalmente en un proyecto Eureka/ITEA, es un entorno abierto y extensible para la definición y comprobación automática de reglas de programación, una metodología de extendido uso por las empresas.
  El trabajo realizado en estos primeros meses se ha centrado en la extensión de CRISP con los mecanismos para usar análisis estáticos ya existentes (ej. de alias de punteros) en la definición y comprobación de reglas de codificación más complejas. Asimismo, se ha decidido basar los próximos prototipos en la infraestructura de compilación con licencia libre LLVM/clang, Esto facilitará mucho el uso de análisis ya existentes en LLVM, como son varias implementaciones de análisis de alias de punteros.
• TOY. TOY es un sistema de programación multiparadigma fundamentado en el marco lógico CRWL.
  Durante esta primera fase, se ha iniciado la reconstrucción integral del sistema: en concreto, se ha trabajado en el núcleo del sistema, incluyendo el análisis sintáctico, inferencia de tipos de acuerdo a las recientes propuestas desarrolladas, compilación a Prolog multiplataforma y gestión del sistema de módulos.
• Sloth. El sistema Sloth es una implementación del lenguaje lógico funcional Curry. Su núcleo es un compilador de Curry a Prolog construido sobre Ciao, lo que permite aprovechar características subyacentes de Ciao (restricciones, concurrencia, ...) para investigar diferentes extensiones de Curry.
  En esta primera fase del programa hemos desarrollado una nueva versión de Sloth que incluye extensiones al estándar del lenguaje Curry tales como polimorfismo ad-hoc} mediante clases de tipos y de constructores de tipos ("type and constructor classes") así comosinónimos ("alias") de tipos.
• DES. DES es un sistema de bases de datos deductivas interactivo, multiplataforma y portable.
  En esta primera fase del programa se han lanzado sucesivas versiones del sistema con nuevas funcionalidades: en concreto, restricciones fuertes de integridad y acceso desde instrucciones SQL a relaciones Datalog mediante restricciones de tipos; acceso a sistemas gestores de bases de datos relacionales vía ODBC; trazadores para Datalog y SQL; e integración con el entorno gráfico ACIDE.
• EOS. EOS es un componente Java que implementa la evaluación de OCL2.0 sobre escenarios de modelos, dando soporte a diferentes usos de OCL, como validación, análisis, auditoría o medida de modelos.
  Además de extender la clase de expresiones OCL que soporta EOS, en esta primera fase del programa hemos integrado EOS en SSG, una herramienta para el desarrollo, a partir de modelos, de aplicaciones seguras para la gestión de información. En concreto, dentro de SSG, EOS se utiliza para el análisis sintáctico de las expresiones OCL que aparecen en los modelos (de seguridad y de GUIs) y para comprobar, además, la conformidad de los modelos (de datos, de seguridad y de GUIs) con respecto a sus metamodelos, evaluando para ello las correspondientes invariantes OCL.