Modular Formal Islands: Embed theory in your practice

Emilie Balland 1 Claude Kirchner 1 Pierre-Etienne Moreau 1 Anderson Santana de Oliveira 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 modularity, pattern matching or strategic rewriting, we have introduced in previous works the Formal Islands framework. The main idea consists in integrating, 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. We present this generic framework and we show that language extensions like Mhtml—providing modular constructions for html— or Tom—a Java language extension allowing for pattern matching and rewriting—are indeed Islands and can therefore be used to embed formal software developments into legacy code.
Type de document :
Communication dans un congrès
Third Taiwanese-French Conference on Information Technology - TFIT 2006, Mar 2006, Nancy/France, 2006
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00001186
Contributeur : Anderson Santana de Oliveira <>
Soumis le : vendredi 31 mars 2006 - 12:15:35
Dernière modification le : mardi 25 octobre 2016 - 16:57:15
Document(s) archivé(s) le : lundi 17 septembre 2012 - 13:15:39

Fichier

Identifiants

  • HAL Id : inria-00001186, version 1

Collections

Citation

Emilie Balland, Claude Kirchner, Pierre-Etienne Moreau, Anderson Santana de Oliveira. Modular Formal Islands: Embed theory in your practice. Third Taiwanese-French Conference on Information Technology - TFIT 2006, Mar 2006, Nancy/France, 2006. 〈inria-00001186〉

Partager

Métriques

Consultations de la notice

204

Téléchargements de fichiers

115