Une Approche Formelle de L'Interop Rabilit Pour Une Famille de DSL

Dans ce Livre, nous proposons une m thode rigoureuse, formellement fond e pour traiter de l'interop rabilit d'une famille de langages d di?‘s (DSL) issus d'un m me domaine m tier. A partir de la s mantique de chacun des DSL, notre d marche construit, par un calcul de co-limite sur des sp cifications alg briques, un langage qui unifie les concepts de la famille. L'approche se caract rise notamment par la capacit traduire automatiquement le code d'un DSL vers le langage unificateur. Un autre b n fice r side dans la preuve qu'une propri t sur un langage de la famille se d cline, par construction, vers l'environnement unifi . La mise en uvre de la d marche a t outill e; elle s'appuie principalement sur le logiciel Specware de Kestrel et l'assistant de preuve Isabelle.