Toward formal development of programs from algebraic specifications: Implementations revisited
type: Item
instance of: scholarly article
title: Toward formal development of programs from algebraic specifications: Implementations revisited
zbMATH Open document ID: 0621.68004
DOI: 10.1007/BF02737104
author: Donald Sannella
author: Andrzej Tarlecki
published in: Acta Informatica
publication date: 1988-01-01T00:00:00Z
review text: 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 are shown to generalize to the framework of an arbitrary institution, and a way of changing institutions during the implementation process is introduced. All this is illustrated by means of simple concrete examples.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68P05
zbMATH DE Number: 4007698
zbMATH Keywords: program development process
zbMATH Keywords: refinement
zbMATH Keywords: constructor implementations
zbMATH Keywords: abstractor implementations
zbMATH Keywords: institution
describes a project that uses: ML
MaRDI profile type: Publication
cites work: Q4152697
cites work: Q3677154
cites work: Axioms for abstract model theory
cites work: Programming in a wide spectrum language: A collection of examples
cites work: Q3709866
cites work: Q3695436
cites work: Algebraic implementations preserve program correctness
cites work: Partial abstract types
cites work: Q3731650
cites work: Q3906394
cites work: Q3667921
cites work: Testing equivalences for processes
cites work: Q3917479
cites work: On the Theory of Specification, Implementation, and Parametrization of Abstract Data Types
cites work: Q3341871
cites work: Q3947104
cites work: Algebraic implementation of abstract data types
cites work: Q3906461
cites work: Q3221381
cites work: Q3667933
cites work: Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability
cites work: Q4105777
cites work: Algebraic and operational semantics of specifications allowing exceptions and errors
cites work: Q3332238
cites work: Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories
cites work: Q4723263
cites work: Q3719824
cites work: Q3956373
cites work: Initial Algebra Semantics and Continuous Algebras
cites work: Q4199490
cites work: Report on the Larch shared language
cites work: Final Data Types and Their Specification
cites work: Q3668830
cites work: Q4693151
cites work: A Deductive Approach to Program Synthesis
cites work: Q3687683
cites work: A theory of type polymorphism in programming
cites work: Q3686016
cites work: Q3677150
cites work: LCF considered as a programming language
cites work: Q3938468
cites work: Q3707381
cites work: Q3677153
cites work: Q3345753
cites work: Q4725720
cites work: On observational equivalence and algebraic specification
cites work: Q4721633
cites work: Q3954805
cites work: Q3666260
cites work: On the existence of free models in abstract algebraic institutions
cites work: Quasi-varieties in abstract algebraic institutions
cites work: Q3687694
cites work: Specifications, models, and implementations of data abstractions
cites work: Structured algebraic specifications: A kernel language
full work available at URL: https://doi.org/10.1007/bf02737104
OpenAlex ID: W4249644839
description: scientific article; zbMATH DE number 4007698