Computer-aided refinement of data structures on higher-order algebraic specifications

Walter Dosch*, Sönke Magnussen

*Corresponding author for this work
3 Citations (Scopus)


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].

Original languageEnglish
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages (from-to)7-33
Number of pages27
Publication statusPublished - 01.12.2004


Dive into the research topics of 'Computer-aided refinement of data structures on higher-order algebraic specifications'. Together they form a unique fingerprint.

Cite this