ELAN : Modélisation et preuve en calcul de réécriture

Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : La réécriture a été utilisée dès les années 1970 pour modéliser l'égalité. La logique de réécriture proposée par José Meseguer~\cite{Meseguer-92} au tout début des années 1990 a permis de mieux comprendre les aspects logiques de la relation de réécriture. Plus récemment nous avons introduit avec Horatiu Cirstea le calcul de réécriture~\cite{rhoCalIGLP-I+II-2001} qui permet de comprendre la flèche de réécriture comme une abstraction dont l'application explicite à un terme produit un ensemble de résultats. Ce calcul généralise le lambda calcul et offre par son mécanisme de passage de paramètre controlé par filtrage un outil puissant de modélisation et de preuve. {\sf ELAN}~\cite{ELAN-wrla98} (dont l'environnement est disponible à l'addresse \texttt{elan.loria.fr}) est un langage que nous développons à Nancy depuis plusieurs années et qui implante partiellement le calcul de réécriture. Les concepts fondamentaux du langage sont la notion de régle de réécriture et celle de stratégie permettant de décrire finement l'enchainement souhaité des étapes de réécriture. De plus le langage permet de spécifier l'associativité commutativité éventuelle d'opérateurs déclarés par l'utilisateur. Les travaux de Marian Vittek~\cite{Vittek-RTA96} et Pierre-Etienne Moreau~\cite{MoreauK-PLILP+ALP98} ont montré que ce type de langage peut être compilé très efficacement. Sur des exemples purement fonctionels, le compilateur actuellement diffusé permet d'atteindre l'application de quelques 15 millions de réécritures par seconde. Dans cette présentation, le calcul de réécriture sera d'abord introduit avec des exemples simples d'utilisation. Puis nous montrerons comment ce calcul et le système {\sf ELAN} peuvent être utilisés comme outil de modélisation et de preuve en prennant comme exemple nos travaux récents sur les automates temporisés.
Type de document :
Communication dans un congrès
Approches Formelles dans l'Assistance au Développement de Logiciels, 2001, Nancy, France, 2 p, 2001
Liste complète des métadonnées

https://hal.inria.fr/inria-00100560
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:47:37
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00100560, version 1

Collections

Citation

Claude Kirchner. ELAN : Modélisation et preuve en calcul de réécriture. Approches Formelles dans l'Assistance au Développement de Logiciels, 2001, Nancy, France, 2 p, 2001. 〈inria-00100560〉

Partager

Métriques

Consultations de la notice

73