Abstract
The paper studies the transformational refinement of data structures in the framework of higher-order algebraic specifications. We present novel procedures that mechanize the refinement of entire data structures within a single complex transformation step. The transformations validate a general refinement relation that captures different types of simulations. General transformation rules describe algebraic implementations based on abstraction and representation functions. Specialized transformations cover particular changes between data structures. All transformation procedures have been implemented in the Lübeck Transformation System. The system uses analysis algorithms to establish the soundness conditions of the transformations by syntactic criteria. We report practical experiences about manipulating data structures with the system. The paper summarizes results from the second author's PhD thesis [20].
| Originalsprache | Englisch |
|---|---|
| Zeitschrift | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Jahrgang | 3026 |
| Seiten (von - bis) | 7-33 |
| Seitenumfang | 27 |
| ISSN | 0302-9743 |
| DOIs | |
| Publikationsstatus | Veröffentlicht - 01.12.2004 |