A modular framework for specification and implementation

Martin Wirsing, Manfred Broy

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

9 Scopus citations

Abstract

A modular framework for the formal specification and implementation of large families of sorts and functions is introduced. It is intended to express generation principles, to rename, combine and construct implementations of specifications in flexible styles. Parameterization is also included. The main characteristics of this approach are the inclusion of predicates in the signature of specifications and the use of an ultra-loose semantics. Signatures are triples of sets of sorts, sets of function symbols and sets of predicate symbols; the latter contain among others also standard predicate symbols, in particular the equality symbols as well as predicate symbols expressing generation principles which hold for an object if and only if it can be denoted by a term of a specific signature. These standard predicate symbols lead to an ultra-loose semantics for specifications: models are not required to be term-generated; instead, the term-generated subalgebra of a model is required to satisfy the axioms. Main advantages of this approach are the simplicity of the notion of implementation and the simplicity of the corresponding language for writing structured specifications.

Original languageEnglish
Title of host publicationTAPSOFT 1989
Subtitle of host publicationProceedings of the International Joint Conference on Theory and Practice of Software Development - Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming, CAAP 1989
EditorsJosep Diaz, Fernando Orejas
PublisherSpringer Verlag
Pages42-73
Number of pages32
ISBN (Print)9783540509394
DOIs
StatePublished - 1989
Externally publishedYes
Event3rd International Joint Conference on Theory and Practice of Software Development, TAPSOFT 1989 - Barcelona, Spain
Duration: 13 Mar 198917 Mar 1989

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume351 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Joint Conference on Theory and Practice of Software Development, TAPSOFT 1989
Country/TerritorySpain
CityBarcelona
Period13/03/8917/03/89

Fingerprint

Dive into the research topics of 'A modular framework for specification and implementation'. Together they form a unique fingerprint.

Cite this