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

Walter Dosch; Sönke Magnussen

doi:10.1007/978-3-540-24675-6_6

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

Walter Dosch^*, Sönke Magnussen

^*Corresponding author for this work

Institute of Software Engineering and Programming Languages

Lufthansa Revenue Services GmbH

3 Citations (Scopus)

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

Original language	English
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3026
Pages (from-to)	7-33
Number of pages	27
ISSN	0302-9743
DOIs	https://doi.org/10.1007/978-3-540-24675-6_6
Publication status	Published - 01.12.2004

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/978-3-540-24675-6_6

Cite this

@article{41bcf3cc9fef4fc29e2151a0c1227eac,

title = "Computer-aided refinement of data structures on higher-order algebraic specifications",

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{\"u}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].",

author = "Walter Dosch and S{\"o}nke Magnussen",

year = "2004",

month = dec,

day = "1",

doi = "10.1007/978-3-540-24675-6_6",

language = "English",

volume = "3026",

pages = "7--33",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

}

Computer-aided refinement of data structures on higher-order algebraic specifications. / Dosch, Walter; Magnussen, Sönke.
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 3026, 01.12.2004, p. 7-33.

Research output: Journal Articles › Journal articles › Research › peer-review

TY - JOUR

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

AU - Dosch, Walter

AU - Magnussen, Sönke

PY - 2004/12/1

Y1 - 2004/12/1

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

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

UR - http://www.scopus.com/inward/record.url?scp=35048901595&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-24675-6_6

DO - 10.1007/978-3-540-24675-6_6

M3 - Journal articles

AN - SCOPUS:35048901595

SN - 0302-9743

VL - 3026

SP - 7

EP - 33

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -

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

Abstract

UN SDGs

Access to Document

Other files and links

Fingerprint

Cite this