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

Baumeister, Hubert

DetailsSummary

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

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

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-AD16-B Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-AD17-9

Genre: Conference Paper

Files

show Files

Locators

show

Creators

show

hide

Creators:
Baumeister, Hubert¹, Author

Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Content

show

hide

Free keywords: -

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.

Details

show

hide

Language(s): eng - English

Dates: Modified: 2010-03-12Date issued: 1995

Publication Status: Issued

Pages: -

Publishing info: Berlin, Germany : Springer

Table of Contents: -

Rev. Type: -

Identifiers: eDoc: 519507
Other: Local-ID: C1256104005ECAFC-4357FF8D279CD440C12562D900664EC6-Baumeister95

Degree: -

Event

show

hide

Title: Untitled Event

Place of Event: Århus, Denmark

Start-/End Date: -

Legal Case

show

Project information

show

Source 1

show

hide

Title: Proceedings of the 6th Joint Conference on Theory and Practice of Software Development (TAPSOFT '95)

Source Genre: Proceedings

Creator(s):
Mosses, Peter D., Editor
Nielsen, Mogens, Editor
Schwartzbach, Michael I., Editor

Affiliations:
-

Publ. Info: Berlin, Germany : Springer

Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 756 - 771 Identifier: -

Source 2

show

hide

Title: Lecture Notes in Computer Science

Source Genre: Series

Creator(s):

Affiliations:

Publ. Info: -

Pages: - Volume / Issue: - Sequence Number: - Start / End Page: - Identifier: -