Tools Developed

The theoretical work in the various research lines has led to different tools which has been developed (or improved) under the programme. All these tools are distributed as free software and can be obtained through the Internet.

• ITP: Inductive theorem prover that can be used to prove properties of membership equational specifications, as well as incompletely specified algorithms on them, as a way to support incremental development of specifications.
• MOVA: Modeling and validation tool for UML with OCL constraints.
• TOY: constraint functional logic system, designed to support the main declarative programming styles and their combination.
• OOPS: System for logical and functional programming, it is the only logical-functional system known with capacity of finite constructive failure. This system also provides the automatic generation of traces, postscripts of computations.
• DES: Educational database system, implemented on Prolog. This is a deductive database, with stratified negation which uses DATALOG as query language. It allows the use of full recursion and memorization techniques.
• JDD: Prototype of a declarative debugger for Java programs. It applies transferred classical formal techniques from declarative programming to object oriented programming. The students who collaborated on its implementation were awarded with the second place in the first edition of the Sun Microsystems Awards.
• SLAM: There are two tools. The one implemented in Java allows you to: a sithesized code (readable and efficient) from specifications, having the possibility to optimize manually the original specifications, visual debugging to validate the specifications, generating code for several object oriented languages (C + +,Java, C #, etc.). The second one, implemented in Haskell, in addition to the above functionality, supports: Analysis of specifications, generation of debugging information and the generation of semi-skeletons in Java.
• Sloth: Sloth is the implementation of a logical-functional Curry language carried out by the Babel group. It is been distributed under GPL license.
• McErlang: It is a model-checking tool for Erlang for validating properties of Erlang distributed programs. This tool has been used for non-trivial applications.
• MTP This tool is a compiler generator. A new version, 0.3.3, has been released which is incorporated in Gentoo Linux official repositories.
• RAM: A prolog compiler with relational constraints for a relational allegories language. It is usable as an experimental tool and supports several kinds of unification, full SLD, various execution systems and improvements in results visualization.
• Negation modules for Prolog: This is a series of Ciao Prolog modules which allow the efficient implementation of negated goals in Prolog.
• Fuzzy-Prolog: A Ciao library implementing an extension of Prolog to deal with uncertainty. This implementation models based interval-valued fuzzy logic. A java interface has also been developed for the use of fuzzy reasoner, with simulators of the RoboCup league (in Ciao).
• Interactive quiz GCC: The GCC consists of an improvement of the GNU GCC compiler that incorporates error detection and bad programming practices at compile time. The technology used leverages progress from the declarative technology project. The main contribution to date is of considerable impact because it enables the development of a proposal of codification rules and their validation through an online questionnaire, that is answered by hundreds of European companies. The questionnaire can be found at:
• CiaoJVM: Implementation of a Java Virtual Machine Specification as a Prolog meta-interpreter, and using it for de-compiling Java bytecode Programs into Prolog using Partial evaluation techniques. The de-compiled code is then used for analysis, optimization and testing of the original bytecode program.
• Two analyzers for run-time properties of Java and Java bytecode programs. Both are based on translating the original code into Prolog, which allow using all the analyses and techniques that have been previously developed for Prolog.
• LProlog: implementation in Ciao of translator form Lambda Prolog to pure Prolog, including higher-order unification, in collaboration with the U. Minesota (Gopalan Nadathur) and U. New Mexico (Amadeo Casas) in E.E.U.U..
• FLazy: Ciao library enabling the use of functional syntax in logic programs and integrating not typed lazy functional programming by translation and use of specific implementation techniques.
• New Ciao implementation of conjunctive parallelism for logic languages: Analyzers, automatic weighting, and implementation mechanisms to use conjunctive parallelism in the execution of logic languages, specially adapted to multicore processors. The implementation is original in the sense that is largely done at the source level, rather than abstract machine, thus simplifying development and maintenance.
• DHT: generic Ciao module to create and access distributed hash tables using an efficient algorithms for routing and key distribution.
• Prediction system for real-time programs through the combined use of a tool for profiling performance (which determines the execution time, instructions and basic constructions) using static analysis techniques to determine the complexity of program fragments (in Ciao).
• Integrated environment in the Ciao system to distribute and check, easyly, certifications of programs properties using abstract interpretation as a basis for tester Abstraction Carrying Code , ACC).
• Design and implementation of a mechanism to insert the automatic code mode checking unverified properties (due to its difficulty) at runtime execution. The violation of these properties produces a warning (with a programmable format) to programmer or system users.
• Multivariate partial evaluator for Ciao programs with Awareness of resources, which seeks the best partial evaluation with respect to consumption of any specific resource using techniques for guided search for functions of costs and genetic drift.(Abstraction Carrying Code, ACC).
• Lace patterns library using regular text expressions regular.
• Prototype of a Ciao library implementing tabulation (that improves the routine strategy performance, passing in some very relevant cases from non-completion to termination of programs), using a modular new method for combination of processing program and portable external code (shared with YAP system, in collaboration with the U. Porto).
• Ciao library to facilitate the writing and implementation of Unit Tests: evidence of a software system that specializes in checking the correctness of usually smallfragments of a program or library. The tests are integral part of the Ciao assertion language.
• Improving the Ciao environment for programming and debugging based on programmable text editor Emacs. Development of specific environments to VIM (in collaboration with the University of New Mexico, USA) and Eclipse. Automatic generation of user menus for the analysis tool CiaoPP.
• ciaocc: prototype of a optimizing compiler, which translates Ciao code to an assembler code via C, using information of types, modes and determinism. Such information may be generated by the analyzing tool and processing programs CiaoPP, or be inserted manually.
• Ciao library implementing the CHR language (Constraint Handling Rules), in collaboration with the University of Leuven. CHR are a high-level language for concurrent logical systems. CHR make it easy to define constraint reasoning: simplification and propagation as well as incremental solving of constraints.
• Automatic systems of generation of user menus for the CiaoPP analysis tool.
• Design and implementation in Ciao of an environment for the incremental analysis of modular programs, necessary to perform in such an efficient mode as to be practical analysis of non-trivial programs.
• Substantial improvements to the automatic documentation generator Ciao Ciao System, which has increased robustness.