Program Equivalence by Circular Reasoning

Dorel Lucanu 1 Vlad Rusu 2
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 : We propose a logic and a deductive system for stating and automatically proving the equivalence of programs written in languages having a rewriting-based operational semantics. The chosen equivalence is parametric in a so-called observation relation, and it says that two programs satisfying the observation relation will inevitably be, in the future, in the observation relation again. This notion of equivalence generalises several well-known equivalences and is appropriate for deterministic (or, at least, for confluent) programs. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the given program-equivalence problem. We show that our approach is suitable for proving equivalence for terminating and non-terminating programs as well as for concrete and symbolic programs. The latter are programs in which some statements or expressions are symbolic variables. By proving the equivalence between symbolic programs, one proves the equivalence of (infinitely) many concrete programs obtained by replacing the variables by concrete statements or expressions. The approach is illustrated by proving program equivalence in two languages from different programming paradigms. The examples in the paper, as well as other examples, can be checked using an online tool.
Type de document :
Article dans une revue
Formal Aspects of Computing, Springer Verlag, 2015, 27 (4), pp.701-726. 〈10.1007/s00165-014-0319-6〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01065830
Contributeur : Mister Dart <>
Soumis le : jeudi 18 septembre 2014 - 15:46:28
Dernière modification le : mardi 3 juillet 2018 - 11:32:44
Document(s) archivé(s) le : vendredi 19 décembre 2014 - 14:00:16

Fichier

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

Identifiants

Collections

Citation

Dorel Lucanu, Vlad Rusu. Program Equivalence by Circular Reasoning. Formal Aspects of Computing, Springer Verlag, 2015, 27 (4), pp.701-726. 〈10.1007/s00165-014-0319-6〉. 〈hal-01065830〉

Partager

Métriques

Consultations de la notice

456

Téléchargements de fichiers

167