×

zbMATH — the first resource for mathematics

Functorial theory of parameterized specifications in a general specification framework. (English) Zbl 0829.68086
Summary: A general specification framework based on the notion of indexed categories is introduced in order to study the structural aspects of specifications independent of the underlying logics. Similar to institutions this concept of specification frames allows to formulate a unified structural theory of various kinds of algebraic specifications which have been studied separately in the literature before. In contract to institutions we do not require to have satisfaction relations and conditions which allows to handle also behavioural specifications and semantics and various concepts of constraints in this framework.
In this framework we generalize the well-known theory of parametrized algebraic specifications with initial semantics from the equational case to specification frames satisfying mainly three basic axioms: The existence of pushouts, free constructions and amalgamation. Moreover, an axiomatic treatment of restriction is presented which allows to study in addition to refinement also implementations of parametrized specifications including restrictions. Finally we present an axiomatic framework for functorial semantics which opens the way to apply the theory not only to initial semantics but also to other kinds of functorial semantics, including final and specific kinds of loose semantics.
Reviewer: Reviewer (Berlin)

MSC:
68Q65 Abstract data types; algebraic specification
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Andréka, H.; Németi, I., A general axiomatizability theorem formulated in terms of cone-injective, (), 13-35, Colloquia Mathematica Societas János Bolyai, 29
[2] Baldamus, M., Constraints and their normal forms in the framework of specification logics, (1990), Studienarbeit TU Berlin, (in German)
[3] Baumeister, H., Unifying initial and loose semantics of parameterized specifications in an arbitary institutions, (), 103-120, (Brighton 1991) · Zbl 0967.68533
[4] Benabou, J., Fibred categories and the foundations of naive category theorem, J. symbolic logic, 50, 10-37, (1985) · Zbl 0564.18001
[5] Blum, E.K.; Ehrig, H.; Parisi-Presicce, F., Algebraic specification of modules and their basic interconnections, J. comput. system sci., 34, 2/3, 293-339, (1987) · Zbl 0619.68027
[6] Burstall, R.M.; Goguen, J.A., Semantics of CLEAR, a specification language, (), 293-332, Abstract Software Specifications · Zbl 0456.68024
[7] Burstall, R.M.; Goguen, J.A.; Tarlecki, A., Some fundamental algebraic tools for the semantics of computation, part 3: indexed categories, (), Theoret. comput. sci., 91, 239-264, (1991) · Zbl 0755.18004
[8] Compass espirit brg WG no.3264, (1991), University of Bremen 7⧸91, Final Report, Tech. Report
[9] Diaconescu, R.; Goguen, J.; Stefaneas, P., Logical support for modularization, ()
[10] Ehrig, H.; Baldamus, M.; Cornelius, F.; Orejas, F., Theory of algebraic module specifications including behavioural semantics, constraitns and aspects of generalized morphisms, Proc. AM AST’91, (1991), Iowa City
[11] H. Ehrig, M. Baldamus, F. Cornelius and F. Orejas, Abstract and behavioural module specifications, submitted for publication. · Zbl 0923.68089
[12] Ehrig, H.; Baldamus, M.; Orejas, F., New concepts for amalgamation and extension in the framework of specification logic, (), (long version)
[13] Ehrig, H., A categorical concept of constraints for algebraic specifications, (), 1-15
[14] Ehrig, H., Algebraic specification of modules and modular software systems within the framework of specification logics, Tech. report. 89/17, (1989), TU Berlin
[15] Ehrig, H., Concepts and compatibility requirements for implementations and transformations of specifications, algebraic specification column, Bull. EATCS38, 79-92, (1989), Part 6
[16] Ehrig, H., Algebraic theory of parameterized specifications with requirements, Proc. CAAP ’81, Lecture notes in computer science, Vol. 112, 1-24, (1981) · Zbl 0465.68006
[17] Ehrig, H.; Jimenez, R.M.; Orejas, F., Compositionality results for different types of parameterization and parameter passing in specification languages, Proc. TAPSOFT’93, (1993)
[18] Ehrig, H.; Kreowski, H.-J.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Parameterized data types in algebraic specification languages, Proc. ICALP’80, Lecture notes in computer science, Vol. 85, 157-168, (1980)
[19] Ehrig, H.; Kreowski, H.-J.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Parameter passing in algebraic specification languages, (), Theoret. comput. sci., 45-81, (1984) · Zbl 0522.68027
[20] Ehrich, H.D.; Lohberger, V.G., Constructing specifications of abstract data types by replacements, () · Zbl 0402.68012
[21] Ehrig, H.; Mahr, B., Fundamentals of algebraic specification 1. equations and initial semantics, () · Zbl 0557.68013
[22] Ehrig, H.; Mahr, B., Fundamentals of algebraic specification 2. module specifications and constraints, () · Zbl 0759.68013
[23] Ehrig, H.; Parisi-Presicce, F.; Boehm, P.; Rieckhoff, C.; Dimitrovici, C.; Große-Rhode, M., Combining data type and recursive process specifications using projection algebras, Theoret. comput. sci., 71, 347-380, (1991) · Zbl 0695.68015
[24] Ehrig, H.; Pepper, P.; Orejas, F., On recent trends in algebraic specification, (), 263-288 · Zbl 0689.68013
[25] Ehrig, H.; Wagner, E.; Thatcher, J., Algebraic constraints for specifications and canonical form results, (), FB 20 · Zbl 0518.68019
[26] Ehrig, H.; Wagner, E.G.; Thatcher, J.W., Algebraic specifications with generating constraints, (), 188-202 · Zbl 0518.68019
[27] Ehrig, H.; Weber, H., Algebraic specifications of modules, Proc. IFIP work conf. 85: the role of abstract models in programming, (1985), Wien
[28] Ehrig, H.; Weber, H., Programming in the large with algebraic module specifications, (), 675-684 · Zbl 0606.68009
[29] Ganzinger, H., A final algebra semantics for parameterized specifications, ()
[30] Goguen, J.A.; Burstall, R.M., Introducing institutions, (), 221-256 · Zbl 1288.03001
[31] Goguen, J.A.; Burstall, R.M., Institutions: abstract models, theory for computer science, () · Zbl 1288.03001
[32] Goguen, J.A.; Burstall, R.M., Institutions: abstract model theory for specification and programming, J. ACM, 39, 1, 95-146, (1992) · Zbl 0799.68134
[33] Große-Rhode, M.; Ehrig, H., Transformation of combined data type and process specifications, using projections algebras, (), 301-339
[34] Große-Rhode, M., Parameterized data type and process specifications using projection algebras, ()
[35] Gray, J.W., Fibred and cofibred categories, (), 21-83 · Zbl 0192.10701
[36] Gray, J.W., The integration of logical and algebraic types, (), 16-35
[37] Grothendieck, A.; Grothendieck, A., Catégories fibrées et descente, in: in: revétements étales et groupe fondamental, (), 145-194, reprinted in
[38] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G.; Goguen, J.A.; Thatcher, J.W.; Wagner, E.G., An initial algebra approach to the specification, correctness and implementation of abstract data types, (), 80-144, (1976) · Zbl 0333.93002
[39] Herrlich, H.; Strecker, G.E., Category theory, (1973), Allyn and Bacon Boston · Zbl 0265.18001
[40] Johnstone, P.T.; Paré, R., Indexed categories and their applications, () · Zbl 0372.00009
[41] Mahr, B., Empty carriers: the categorical burden on logic, (), 50-64
[42] Meseguer, T., General logics, (), 275-329
[43] Möller, B., Higher-order algebraic specifications, ()
[44] Mosses, P., An introduction to action semantics, ()
[45] Nivela, P.; Orejas, F., Behavioral semantics for algebraic specification languages, Proc. ADT-Workshop Gullane, 1987, Lecture notes in computer science, Vol. 332, 184-207, (1988) · Zbl 0679.68026
[46] Orejas, F.; Nivela, P.; Ehrig, H., Semantical constructions for categories of behavioral specifications, (), 220-243
[47] Orejas, F.; Nivela, P., Constraints for behavioral specifications, () · Zbl 0679.68026
[48] Padawitz, P., Correctness, completeness, and consistency of equational data type specifications, (), Ph.D. Thesis · Zbl 0525.68007
[49] Padawitz, P., Computing in Horn clause theories, () · Zbl 0646.68004
[50] Poigné, A., On specification theories, and models with higher types, Inform. and control, 68, 1-46, (1986) · Zbl 0591.68019
[51] Reichel, H., Initially restricting algebraic theories, (), 291 · Zbl 0469.68026
[52] Reichel, H., Behavioural equivalence — a unifying concept for initial and final specification methods, Proc. 3rd Hungarian comp. sci. conf., 27-39, (1981), Budapest · Zbl 0479.68017
[53] D. Sannella, S. Sokolowski and A. Tarlecki, Toward formal development of programs from algebraic specifications: parameterisation revisited. FB3-Mathematik/Informatik, Universität Bremen, to appear in: Acta Informatica. · Zbl 0790.68077
[54] Sannella, D.T.; Tarlecki, A., Building specifications in an arbitrary institution, () · Zbl 0552.68015
[55] Tarlecki, A., Software-system development — an abstract view, (), 685-688
[56] Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Data type specification: parameterization and the power of specification techniques, 10th symp. theory of computing, Trans. prog. languages systems, 4, 711-732, (1982) · Zbl 0495.68020
[57] Wells, C.; Barr, M., The formal description of data types using sketches, (), 490-527
[58] Wirsing, M., Structured algebraic specifications: A kernel language, Theoret. comput. sci., 42, 123, 123-249, (1986) · Zbl 0599.68021
[59] Zilles, S.N., Algebraic specification of data types, (), 28-52
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.