A Language-Independent Proof System for Mutual Program Equivalence

Résumé : Deux programmes sont en équivalence mutuelle s'ils divergent tous les deux ou s'ils terminent dans des états similaires. L'équivalence mutuelle est une notion adéquate d'équivalence pour les programmes déterministes. Elle est utile dans divers contextes, parmi lesquels on peut citer la preuve de transformations de programmes dans un langage donné, et la preuve de compilateurs entre deux langages. Dans cet article nous introduisons un système déductif pour l'équivalence mutuelle, qui a comme paramètres les sémantiques opérationnelles de deux langages ainsi qu'une relation de similitude entre états des programmes. Le système déductif est correct: lorsqu'il termine, il démontre l'équivalence des programmes qui lui sont donnés en entrée. Nous l'illustrons sur deux programmes, appartenant à des langages différents : l'un impératif, l'autre fonctionnel, qui calculent la séquence de Collatz de deux manières différentes.
Type de document :
Communication dans un congrès
ICFEM'14 - 16th International Conference on Formal Engineering Methods, Nov 2014, Luxembourg-Ville, Luxembourg. Springer, 2014, LNCS (to appear)
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01030754
Contributeur : Mister Dart <>
Soumis le : mardi 22 juillet 2014 - 13:37:44
Dernière modification le : jeudi 11 janvier 2018 - 06:25:37
Document(s) archivé(s) le : mardi 25 novembre 2014 - 11:05:14

Fichier

submission.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01030754, version 1

Collections

Citation

Ştefan Ciobâcǎ, Dorel Lucanu, Vlad Rusu, Grigore Rosu. A Language-Independent Proof System for Mutual Program Equivalence. ICFEM'14 - 16th International Conference on Formal Engineering Methods, Nov 2014, Luxembourg-Ville, Luxembourg. Springer, 2014, LNCS (to appear). 〈hal-01030754〉

Partager

Métriques

Consultations de la notice

325

Téléchargements de fichiers

99