×

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.

MSC:

68Q65 Abstract data types; algebraic specification
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Andréka, H.; Németi, I., A general axiomatizability theorem formulated in terms of cone-injective, (Universal Algebra (1981), North-Holland: North-Holland Amsterdam), 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: Studienarbeit TU Berlin, (in German)
[3] Baumeister, H., Unifying initial and loose semantics of parameterized specifications in an arbitary institutions, (Proc. TAPSOFT’91. Proc. TAPSOFT’91, Lecture Notes in Computer Science, Vol. 493 (1991), Springer: Springer Berlin), 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, (Björner, D., Proc. 1979 Copenhagen Winter School. Proc. 1979 Copenhagen Winter School, Lecture Notes in Computer Science, Vol. 86 (1980)), 293-332, Abstract Software Specifications · Zbl 0456.68024
[7] 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, (Tech. Report (1991), University of Oxford)
[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.; 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, (Tech. Report 91/02 (1991), TU: TU Berlin), (long version)
[13] Ehrig, H., A categorical concept of constraints for algebraic specifications, (Ehrig, H.; Herrlich, H.; Kreowski, H.-J.; Preuß, G., Categorical Methods in Computer Science — with Aspects from Topology. Categorical Methods in Computer Science — with Aspects from Topology, Lecture Notes in Computer Science, Vol. 393 (1989), Springer: Springer Berlin), 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. 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) · Zbl 1497.68296
[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. 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, (Proc. Workshop on Program Specification, Aarhus 1981. Proc. Workshop on Program Specification, Aarhus 1981, Lecture Notes in Computer Science, Vol. 134 (1984), Springer: Springer Berlin). (Proc. Workshop on Program Specification, Aarhus 1981. Proc. Workshop on Program Specification, Aarhus 1981, Lecture Notes in Computer Science, Vol. 134 (1984), Springer: Springer Berlin), Theoret. Comput. Sci., 45-81 (1984) · Zbl 0522.68027
[20] Ehrich, H. D.; Lohberger, V. G., Constructing specifications of abstract data types by replacements, (Internat. Workshop Graph Grammars and Their Applications to Comp. Sci. &Biology (1978), Bad Honnef) · Zbl 0402.68012
[21] Ehrig, H.; Mahr, B., Fundamentals of Algebraic Specification 1. Equations and Initial Semantics, (EATCS Monographs on Theoretical Computer Science, Vol. 6 (1985), Springer: Springer Berlin) · Zbl 0557.68013
[22] Ehrig, H.; Mahr, B., Fundamentals of Algebraic Specification 2. Module Specifications and Constraints, (EATCS Monographs on Theoretical Computer Science, Vol. 21 (1990), Springer: Springer Berlin) · 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, (Proc. ICALP’89. Proc. ICALP’89, Lecture Notes in Computer Science, Vol. 372 (1989), Springer: Springer Berlin), 263-288 · Zbl 0689.68013
[25] Ehrig, H.; Wagner, E.; Thatcher, J., Algebraic constraints for specifications and canonical form results, (Tech. Report. No. 82-09 (1982), TU: TU Berlin), FB 20 · Zbl 0518.68019
[26] Ehrig, H.; Wagner, E. G.; Thatcher, J. W., Algebraic specifications with generating constraints, (Proc. ICAP’83. Proc. ICAP’83, Lectures Notes in Computer Science, Vol. 154 (1983), Springer: Springer Berlin), 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, (Kugler, H. J., Information Processing 86 (1986), North-Holland: North-Holland Amsterdam), 675-684 · Zbl 0606.68009
[29] Ganzinger, H., A final algebra semantics for parameterized specifications, (Tech. Report (1980), TU: TU München)
[30] Goguen, J. A.; Burstall, R. M., Introducing institutions, (Proc. Logics of Programming Workshop, Carnegie-Mellon. Proc. Logics of Programming Workshop, Carnegie-Mellon, Lecture Notes in Computer Science, Vol. 164 (1984), Springer: Springer Berlin), 221-256 · Zbl 1288.03001
[31] Goguen, J. A.; Burstall, R. M., Institutions: Abstract models, theory for computer science, (Tech. Report CSLI-85-30 (1985), Stanford University) · 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, (Stepwise Refinement of Distributed Systems, REX-Workshop 1989. Stepwise Refinement of Distributed Systems, REX-Workshop 1989, Lecture Notes in Computer Science, Vol. 430 (1990), Springer: Springer Berlin), 301-339
[34] Große-Rhode, M., Parameterized data type and process specifications using projection algebras, (Ehrig, H.; Herrlich, H.; Kreowski, H.-J.; Preuß, G., Categorical Methods in Computer Science — with Aspects from Topology. Categorical Methods in Computer Science — with Aspects from Topology, Lecture Notes in Computer Science, Vol. 393 (1989), Springer: Springer Berlin)
[35] Gray, J. W., Fibred and cofibred categories, (Eilenberg, S.; Harrison, D. K.; MacLane, S.; Röhrl, H., Proc. Conf. on Categorical Algebra (1966), Springer: Springer Berlin), 21-83 · Zbl 0192.10701
[36] Gray, J. W., The integration of logical and algebraic types, (Lecture Notes in Computer Science, Vol. 393 (1989), Springer: Springer Berlin), 16-35
[37] Grothendieck, A., Catégories fibrées et descente, in: in: Revétements étales et groupe fondamental, (Lecture Notes in Mathematics, Vol. 224 (1971), Springer: Springer Berlin), 145-194, reprinted in
[38] Goguen, J. A.; Thatcher, J. W.; Wagner, E. G., An initial algebra approach to the specification, correctness and implementation of abstract data types, (Yeh, R., Current Trends in Programming Methodology IV: Data Structuring (1978), Prentice Hall: Prentice Hall Englewood cliffs, NJ), 80-144 · Zbl 0333.93002
[39] Herrlich, H.; Strecker, G. E., Category Theory (1973), Allyn and Bacon: Allyn and Bacon Boston · Zbl 0265.18001
[40] Johnstone, P. T.; Paré, R., Indexed categories and their applications, (Lecture Notes in Mathematics, Vol. 661 (1978), Springer: Springer Berlin) · Zbl 0372.00009
[41] Mahr, B., Empty carriers: the categorical burden on logic, (Ehrig, H.; Herrlich, H.; Kreowski, H.-J.; Preuß, G., Categorical Methods in Computer Science — with Aspects from Topology. Categorical Methods in Computer Science — with Aspects from Topology, Lecture Notes in Computer Science, Vol. 393 (1989), Springer: Springer Berlin), 50-64
[42] Meseguer, T., General logics, (Ebbinhaus, H. D., Logic Colloquium ’87 (1989), North-Holland: North-Holland Amsterdam), 275-329
[43] Möller, B., Higher-order algebraic specifications, (Habilitationsschrift (1987), TU: TU München)
[44] Mosses, P., An Introduction to Action Semantics, (Tech. Report DAIMI PB-370 (1991), Aarhus University)
[45] Nivela, P.; Orejas, F., Behavioral semantics for algebraic specification languages, Proc. ADT-Workshop Gullane, 1987. 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, (Ehrig, H.; Herrlich, H.; Kreowski, H.-J.; Preuß, G., Computer Science — with Aspects from Topology. Computer Science — with Aspects from Topology, Lecture Notes in Computer Science, Vol. 393 (1989)), 220-243
[47] Orejas, F.; Nivela, P., Constraints for behavioral specifications, (Technical Report (1990), University Politecnica de Catalunya) · Zbl 0679.68026
[48] Padawitz, P., Correctness, completeness, and consistency of equational data type specifications, (Tech. Report No. 83-1 (1983), TU: TU Berlin), Ph.D. Thesis · Zbl 0525.68007
[49] Padawitz, P., Computing in Horn Clause Theories, (EATCS Monographs on Theoretical Computer Science, Vol. 16 (1988), Springer: Springer Berlin) · 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, (Proc. MFCS’80. Proc. MFCS’80, Lecture Notes in Computer Science, Vol. 88 (1980), Springer: Springer Berlin), 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; 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, (Proc. the Internat. Symp. on Semantics of Data Types. Proc. the Internat. Symp. on Semantics of Data Types, Lecture Notes in Computer Science, Vol. 173 (1984), Springer: Springer Berlin) · Zbl 0552.68015
[55] Tarlecki, A., Software-system development — An abstract view, (Kugler, H. J., Information Proc. 86 (1986), North-Holland: North-Holland Amsterdam), 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. 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, (Lecture Notes in Computer Science, Vol. 298 (1987), Springer: Springer Berlin), 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, (Project MAC Progress Report 11 (1974), MIT), 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.