Programming Language Aggregation with Applications in Equivalence Checking - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

Programming Language Aggregation with Applications in Equivalence Checking

Résumé

We show that, given the operational semantics of two programming languages L and R, it is possible to construct an aggregate language, in which programs consist of pairs of programs from L and respectively R. In the aggregate language, a program P = (PL, PR) takes a step from either PL or PR. The main difficulty is how to aggregate the two languages so that data such as integers or booleans that are common to both languages has the same representation in the aggregate language. The aggregation is based on the pushout theorem, which allows us to construct a model of the aggregate language from models of the initial languages, while making sure that the interpretation of common data such as integers is the same. A main application of the aggregation result is in equivalence checking. It is possible to check for example that two programs PL and PR (written in L and respectively R) compute the same result by checking the partial correctness of the pair (PL,PR) in the aggregate language.
Nous montrons qu'à partir des sémantiques opérationnelles de deux langages de programmation L et R il est possible de construire leur agrégation, qui est un langage dont les programmes sont des paires de programmes de L et de R. Dans ce nouveau langage, les données ou expressions communes à L et R sont factorisés afin d'éviter d'en garder deux copies distinctes. Ceci est rendu possible grâce au théorème de "pushout" qui construit un modèle de l'agrégation à partir de modèles des composantes L et R. Nous appliquons ces résultats à la preuve d'équivalence de programmes.
Fichier principal
Vignette du fichier
pas2014_submission_14_1_.pdf (112.5 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00998930 , version 1 (03-06-2014)

Identifiants

  • HAL Id : hal-00998930 , version 1

Citer

Ştefan Ciobâcǎ, Dorel Lucanu, Vlad Rusu, Grigore Rosu. Programming Language Aggregation with Applications in Equivalence Checking. Third International Seminar on Program Verification, Automated Debugging and Symbolic Computation (PAS 2014), Jul 2014, Vienne, Austria. ⟨hal-00998930⟩
82 Consultations
111 Téléchargements

Partager

Gmail Facebook X LinkedIn More