Relations as Abstract Datatypes: An Institution to Specify Relations between 
Algebras

Baumeister, Hubert

doi:10.1007/3-540-59293-8_233

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Relations as Abstract Datatypes: An Institution to Specify Relations between Algebras

MPS-Authors

/persons/resource/persons44086

Baumeister, Hubert
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

https://rdcu.be/dxCO4
(Publisher version)

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Baumeister, H. (1995). Relations as Abstract Datatypes: An Institution to Specify Relations between Algebras. In P. D. Mosses, M. Nielsen, & M. I. Schwartzbach (Eds.), TAPSOFT '95: Theory and Practice of Software Development (pp. 756-771). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-AD16-B

Abstract

One way to model the execution state of an imperative program is as
a many sorted algebra. Program variables are modeled by functions
and their types by sorts. The execution of a program is modeled by a
relation between the states of the program (algebras) before and after
the execution of the program. There are several methods to specify such
relations between algebras. One method is to use specifications in the
style of Z, VDM-SL or Larch. Specifications in Z of relations between
states are first order formulas over the value of the variables comprising
the state before and after an operation. In this paper we shall define an
institution for the specification of relations between structures of some
base institution (eg.\ the institution of equational logic or first order
predicate logic).
Sets of structures over a common signature, abstract datatypes, in this
institution
denote relations between structures of the base institution. This makes it
possible to apply a rich repertoire of already existent techniques for
specifying
abstract datatypes, which can be found for example in the work of Goguen
and Burstall, Sannella, Wirsing and Tarlecki, Ehrig, Pepper and Orejas and
others, to the specification of relations. This paper tries to narrow the gap
between
algebraic specification languages like Clear, ASL or Act-One and
model theoretic based specification languages like Z, VDM-SL or the
Larch Interface language.