Program Equivalence by Circular Reasoning

Dorel Lucanu 1 Vlad Rusu 2
2 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Université de Lille, Sciences et Technologies, Inria Lille - Nord Europe, CNRS - Centre National de la Recherche Scientifique
Résumé : Nous proposons une logique et un système déductif pour exprimer et prouver automatiquement l'équivalence de programmes dans des langages déterministes munis de sé- mantiques opérationnelles définies par réécriture. Le système déductif proposé est de nature circulaire; nous démontrons qu'il est correct et faiblement complet. Ces deux résultats sig- nifient que, lorsqu'il termine, notre système résout correctement le problème d'équivalence de programmes tels que nous l'avons posé. Nous montrons que ce système fonctionne autant pour des programmes qui terminent que pour des programmes qui ne terminent pas. Les programmes dits symboliques, dans lesquels certaines expressions ou instructions restent non-interprétés, peu- vent également être traités par notre approche. La démonstration d'une équivalence entre deux programmes symboliques revient à démontrer l'équivalence entre une infinité potentielle de pro- grammes concrets, qui sont des instances des programmes symboliques obtenues en remplaçant les variables symboliques par des instructions ou des expressions concrètes. L'approche est illustrée par la preuve d'équivalence de programmes dans deux langages appartenant à des paradigmes de programmation différents. Les exemples contenus dans l'article, ainsi que d'autres exemples, peuvent être essayés dans un outil en ligne.
Type de document :
Rapport
[Research Report] RR-8116, INRIA. 2013, pp.33
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00744374
Contributeur : Mister Dart <>
Soumis le : dimanche 8 décembre 2013 - 20:32:33
Dernière modification le : jeudi 11 janvier 2018 - 06:25:37
Document(s) archivé(s) le : samedi 8 avril 2017 - 05:27:05

Fichier

ifm-facs-techreport.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00744374, version 4

Citation

Dorel Lucanu, Vlad Rusu. Program Equivalence by Circular Reasoning. [Research Report] RR-8116, INRIA. 2013, pp.33. 〈hal-00744374v4〉

Partager

Métriques

Consultations de la notice

455

Téléchargements de fichiers

179