Implementation of parameterised specifications: Automata, Languages and Programming

Donald Sannella, Martin Wirsing

Research output: Chapter in Book/Report/Conference proceedingChapter


A new notion is given for the implementation of one specification by another. Unlike most previous notions, this generalises to handle parameterised specifications as well as loose specifications (having an assortment of non-isomorphic models). Examples are given to illustrate the notion. The definition of implementation is based on a new notion of the simulation of a theory by an algebra. For the bulk of the paper we employ a variant of the Clear specification language [BG 77] in which the notion of a data constraint is replaced by the weaker notion of a hierarchy constraint. All results hold for Clear with data constraints as well, but only under more restrictive conditions.

We prove that implementations compose vertically (two successive implementation steps compose to give one large step) and that they compose horizontally under application of (well-behaved) parameterised specifications (separate implementations of the parameterised specification and the actual parameter compose to give an implementation of the application).
Original languageEnglish
Title of host publicationAutomata, Languages and Programming
Subtitle of host publicationNinth Colloquium Aarhus, Denmark, July 12–16, 1982
EditorsMogens Nielsen, Erik Meineche Schmidt
PublisherSpringer-Verlag GmbH
Number of pages16
ISBN (Electronic)978-3-540-39308-5
ISBN (Print)978-3-540-11576-2
Publication statusPublished - 1982

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Implementation of parameterised specifications: Automata, Languages and Programming'. Together they form a unique fingerprint.

Cite this