Formal Islands

Emilie Balland 1 Claude Kirchner 1 Pierre-Etienne Moreau 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Motivated by the proliferation and usefulness of Domain Specific Languages as well as the demand in enriching well established languages by high level capabilities like pattern matching or strategic rewriting, we introduce the \emph{Formal Islands} framework. The main idea consists to integrate, in existing programs, formally defined parts called Islands, on which proofs and tests can be meaningfully developed. Then, Formal Islands could be safely dissolved into their hosting language to be transparently integrated in the existing user environment. The paper presents this generic framework and shows that the properties valid on the formal islands are also valid on the corresponding dissolved host codes. Formal Islands can be used as a general methodology to develop new DSL and we show that language extensions like sqlj ---embedding sql capabilities in Java ---, or Tom ---a Java language extension allowing for pattern matching and rewriting---are indeed Islands and they can therefore be used for formal software developments.
Type de document :
Communication dans un congrès
Michael Johnson and Varmo Vene. 11th International Conference on Algebraic Methodology and Software Technology - AMAST '06, Jul 2006, Kuressaare, Estonia. Springer, 4019, pp.51-65, 2006, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00001146
Contributeur : Emilie Balland <>
Soumis le : mercredi 8 mars 2006 - 17:18:10
Dernière modification le : mardi 25 octobre 2016 - 16:58:17
Document(s) archivé(s) le : lundi 17 septembre 2012 - 12:26:37

Identifiants

  • HAL Id : inria-00001146, version 1

Collections

Citation

Emilie Balland, Claude Kirchner, Pierre-Etienne Moreau. Formal Islands. Michael Johnson and Varmo Vene. 11th International Conference on Algebraic Methodology and Software Technology - AMAST '06, Jul 2006, Kuressaare, Estonia. Springer, 4019, pp.51-65, 2006, Lecture Notes in Computer Science. 〈inria-00001146〉

Partager

Métriques

Consultations de la notice

246

Téléchargements de fichiers

194