Logiciels développés dans le groupe PROTHEO

Tom

Tom est un outil de compilation du filtrage qui peut être vu comme un préprocesseur capable de compiler des constructions de filtrage. Une de ses particularités est d'être indépendant du langage natif : Tom peut générer des automates de filtrages dans différents langages, dont C, Java et Eiffel.

Une autre caractéristique essentielle est d'être indépendant de la représentation des termes : Tom accède aux termes en utilisant une interface commune permettant de le rendre indépendent de la représentation concrète.

Ces caractéristiques font de Tom un outil idéal pour implanter des systèmes de transformation de termes et plus particulièrement les langages fondés sur la notion de règles de réécriture (ASF+SDF, ELAN et Stratego par exemple).

Tom est documenté, maintenu et disponible sur le Web. Plus d'informations sont disponibles sur la page Gforge du projet Tom et le Tom bug tracker.

ATerm-java et SharedObjects

ATerm-java et SharedObjects sont deux bibliothèques écrites en Java qui permettent de représenter des termes de manière extrêmement efficace, en temps et en mémoire. Reposant sur une technique de partage maximum, la comparaison de deux termes se fait en temps constant. La bibliothèque offre également des facilités d'entrée-sortie.

Ces bibliothèques sont incluses dans la distribution de Tom.

Gom

Gom est un générateur de structures de données typées. Reposant sur ATerm-java et SharedObjects, le code généré est efficace et repose sur le principe de partage maximal. Gom permet de définir des fonctions de normalisation permettant de maintenir les données en forme normale. Un support particulier est offert pour obtenir des formes canoniques modulo les théories associatives, commutatives, avec élément neutre.

L'outil Gom s'interface facilement avec Tom. Il est inclus dans la distribution de Tom.

CoLoR

CoLor est une librairie Coq dont le but est de fournir les bases formelles nécessaires à la certification de candidats de preuve de terminaison trouvés et construits par des outils tels que CiME, AProVE, TTT, CARIBOO, etc. Elle inclut entre autres une bibliothèque sur les vecteurs, une bibliothèque sur les polynômes à coefficients entiers et variables multiples, une bibliothèque sur les termes algébriques avec symboles à arité fixe, une preuve du critère de terminaison basé sur les interprétations polynomiales, et une preuve du théorème des paires de dépendances. La librairie est promise à évoluer et inclure plus de développements rapidement. Pour des informations plus récentes, voir la page web de CoLoR.

Rainbow

Rainbow fournit une grammaire pour les preuves de terminaison et un outil pour automatiquement certifier les preuves exprimées dans cette grammaire en utilisant la bibliothèque CoLoR.

CARIBOO

CARIBOO est un outil de preuve de terminaison pour les langages à base de règles dans lesquels un programma est un système de réécriture et une évaluation consiste à réécrire une expression de départ. Il s'applique à des langages comme ASF+SDF, Maude, Cafe-OBJ ou ELAN.

CARIBOO (pour Computing AbstRaction for Induction Based termination prOOfs), est dédié aux preuves de terminaison sous certaines stratégies de réduction particulières, ce qui devient particulièrement intéressant quand les calculs divergent pour la réécriture standard.

ELAN

ELAN est un environnement de spécification et de prototypage fondé sur l'application de règles de réécriture contrôlée au moyen de stratégies. Il offre un cadre logique simple et naturel pour combiner les paradigmes de calcul et de déduction. Ses originalités principales sont d'implanter des techniques de filtrage et de réduction de termes modulo l'associativité-commutativité, compilées de façon très efficace; le traitement de calculs non-déterministes, i.e. pouvant retourner plusieurs résultats, dont l'énumération est gérée par des stratégies; un langage de stratégies dont les primitives, en particulier les opérateurs de choix, permettent une gestion fine de l'exploration de l'arbre de recherche ; la possibilité donnée à l'utilisateur de définir ses propres stratégies. ELAN est utilisé pour prototyper des démonstrateurs de théorèmes, des langages de programmation, des résolveurs de contraintes et des procédures de décision. Il offre un cadre modulaire pour étudier leur combinaison.

Le système ELAN inclut un interpréteur, un compilateur, une bibliothèque de support d'exécution, un ramasse miettes, une bibliothèque de gestion du backtracking ainsi qu'une bibliothèque de programmes standard, des exemples d'applications et un manuel d'utilisation.

ELAN est documenté, maintenu, diffusé par ftp et accessible sur le Web. Le correspondant au sein du projet est Claude Kirchner.

Autres logiciels