English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  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.), TAPSOFT '95: Theory and Practice of Software Development (pp. 756-771). Berlin, Germany: Springer.

Item is

 

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/21.11116/0000-000E-5820-B
Genre: Conference Paper

Files

show Files

Locators

show
hide
Locator:
https://rdcu.be/dxCO4 (Publisher version)
Description:
-
OA-Status:
Not specified

Creators

show
hide
 Creators:
Baumeister, Hubert1, 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: 2010-03-121995
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519507
Other: Local-ID: C1256104005ECAFC-4357FF8D279CD440C12562D900664EC6-Baumeister95
DOI: 10.1007/3-540-59293-8_233
BibTex Citekey: Baumeister_TaPSOFT95
 Degree: -

Event

show
hide
Title: 6th Joint Conference on Theory and Practice of Software Development
Place of Event: Århus, Denmark
Start-/End Date: 1995-05-22 - 1995-05-26

Legal Case

show

Project information

show

Source 1

show
hide
Title: TAPSOFT '95: Theory and Practice of Software Development
  Subtitle : 6th International Joint Conference CAAP/FASE, Aarhus, Denmark, May 22 - 26, 1995. Proceedings
  Abbreviation : TAPSOFT 1995
Source Genre: Proceedings
 Creator(s):
Mosses, Peter D.1, Editor
Nielsen, Mogens1, Editor
Schwartzbach, Michael I.1, Editor
Affiliations:
1 External Organizations, ou_persistent22            
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 756 - 771 Identifier: ISBN: 978-3-540-59293-8

Source 2

show
hide
Title: Lecture Notes in Computer Science
  Abbreviation : LNCS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 915 Sequence Number: - Start / End Page: - Identifier: -