Toward formal development of programs from algebraic specifications: Implementations revisited

Donald Sannella, Andrzej Tarlecki

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The program development process is viewed as a sequence of implementation steps leading from a specification to a program. Based on an elementary notion of refinement, two notions of implementation are studied: constructor implementations which involve a construction "on top of" the implementing specification, and abstractor implementations which additionally provide for abstraction from some details of the implemented specification. These subsume most formal notions of implementation in the literature. Both kinds of implementations satisfy a vertical composition and a (modified) horizontal composition property. All the definitions and results generalise to the framework of an arbitrary institution.
Original languageEnglish
Title of host publicationTAPSOFT '87
Subtitle of host publicationProceedings of the International Joint Conference on Theory and Practice of Software Development Pisa, Italy, March 23–27, 1987
EditorsHartmut Ehrig, Robert Kowalski, Giorgio Levi, Ugo Montanari
PublisherSpringer-Verlag GmbH
Pages96-110
Number of pages15
ISBN (Electronic)978-3-540-47746-4
ISBN (Print)978-3-540-17660-2
DOIs
Publication statusPublished - 1987

Publication series

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

Fingerprint

Dive into the research topics of 'Toward formal development of programs from algebraic specifications: Implementations revisited'. Together they form a unique fingerprint.

Cite this