A Language-Independent Proof System for Full Program Equivalence

Stefan Ciobaca 1 Dorel Lucanu 1 Vlad Rusu 2 Grigore Rosu 3
2 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
Abstract : Two programs are mutually equivalent if, for the same input, either they both diverge or they both terminate with the same result. Mutual equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for mutual equivalence, which is para-metric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: if it terminates then it establishes the mutual equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known wether the sequence terminates or not; nevertheless, our proof system shows that the two programs are mutually equivalent (even if we cannot establish termination or divergence of either one).
Type de document :
Article dans une revue
Formal Aspects of Computing, Springer Verlag, 2016, 28 (3), pp.469--497. 〈10.1007/s00165-016-0361-7〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01245528
Contributeur : Pal Dream <>
Soumis le : lundi 25 janvier 2016 - 15:35:11
Dernière modification le : mercredi 25 avril 2018 - 15:42:33

Fichier

icfem-postproceedings-final-ve...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu. A Language-Independent Proof System for Full Program Equivalence. Formal Aspects of Computing, Springer Verlag, 2016, 28 (3), pp.469--497. 〈10.1007/s00165-016-0361-7〉. 〈hal-01245528v2〉

Partager

Métriques

Consultations de la notice

182

Téléchargements de fichiers

111