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

8Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.

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 defining concrete data types with invariants: it generates efficient construction functions for the combination of common invariants and builds representatives that belong to a concrete data type with private constructors. © Springer-Verlag Berlin Heidelberg 2007.

References Powered by Scopus

56Citations
6Readers
21Citations
4Readers

Cited by Powered by Scopus

Dependency pairs for rewriting with built-in numbers and semantic data structures

21Citations
1Readers
Get full text

Nonfree datatypes in Isabelle/HOL animating a many-sorted metatheory

10Citations
4Readers
Get full text

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Cite

CITATION STYLE

APA

Blanqui, F., Hardin, T., & Weis, P. (2007). On the implementation of construction functions for non-free concrete data types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4421 LNCS, pp. 95–109). Springer Verlag. https://doi.org/10.1007/978-3-540-71316-6_8

Readers over time

‘10‘11‘12‘14‘15‘1700.511.52

Readers' Seniority

Tooltip

Researcher 3

50%

PhD / Post grad / Masters / Doc 2

33%

Professor / Associate Prof. 1

17%

Readers' Discipline

Tooltip

Computer Science 7

100%

Save time finding and organizing research with Mendeley

Sign up for free
0