On the implementation of construction functions for non-free concrete data types

Frédéric Blanqui 1 Thérèse Hardin 2 Pierre Weis 3
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 SPI - Sémantiques, preuves et implantation
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : Many algorithms use concrete data types with some additional invariants. The set of values satisfying the invariants is often a set of representatives for the equivalence classes of some equational theory. For instance, a sorted list is a particular representative wrt commutativity. Theories like associativity, neutral element, idempotence, etc. are also very common. Now, when one wants to combine various invariants, it may be difficult to find the suitable representatives and to efficiently implement the invariants. The preservation of invariants throughout the whole program is even more difficult and error prone. Classically, the programmer solves this problem using a combination of two techniques: the definition of appropriate construction functions for the representatives and the consistent usage of these functions ensured via compiler verifications. The common way of ensuring consistency is to use an abstract data type for the representatives; unfortunately, pattern matching on representatives is lost. A more appealing alternative is to define a concrete data type with private constructors so that both compiler verification and pattern matching on representatives are granted. In this paper, we detail the notion of private data type and study the existence of construction functions. We also describe a prototype, called Moca, that addresses the entire problem of...
Type de document :
Communication dans un congrès
16th European Symposium on Programming - ESOP'07, Mar 2007, Braga, Portugal. Springer, 4421, pp.95-109, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-71316-6_8〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00095110
Contributeur : Frédéric Blanqui <>
Soumis le : vendredi 5 janvier 2007 - 17:49:07
Dernière modification le : lundi 29 mai 2017 - 14:25:06
Document(s) archivé(s) le : lundi 5 avril 2010 - 22:46:36

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Frédéric Blanqui, Thérèse Hardin, Pierre Weis. On the implementation of construction functions for non-free concrete data types. 16th European Symposium on Programming - ESOP'07, Mar 2007, Braga, Portugal. Springer, 4421, pp.95-109, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-71316-6_8〉. 〈inria-00095110〉

Partager

Métriques

Consultations de la notice

302

Téléchargements de fichiers

89