On the Implementation of Construction Functions for Non-free Concrete Data Types

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 dicult to nd the suitable representatives and to eciently implement the invariants. The preservation of invariants throughout the whole program is even more dicult and error prone. Classically, the programmer solves this problem using a combination of two techniques: the denition of appropriate construction functions for the representatives and the consistent usage of these functions ensured via compiler verications. The common way of ensuring consistency is to use an abstract data type for the representatives; unfortunately, pattern matching on r...

• Type: Conference
• Year: 2007
• Where: ESOP
• Authors: Frédéric Blanqui, Thérèse Hardin, Pierre Weis
• Keywords: Concrete Data Type, Construction Functions, Data Type, ESOP 2007, Programming Languages