Toward formal development of programs from algebraic specifications: Implementations revisited

Donald Sannella; Andrzej Tarlecki

doi:10.1007/3-540-17660-8_50

Toward formal development of programs from algebraic specifications: Implementations revisited

Donald Sannella, Andrzej Tarlecki

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	TAPSOFT '87
Subtitle of host publication	Proceedings of the International Joint Conference on Theory and Practice of Software Development Pisa, Italy, March 23–27, 1987
Editors	Hartmut Ehrig, Robert Kowalski, Giorgio Levi, Ugo Montanari
Publisher	Springer
Pages	96-110
Number of pages	15
ISBN (Electronic)	978-3-540-47746-4
ISBN (Print)	978-3-540-17660-2
DOIs	https://doi.org/10.1007/3-540-17660-8_50
Publication status	Published - 1987

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	249
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/3-540-17660-8_50

Cite this

Sannella, D., & Tarlecki, A. (1987). Toward formal development of programs from algebraic specifications: Implementations revisited. In H. Ehrig, R. Kowalski, G. Levi, & U. Montanari (Eds.), TAPSOFT '87: Proceedings of the International Joint Conference on Theory and Practice of Software Development Pisa, Italy, March 23–27, 1987 (pp. 96-110). (Lecture Notes in Computer Science; Vol. 249). Springer. https://doi.org/10.1007/3-540-17660-8_50

Sannella, Donald ; Tarlecki, Andrzej. / Toward formal development of programs from algebraic specifications: Implementations revisited. TAPSOFT '87: Proceedings of the International Joint Conference on Theory and Practice of Software Development Pisa, Italy, March 23–27, 1987. editor / Hartmut Ehrig ; Robert Kowalski ; Giorgio Levi ; Ugo Montanari. Springer, 1987. pp. 96-110 (Lecture Notes in Computer Science).

@inproceedings{40696e44a2c54bc3844fba3f556d83ba,

title = "Toward formal development of programs from algebraic specifications: Implementations revisited",

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.",

author = "Donald Sannella and Andrzej Tarlecki",

year = "1987",

doi = "10.1007/3-540-17660-8\_50",

language = "English",

isbn = "978-3-540-17660-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "96--110",

editor = "Hartmut Ehrig and Robert Kowalski and Giorgio Levi and Ugo Montanari",

booktitle = "TAPSOFT '87",

address = "United Kingdom",

}

Sannella, D & Tarlecki, A 1987, Toward formal development of programs from algebraic specifications: Implementations revisited. in H Ehrig, R Kowalski, G Levi & U Montanari (eds), TAPSOFT '87: Proceedings of the International Joint Conference on Theory and Practice of Software Development Pisa, Italy, March 23–27, 1987. Lecture Notes in Computer Science, vol. 249, Springer, pp. 96-110. https://doi.org/10.1007/3-540-17660-8_50

Toward formal development of programs from algebraic specifications: Implementations revisited. / Sannella, Donald; Tarlecki, Andrzej.
TAPSOFT '87: Proceedings of the International Joint Conference on Theory and Practice of Software Development Pisa, Italy, March 23–27, 1987. ed. / Hartmut Ehrig; Robert Kowalski; Giorgio Levi; Ugo Montanari. Springer, 1987. p. 96-110 (Lecture Notes in Computer Science; Vol. 249).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Toward formal development of programs from algebraic specifications: Implementations revisited

AU - Sannella, Donald

AU - Tarlecki, Andrzej

PY - 1987

Y1 - 1987

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

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

U2 - 10.1007/3-540-17660-8_50

DO - 10.1007/3-540-17660-8_50

M3 - Conference contribution

SN - 978-3-540-17660-2

T3 - Lecture Notes in Computer Science

SP - 96

EP - 110

BT - TAPSOFT '87

A2 - Ehrig, Hartmut

A2 - Kowalski, Robert

A2 - Levi, Giorgio

A2 - Montanari, Ugo

PB - Springer

ER -

Sannella D, Tarlecki A. Toward formal development of programs from algebraic specifications: Implementations revisited. In Ehrig H, Kowalski R, Levi G, Montanari U, editors, TAPSOFT '87: Proceedings of the International Joint Conference on Theory and Practice of Software Development Pisa, Italy, March 23–27, 1987. Springer. 1987. p. 96-110. (Lecture Notes in Computer Science). doi: 10.1007/3-540-17660-8_50

Toward formal development of programs from algebraic specifications: Implementations revisited

Abstract

Publication series

Access to Document

Fingerprint

Cite this