Abstract
We propose to detect isomorphisms of algebraic modular specifications, by representing specifications as diagrams over a category C o of base specifications and specification morphisms. We start with a formulation of modular specifications as terms, which are interpreted as diagrams. This representation has the advantage of being more abstract, i.e. less dependent of one specific construction than terms. For that, we define a category diagr (C o) of diagrams, which is a completion of C o with finite colimits. The category diagr (C o) is finitely cocomplete, even if C o is not finitely cocomplete. We define a functor
: Term (C o) → diagr (C o) which maps specifications to diagrams, and specification morphisms to diagram morphisms. This interpretation is sound in that the colimit of a diagram representing a specification is isomorphic to this specification. The problem of isomorphisms of modular specifications is solved by detecting isomorphisms of diagrams.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In Proceedings of ESOP'86, number 213 in LNCS, pages 119–132. Springer-Verlag, 1986.
M. Bidoit. The stratified loose approach: A generalization of initial and loose semantics. Technical Report 402, Université d'Orsay, France, 1988.
R.M. Burstall and J.A. Goguen. Putting theories together to make specifications. In Int. Conf. Artificial Intelligence, 1977.
R.M. Burstall and J.A. Goguen. The semantics of CLEAR, a specification language. In Proc. Advanced Course on Abstract Software Specification, number 86 in LNCS, pages 292–332. Springer-Verlag, 1980.
J. Cartmell. Generalized algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209–243, 1986.
H. Ehrig and B. Mahr. Fundamentals of algebraic specification 1. Equations and initial semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.
K. Futatsugi, J.A. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proc. Principles of Programming Languages, pages 52–66, 1985.
M.-C. Gaudel. A first introduction to PLUSS. Technical report, Université d'Orsay, France, 1984.
S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.
J.-C Reynaud. Putting algebraic components together: A dependent type approach. Research Report 810 I IMAG, LIFIA, Apr. 1990.
J.-C. Reynaud. Putting algebraic components together: A dependent type approach. Number 429 in LNCS. Springer-Verlag, 1990.
J.-C. Reynaud. Isomorphism of typed algebraic specifications. Internal Report, LGI-IMAG, Feb. 1993.
A. Tarlecki, R.M. Burstall, and J.A. Goguen. Some fundamental algebraic tools for the semantics of computation: Part 3. indexed categories. Theoretical Computer Science, 91:239–264, 1991.
M. Wirsing. Structured Algebraic Specifications: A Kernel Language. Theoretical Computer Science, 42:123–249, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Oriat, C. (1995). Detecting isomorphisms of modular specifications with diagrams. In: Alagar, V.S., Nivat, M. (eds) Algebraic Methodology and Software Technology. AMAST 1995. Lecture Notes in Computer Science, vol 936. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60043-4_53
Download citation
DOI: https://doi.org/10.1007/3-540-60043-4_53
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60043-5
Online ISBN: 978-3-540-49410-2
eBook Packages: Springer Book Archive