A Language-Independent Proof System for ...
Type de document :
Communication dans un congrès avec actes
Titre :
A Language-Independent Proof System for Mutual Program Equivalence
Auteur(s) :
Ciobâcǎ, Ştefan [Auteur]
Lucanu, Dorel [Auteur]
Department of Computer Science [Lasi]
Rusu, Vlad [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Rosu, Grigore [Auteur]
Lucanu, Dorel [Auteur]
Department of Computer Science [Lasi]
Rusu, Vlad [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Rosu, Grigore [Auteur]
Titre de la manifestation scientifique :
ICFEM'14 - 16th International Conference on Formal Engineering Methods
Ville :
Luxembourg-Ville
Pays :
Luxembourg
Date de début de la manifestation scientifique :
2014-11
Titre de la revue :
LNCS (to appear)
Éditeur :
Springer
Date de publication :
2014-11
Discipline(s) HAL :
Informatique [cs]/Systèmes embarqués
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 ...
Lire la suite >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.Lire moins >
Lire la suite >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.Lire moins >
Résumé en anglais : [en]
Two programs are mutually equivalent if they both diverge or they end up in similar states. Mutual equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many ...
Lire la suite >Two programs are mutually equivalent if they both diverge or they end up in similar states. 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 parametric 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.Lire moins >
Lire la suite >Two programs are mutually equivalent if they both diverge or they end up in similar states. 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 parametric 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.Lire moins >
Langue :
Anglais
Comité de lecture :
Oui
Audience :
Internationale
Vulgarisation :
Non
Collections :
Source :
Fichiers
- https://hal.inria.fr/hal-01030754/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-01030754/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-01030754/document
- Accès libre
- Accéder au document
- document
- Accès libre
- Accéder au document
- submission.pdf
- Accès libre
- Accéder au document