ELAN ou la programmation par 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 notion de réécriture est omniprésente en informatique, en logique ou en mathématiques. Elle peut être utilisée aussi bien pour déduire -on parle alors souvent de règle d'inférence- ou pour calculer -et on suppose souvent dans ce cas que la relation sous-jacente est noetherienne et confluente-. Il est en fait fondamental de pouvoir décrire non-seulement les étapes élémentaires de réécriture, c'est à dire les règles de réécriture, mais aussi comment elles sont enchainées. Il faut alors introduire le concept de stratégie qui doit permettre d'exprimer des calculs déterministes mais aussi, et c'est plus original, la recherche de bonnes dérivations. Cette présentation montrera dans un premier temps comment le langage ELAN donne la possibilité d'exprimer de façon uniforme règles de réécriture et stratégies et comment le compilateur ELAN permet de les exécuter très efficacement. Nous montrerons sur un exemple de protocole comment le langage nous permet d'écrire puis de prototyper des spécifications éventuellement non déterministes et comment la notion de stratégie permet leur vérification directe. Dans une seconde partie, nous introduirons le calcul de réécriture et nous montrerons comment il permet de donner une sémantique aux langages basés sur la réécriture. ELAN, sa documentation et des exemples d'utilisation sont disponibles à l'addresse www.loria.fr/ELAN.
Type de document :
Communication dans un congrès
FAC 2000, May 2000, Toulouse, France, 96 p, 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00107865
Contributeur : Publications Loria <>
Soumis le : jeudi 19 octobre 2006 - 09:12:09
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57
Document(s) archivé(s) le : mercredi 29 mars 2017 - 13:03:48

Identifiants

  • HAL Id : inria-00107865, version 1

Collections

Citation

Claude Kirchner. ELAN ou la programmation par réécriture. FAC 2000, May 2000, Toulouse, France, 96 p, 2000. 〈inria-00107865〉

Partager

Métriques

Consultations de la notice

125

Téléchargements de fichiers

27