×

A hidden agenda. (English) Zbl 0946.68070

Summary: This paper publicly reveals, motivates, and surveys the results of an ambitious hidden agenda for applying algebra to software engineering. The paper reviews selected literature, introduces a new perspective on nondeterminism, and features powerful hidden coinduction techniques for proving behavioral properties of concurrent systems, especially refinements; some proofs are given using OBJ3. We also discuss where modularization, bisimulation, transition systems and combinations of the object, logic, constraint and functional paradigms fit into our hidden agenda.

MSC:

68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

CafeOBJ; OBJ3
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S., Interaction categories and communicating sequential processes, (Roscoe, A. W., A Classical MindEssays in Honour of C.A.R. Hoare (1994), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 1-15
[2] P. Aczel, N. Mendler, A final coalgebra theorem, in: D.H. Pitt et al. (Eds.), Category Theory and Computer Science, Lecture Notes in Computer Science, Vol. 389, Springer, Berlin, 1989.; P. Aczel, N. Mendler, A final coalgebra theorem, in: D.H. Pitt et al. (Eds.), Category Theory and Computer Science, Lecture Notes in Computer Science, Vol. 389, Springer, Berlin, 1989.
[3] America, P.; de Bakker, J.; Kok, J.; Rutten, J., Denotational semantics of a parallel object-oriented language, Inform. and Comput., 83, 2, 152-205 (1990) · Zbl 0695.68058
[4] J. Baeten, W.P. Weijland, Process Algebra, Cambridge, 1990, Cambridge Tracts in Theoretical Computer Science, Vol. 18.; J. Baeten, W.P. Weijland, Process Algebra, Cambridge, 1990, Cambridge Tracts in Theoretical Computer Science, Vol. 18.
[5] Barr, M., Terminal coalgebras in well-founded set theory, Theoret. Comput. Sci., 114, 299-315 (1993) · Zbl 0779.18004
[6] Bidoit, M.; Hennicker, R.; Wirsing, M., Behavioural and abstractor specifications, Sci. Comput. Programming, 25, 2-3, 149-186 (1995) · Zbl 0853.68130
[7] Birkhoff, G., On the structure of abstract algebras, Proc. Cambridge Philos. Soc., 1935 (31)
[8] Boehm, B., Software Engineering Economics (1981), Prentice-Hall: Prentice-Hall Englewood cliffs, NJ · Zbl 0525.90034
[9] R. Burstall, Programming with modules as typed functional programming, Proc. Internat. Conf. on Fifth Generation Computing Systems, 1985.; R. Burstall, Programming with modules as typed functional programming, Proc. Internat. Conf. on Fifth Generation Computing Systems, 1985.
[10] Burstall, R.; Diaconescu, R., Hiding and behaviouran institutional approach, (Roscoe, A. W., A Classical MindEssays in Honour of C.A.R. Hoare (1994), Prentice Hall: Prentice Hall Englewood Cliffs, NJ), 75-92
[11] R. Burstall, J. Goguen, Putting theories together to make specifications, in: R. Reddy (Ed.), Proc. Internat. Joint Conf. on Artificial Intelligence, 5th Department of Computer Science, Carnegie-Mellon University, 1977, pp. 1045-1058.; R. Burstall, J. Goguen, Putting theories together to make specifications, in: R. Reddy (Ed.), Proc. Internat. Joint Conf. on Artificial Intelligence, 5th Department of Computer Science, Carnegie-Mellon University, 1977, pp. 1045-1058.
[12] Button, G.; Sharrock, W., Occasioned practises in the work of implementing development methodlogies, (Jirotka, M.; Goguen, J., Requirements EngineeringSocial and Technical Issues (1994), Academic Press: Academic Press New York), 217-240
[13] C. Cı̂rstea, A semantic study of the object paradigm, Transfer Thesis, Programming Research Group, Oxford University, 1996.; C. Cı̂rstea, A semantic study of the object paradigm, Transfer Thesis, Programming Research Group, Oxford University, 1996.
[14] C. Cı̂rstea, Coalgebra semantics for hidden algebra: parameterized objects and inheritance, Paper presented at the 12th Workshop on Algebraic Development Techniques, June 1997.; C. Cı̂rstea, Coalgebra semantics for hidden algebra: parameterized objects and inheritance, Paper presented at the 12th Workshop on Algebraic Development Techniques, June 1997.
[15] R. Diaconescu, The logic of Horn clauses is equational, Technical Report PRG-TR-3-93, Programming Research Group, University of Oxford, 1993, Written in 1990.; R. Diaconescu, The logic of Horn clauses is equational, Technical Report PRG-TR-3-93, Programming Research Group, University of Oxford, 1993, Written in 1990.
[16] R. Diaconescu, Category-based Semantics for Equational and Constraint Logic Programming, Ph.D. Thesis, Programming Research Group, Oxford University, 1994.; R. Diaconescu, Category-based Semantics for Equational and Constraint Logic Programming, Ph.D. Thesis, Programming Research Group, Oxford University, 1994.
[17] Diaconescu, R., A category-based equational logic semantics to constraint programming, (Haveraaen, M.; Owe, O.; Dahl, O. J., Recent Trends in Data Type Specification, Lecture Notes in Computer Science (1996), Springer: Springer Berlin), 200-222
[18] R. Diaconescu, Foundations of behavioural specification in rewriting logic, in: Proc. 1st Int. Workshop on Rewriting Logic and its Applications, Asilomar, California, September 1996, North-Holland, Amsterdam, 1996.; R. Diaconescu, Foundations of behavioural specification in rewriting logic, in: Proc. 1st Int. Workshop on Rewriting Logic and its Applications, Asilomar, California, September 1996, North-Holland, Amsterdam, 1996. · Zbl 0912.68092
[19] R. Diaconescu, K. Futatsugi, CafeOBJ Report, AMAST Series in Computing, Vol. 6, World Scientific, Singapore, 1998.; R. Diaconescu, K. Futatsugi, CafeOBJ Report, AMAST Series in Computing, Vol. 6, World Scientific, Singapore, 1998.
[20] R. Diaconescu, J. Goguen, P. Stefaneas, Logical support for modularisation, in: G. Huet, G. Plotkin (Eds.), Logical Environments, Cambridge, 1993. p. 83-130.; R. Diaconescu, J. Goguen, P. Stefaneas, Logical support for modularisation, in: G. Huet, G. Plotkin (Eds.), Logical Environments, Cambridge, 1993. p. 83-130.
[21] Ehrig, H.; Kreowski, H. J.; Mahr, B.; Padawitz, P., Algebraic implementation of abstract data types, Theoret. Comput. Sci, 20, 209-263 (1983) · Zbl 0483.68018
[22] H. Ehrig, F. Orejas, F. Cornelius, M. Baldamus, Abstract and behaviour module specifications, Technical Report 93-25, Technische Universität Berlin, 1993.; H. Ehrig, F. Orejas, F. Cornelius, M. Baldamus, Abstract and behaviour module specifications, Technical Report 93-25, Technische Universität Berlin, 1993. · Zbl 0923.68089
[23] Eilenberg, S.; Wright, J., Automata in general algebras, Inform. and Control, 11, 452-470 (1967) · Zbl 0175.27902
[24] M.C. Gaudel, I. Privara, Context induction: an exercise, Technical Report 687, LRI, Université de Paris-Sud, 1991.; M.C. Gaudel, I. Privara, Context induction: an exercise, Technical Report 687, LRI, Université de Paris-Sud, 1991.
[25] V. Giarrantana, F. Gimona, U. Montanari, Observability concepts in abstract data specifications, in: Proc. Conf. on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 45, Springer, Berlin, 1976.; V. Giarrantana, F. Gimona, U. Montanari, Observability concepts in abstract data specifications, in: Proc. Conf. on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 45, Springer, Berlin, 1976. · Zbl 0338.68023
[26] J. Goguen, Semantics of computation, in: E.G. Manes (Ed.), Category Theory Applied to Computation and Control, Springer, Berlin, 1975. Lecture Notes in Computer Science, Vol. 25, pp. 151-163, also in Proc. Symp. at University of Massachusetts, Amherst, 1974, pp. 234-249.; J. Goguen, Semantics of computation, in: E.G. Manes (Ed.), Category Theory Applied to Computation and Control, Springer, Berlin, 1975. Lecture Notes in Computer Science, Vol. 25, pp. 151-163, also in Proc. Symp. at University of Massachusetts, Amherst, 1974, pp. 234-249.
[27] Goguen, J., Parameterized programming, Trans. Software Eng., SE-10, 5, 528-543 (1984) · Zbl 0545.68017
[28] J. Goguen, Suggestions for using and organizing libraries in software development, in: S. Kartashev, S. Kartashev (Ed.), Proc. 1st Internat. Conf. on Supercomputing Systems, IEEE Computer Society, 1985. Also in Supercomputing Systems, Steven and Svetlana Kartashev (Eds.), Elsevier, Amsterdam, 1986, pp. 349-360.; J. Goguen, Suggestions for using and organizing libraries in software development, in: S. Kartashev, S. Kartashev (Ed.), Proc. 1st Internat. Conf. on Supercomputing Systems, IEEE Computer Society, 1985. Also in Supercomputing Systems, Steven and Svetlana Kartashev (Eds.), Elsevier, Amsterdam, 1986, pp. 349-360.
[29] J. Goguen, Principles of parameterized programming, in: T. Biggerstaff, A. Perlis (Ed.), Software Reusability, Vol. I: Concepts and Models, Addison-Wesley, Reading, MA, 1989, pp. 159-225.; J. Goguen, Principles of parameterized programming, in: T. Biggerstaff, A. Perlis (Ed.), Software Reusability, Vol. I: Concepts and Models, Addison-Wesley, Reading, MA, 1989, pp. 159-225.
[30] Goguen, J., Higher-order functions considered unnecessary for higher-order programming, (Turner, D., Research Topics in Functional Programming (1990), Addison-Wesley: Addison-Wesley Reading MA), 309-352
[31] J. Goguen, Hyperprogramming: formal approach to software environments, in: Proc. Symp. on Formal Approaches to Software Environment Technology, Joint System Development Corporation, Tokyo, Japan, January 1990.; J. Goguen, Hyperprogramming: formal approach to software environments, in: Proc. Symp. on Formal Approaches to Software Environment Technology, Joint System Development Corporation, Tokyo, Japan, January 1990.
[32] J. Goguen, Types as theories, in: G.M. Reed, A.W. Roscoe, R.F. Wachter (Eds.), Topology and Category Theory in Computer Science, Oxford, 1991, pp. 357-390. Proc. Conf. held at Oxford, June 1989, pp. 357-390.; J. Goguen, Types as theories, in: G.M. Reed, A.W. Roscoe, R.F. Wachter (Eds.), Topology and Category Theory in Computer Science, Oxford, 1991, pp. 357-390. Proc. Conf. held at Oxford, June 1989, pp. 357-390. · Zbl 0792.68100
[33] J. Goguen, An approach to situated adaptive software, in: Proc. Internat. Workshop on New Models of Software Architecture, NEDO, 1993, pp. 7-20.; J. Goguen, An approach to situated adaptive software, in: Proc. Internat. Workshop on New Models of Software Architecture, NEDO, 1993, pp. 7-20.
[34] Goguen, J., Requirements engineering as the reconciliation of social and technical issues, (Jirotka, M.; Goguen, J., Requirements EngineeringSocial and Technical Issues (1994), Academic Press: Academic Press New York), 165-200
[35] J. Goguen, Parameterized programming and software architecture, in: Proc. Reuse’96, IEEE Computer Society, Silver Spring, MD, April 1996, pp. 2-11. Invited keynote address.; J. Goguen, Parameterized programming and software architecture, in: Proc. Reuse’96, IEEE Computer Society, Silver Spring, MD, April 1996, pp. 2-11. Invited keynote address.
[36] J. Goguen, Stretching first order equational logic: proofs with partiality, subtypes and retracts, in: M.P. Bonacina, U. Furbach (Eds.), Proc. Workshop on First Order Theorem Proving, Johannes Kepler Univ. Linz, 1997, pp. 78-85. Schloss Hagenberg, Austria, October 1997; RISC-Linz Report No. 95-50; revised version J. Symbolic Comput., to appear.; J. Goguen, Stretching first order equational logic: proofs with partiality, subtypes and retracts, in: M.P. Bonacina, U. Furbach (Eds.), Proc. Workshop on First Order Theorem Proving, Johannes Kepler Univ. Linz, 1997, pp. 78-85. Schloss Hagenberg, Austria, October 1997; RISC-Linz Report No. 95-50; revised version J. Symbolic Comput., to appear.
[37] J. Goguen, Theorem Proving and Algebra, MIT, Cambridge, MA, to appear.; J. Goguen, Theorem Proving and Algebra, MIT, Cambridge, MA, to appear.
[38] J. Goguen, R. Burstall, CAT, a system for the structured elaboration of correct programs from structured specifications, Technical Report CSL-118, SRI Computer Science Lab, October 1980.; J. Goguen, R. Burstall, CAT, a system for the structured elaboration of correct programs from structured specifications, Technical Report CSL-118, SRI Computer Science Lab, October 1980.
[39] Goguen, J.; Burstall, R., Institutionsabstract model theory for specification and programming, J. Assoc. Comput. Mach., 39, 1, 95-146 (1992) · Zbl 0799.68134
[40] Goguen, J.; Diaconescu, R., An Oxford survey of order sorted algebra, Math. Struct. Comput. Sci., 4, 363-392 (1994) · Zbl 0939.68710
[41] Goguen, J.; Diaconescu, R., Towards an algebraic semantics for the object paradigm, (Ehrig, H.; Orejas, F., Proc. 10th Workshop on Abstract Data Types, Lecture Notes in Computer Science, Vol. 785 (1994), Springer: Springer Berlin), 1-29 · Zbl 0941.68637
[42] Goguen, J.; Malcolm, G., Proof of correctness of object representation, (William Roscoe, A., A Classical MindEssays in Honour of C.A.R. Hoare (1994), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 119-142
[43] J. Goguen, G. Malcolm, Situated adaptive software: beyond the object paradigm, in: Proc. Internat. Symp. on New Models of Software Architecture, Information-Technology Promotion Agency, 1995, pp. 126-142.; J. Goguen, G. Malcolm, Situated adaptive software: beyond the object paradigm, in: Proc. Internat. Symp. on New Models of Software Architecture, Information-Technology Promotion Agency, 1995, pp. 126-142.
[44] Goguen, J.; Malcolm, G., Algebraic Semantics of Imperative Programs (1996), MIT: MIT Cambridge, MA · Zbl 0887.68066
[45] J. Goguen, G. Malcolm, Hidden Coinduction: behavioral correctness proofs for objects, Math. Struct. Comput. Sci. 1999, to appear.; J. Goguen, G. Malcolm, Hidden Coinduction: behavioral correctness proofs for objects, Math. Struct. Comput. Sci. 1999, to appear. · Zbl 0931.68067
[46] J. Goguen, G. Malcolm, More higher order programming in OBJ3, in: J. Goguen, G. Malcolm (Eds.), Software Engineering with OBJ: Algebraic Specification in Action, to appear, Kluwer, Boston, 2000.; J. Goguen, G. Malcolm, More higher order programming in OBJ3, in: J. Goguen, G. Malcolm (Eds.), Software Engineering with OBJ: Algebraic Specification in Action, to appear, Kluwer, Boston, 2000.
[47] Goguen, J.; Malcolm, G.; Kemp, T., A hidden Herbrand theorem, (Palamidessi, C.; Glaser, H.; Meinke, K., Principles of Declarative Programming, Lecture Notes in Computer Science, Vol. 1490 (1998), Springer: Springer Berlin), 445-462 · Zbl 0926.03034
[48] Goguen, J.; Meseguer, J., Universal realization, persistent interconnection and implementation of abstract modules, (Nielsen, M.; Schmidt, E. M., Proc. 9th Internat. Conf. on Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 140 (1982), Springer: Springer Berlin), 265-281 · Zbl 0493.68014
[49] Goguen, J.; Meseguer, J., Completeness of many-sorted equational logic, Houston J. Math., 11, 3, 307-334 (1985) · Zbl 0602.08004
[50] J. Goguen, J. Meseguer, Eqlog: Equality, types, and generic modules for logic programming, in: D. DeGroot, G. Lindstrom (Eds.), Logic Programming: Functions, Relations and Equations, Prentice Hall, Englewood Cliffs, NJ, 1986, pp. 295-363. An earlier version appears in J. Logic Programming, 1(2) (1984) 179-210.; J. Goguen, J. Meseguer, Eqlog: Equality, types, and generic modules for logic programming, in: D. DeGroot, G. Lindstrom (Eds.), Logic Programming: Functions, Relations and Equations, Prentice Hall, Englewood Cliffs, NJ, 1986, pp. 295-363. An earlier version appears in J. Logic Programming, 1(2) (1984) 179-210.
[51] J. Goguen, J. Meseguer, Order-sorted algebra solves the constructor selector, multiple representation and coercion problems, in: Proc. 2nd Symp. on Logic in Computer Science, IEEE Computer Society, Silver Spring, MD, 1987, pp. 18-29.; J. Goguen, J. Meseguer, Order-sorted algebra solves the constructor selector, multiple representation and coercion problems, in: Proc. 2nd Symp. on Logic in Computer Science, IEEE Computer Society, Silver Spring, MD, 1987, pp. 18-29. · Zbl 0796.68144
[52] Goguen, J.; Meseguer, J., Unifying functional, object-oriented and relational programming, with logical semantics, (Shriver, B.; Wegner, P., Research Directions in Object-Oriented Programming (1987), MIT Press: MIT Press Cambridge, MA), 417-477
[53] J. Goguen, J. Meseguer, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoret. Comput. Sci. 105(2) (1992) 217-273. Drafts exists from as early as 1985.; J. Goguen, J. Meseguer, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoret. Comput. Sci. 105(2) (1992) 217-273. Drafts exists from as early as 1985. · Zbl 0778.68056
[54] Goguen, J.; Meseguer, J.; Plaisted, D., Programming with parameterized abstract objects in OBJ, (Ferrari, D.; Bolognani, M.; Goguen, J., Theory and Practice of Software Technology (1983), North-Holland: North-Holland Amsterdam), 163-193
[55] Goguen, J.; Lin, K.; Mori, A.; Roşu, G.; Sato, A., Distributed cooperative formal methods tools, (Lowry, M., Proc. Automated Software Eng. (1997), IEEE: IEEE New York), 55-62
[56] J. Goguen, A. Mori, Semiotics, proofwebs, and distributed cooperative proving, To appear in Proceedings, User Interfaces for Theorem Provers, Sophie-Antipolis, France, 1997.; J. Goguen, A. Mori, Semiotics, proofwebs, and distributed cooperative proving, To appear in Proceedings, User Interfaces for Theorem Provers, Sophie-Antipolis, France, 1997.
[57] Goguen, J.; Socorro, A., Module composition and system design for the object paradigm, J. Object Oriented Programming, 7, 9, 47-55 (1995)
[58] Goguen, J.; Thatcher, J.; Wagner, E., An initial algebra approach to the specification, correctness and implementation of abstract data types, (Yeh, R., Current Trends in Programming Methodology, IV (1978), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 80-149
[59] Goguen, J.; Thatcher, J.; Wagner, E.; Wright, J., Initial algebra semantics and continuous algebras, J. Assoc. Comput. Mach., 24, 1, 68-95 (1977) · Zbl 0359.68018
[60] J. Goguen, W. Tracz, An implementation-oriented semantics for module composition, to appear in G. Leavens and M. Sitaraman (Eds.), Foundations of Component-based Systems, Cambridge University Press, Cambridge, 2000.; J. Goguen, W. Tracz, An implementation-oriented semantics for module composition, to appear in G. Leavens and M. Sitaraman (Eds.), Foundations of Component-based Systems, Cambridge University Press, Cambridge, 2000.
[61] Goguen, J.; Winkler, T.; Meseguer, J.; Futatsugi, K.; Jouannaud, J. P., Introducing OBJ, (Goguen, J.; Malcolm, G., Software Engineering with OBJAlgebraic Specification in Action (2000), Kluwer Academic Publishers: Kluwer Academic Publishers Boston)
[62] R. Goldblatt, Logics of Time and Computation, 2nd ed., CSLI Lecture Notes, Vol. 7, Center for Studies in Language and Information, Stanford University, 1992.; R. Goldblatt, Logics of Time and Computation, 2nd ed., CSLI Lecture Notes, Vol. 7, Center for Studies in Language and Information, Stanford University, 1992. · Zbl 0635.03024
[63] A.D. Gordon, Bisimilarity as a theory of functional programming, Electronic Notes in Theoretical Computer Science, 1, 1995.; A.D. Gordon, Bisimilarity as a theory of functional programming, Electronic Notes in Theoretical Computer Science, 1, 1995. · Zbl 0910.68118
[64] J. Guttag, The specification and application to programming of abstract data types, Ph.D. thesis, Report CSRG-59. Computer Science Department, University of Toronto, 1975.; J. Guttag, The specification and application to programming of abstract data types, Ph.D. thesis, Report CSRG-59. Computer Science Department, University of Toronto, 1975.
[65] Guttag, J., Abstract data types and the development of data structures, Comm. Assoc. Comput. Mach., 20, 297-404 (1977) · Zbl 0356.68022
[66] Hagino, T., A typed lambda calculus with categorical type constructors, (Pitt, D. H.; Poigne, A.; Rydeheard, D. E., Category Theory and Computer Science, Lecture Notes in Computer Science, Vol. 283 (1988), Springer: Springer Berlin), 140-157
[67] L. Hamel, Behavioural verification and implementation of an optimizing compiler for OBJ3, Ph.D. Thesis, Oxford University Computing Lab, 1996.; L. Hamel, Behavioural verification and implementation of an optimizing compiler for OBJ3, Ph.D. Thesis, Oxford University Computing Lab, 1996.
[68] Hennicker, R., Context inductiona proof principle for behavioural abstractions, (Miola, A., Proc. Internat. Symp. on the Design and Implementation of Symbolic Computation Systems, Lecture Notes in Computer Science, vol. 429 (1990), Springer: Springer Berlin), 101-110
[69] Hoare, C. A.R., Proof of correctness of data representation, Acta Inform., 1, 271-281 (1972) · Zbl 0244.68009
[70] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall · Zbl 0637.68007
[71] Jacobs, B., Mongruences and cofree coalgebras, (Nivat, M., Algebraic Methodology and Software Technology (AMAST95), Lecture Notes in Computer Science, Vol. 936 (1995), Springer: Springer Berlin), 245-260 · Zbl 1496.68110
[72] Jacobs, B., Objects and classes, coalgebraically, (Freitag, B.; Jones, C.; Lengauer, C.; Schek, H.-J., Object-Orientation with Parallelism and Persistence (1996), Kluwer: Kluwer Dordrecht), 83-103
[73] B. Jacobs, Invariants, bisimulations and the correctness of coalgebraic refinements, Technical Report CSI-R9704, Computer Science Institute, University of Nijmegen, March 1997.; B. Jacobs, Invariants, bisimulations and the correctness of coalgebraic refinements, Technical Report CSI-R9704, Computer Science Institute, University of Nijmegen, March 1997.
[74] Malcolm, G., Data structures and program transformation, Sci. Comput. Programming, 14, 255-279 (1990) · Zbl 0712.68014
[75] Malcolm, G., Behavioural equivalence, bisimilarity, and minimal realisation, (Haveraaen, M.; Owe, O.; Dahl, O.-J., Recent Trends in Data Type Specifications, Lecture Notes in Computer Science, Vol. 1130 (1996), Springer: Springer Berlin), 359-378
[76] G. Malcolm, J. Goguen, Proving correctness of refinement and implementation, Technical Monograph PRG-114, Programming Research Group, University of Oxford, 1994.; G. Malcolm, J. Goguen, Proving correctness of refinement and implementation, Technical Monograph PRG-114, Programming Research Group, University of Oxford, 1994.
[77] Meseguer, J., Conditional rewriting as a unified model of concurrency, Theoret. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043
[78] J. Meseguer, J. Goguen, Initiality, induction and computability, in: M. Nivat, J. Reynolds (Eds.), Algebraic Methods in Semantics, Cambridge, 1985, pp. 459-541.; J. Meseguer, J. Goguen, Initiality, induction and computability, in: M. Nivat, J. Reynolds (Eds.), Algebraic Methods in Semantics, Cambridge, 1985, pp. 459-541. · Zbl 0571.68004
[79] R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, Parts I and II, Technical Report ECS-LFCS-89-85 and -86, University of Edinburgh, Computer Science Department, 1989.; R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, Parts I and II, Technical Report ECS-LFCS-89-85 and -86, University of Edinburgh, Computer Science Department, 1989. · Zbl 0752.68037
[80] E.F. Moore, Gedanken-experiments on sequential machines, in: Automata Studies, Princeton, University Press, Princeton, 1956, pp. 129-153.; E.F. Moore, Gedanken-experiments on sequential machines, in: Automata Studies, Princeton, University Press, Princeton, 1956, pp. 129-153.
[81] L. Moss, J. Meseguer, J. Goguen, Final algebras, cosemicomputable algebras, and degrees of unsolvability, Theoret. Comput. Sci. 100 (1992) 267-302. Original version from March 1987.; L. Moss, J. Meseguer, J. Goguen, Final algebras, cosemicomputable algebras, and degrees of unsolvability, Theoret. Comput. Sci. 100 (1992) 267-302. Original version from March 1987. · Zbl 0768.68093
[82] F. Orejas, M. Navarro, A. Sánchez, Algebraic implementation of abstract data types: a survey of concepts and new compositionality results, Math. Struct. in Comput. Sci. 6(1) (1996).; F. Orejas, M. Navarro, A. Sánchez, Algebraic implementation of abstract data types: a survey of concepts and new compositionality results, Math. Struct. in Comput. Sci. 6(1) (1996). · Zbl 0846.68070
[83] D. Parnas, Information distribution aspects of design methodology, Inform. Process. ’72, 71 (1972) 339-344. Proc. IFIP Congr., 1972.; D. Parnas, Information distribution aspects of design methodology, Inform. Process. ’72, 71 (1972) 339-344. Proc. IFIP Congr., 1972.
[84] F. Pinheiro, J. Goguen, An object-oriented tool for tracing requirements, IEEE Software \((1996)\); F. Pinheiro, J. Goguen, An object-oriented tool for tracing requirements, IEEE Software \((1996)\)
[85] H. Reichel, Behavioural equivalence — a unifying concept for initial and final specifications, in: Proc. 3rd Hungarian Comput. Sci. Conf., Akademiai Kiado, Budapest, 1981.; H. Reichel, Behavioural equivalence — a unifying concept for initial and final specifications, in: Proc. 3rd Hungarian Comput. Sci. Conf., Akademiai Kiado, Budapest, 1981.
[86] H. Reichel, Behavioural validity of conditional equations in abstract data types, in Contributions to General Algebra 3, Teubner, 1985, pp. 301-324 Proc. Vienna Conf. June 21-24, 1984.; H. Reichel, Behavioural validity of conditional equations in abstract data types, in Contributions to General Algebra 3, Teubner, 1985, pp. 301-324 Proc. Vienna Conf. June 21-24, 1984.
[87] Reichel, H., An approach to object semantics based on terminal co-algebras, Math. Struct. Comput. Sci., 5, 129-152 (1995) · Zbl 0854.18006
[88] G. Roşu, A birkhoff-like axiomatizability result for hidden algebra and coalgebra, in: Proc. 1st Workshop on Coalgebraic Methods in Computer Science (CMCS’98), B. Jacobs, L. Moss, H. Reichel and J. Rutten (Eds.), Lisbon, Portugal, March 1998, Electronic Notes in Theoretical Computer Science, Vol. 11, Elsevier, Amsterdam, 1998.; G. Roşu, A birkhoff-like axiomatizability result for hidden algebra and coalgebra, in: Proc. 1st Workshop on Coalgebraic Methods in Computer Science (CMCS’98), B. Jacobs, L. Moss, H. Reichel and J. Rutten (Eds.), Lisbon, Portugal, March 1998, Electronic Notes in Theoretical Computer Science, Vol. 11, Elsevier, Amsterdam, 1998.
[89] G. Roşu, J. Goguen, Hidden congruent deduction, Ricardo Caferra and Gernot Salzer, editors. In Proceedings, International Workshop on First Order Theorem Proving, Technische Universität Wien, pages 213-223, 1998. Schloss Wilhelminenberg, Vienna, November 23-25, 1998. Also, to appear in Lecture Notes in Artificial Intelligence, Springer, 1999.; G. Roşu, J. Goguen, Hidden congruent deduction, Ricardo Caferra and Gernot Salzer, editors. In Proceedings, International Workshop on First Order Theorem Proving, Technische Universität Wien, pages 213-223, 1998. Schloss Wilhelminenberg, Vienna, November 23-25, 1998. Also, to appear in Lecture Notes in Artificial Intelligence, Springer, 1999.
[90] J. Rutten, Universal coalgebra: a theory of systems, Technical Report CS-R9652, CWI, 1996.; J. Rutten, Universal coalgebra: a theory of systems, Technical Report CS-R9652, CWI, 1996. · Zbl 0951.68038
[91] Rutten, J.; Turi, D., Initial algebra and final coalgebra semantics for concurrency, (de Bakker, J.; Jan Willem de Roever; Rozenberg, G., Proc. REX Symposium ‘A Decade of Concurrency’, Lecture Notes in Computer Science, Vol. 803 (1994), Springer: Springer Berlin), 530-582
[92] Sannella, D.; Tarlecki, A., Toward formal development of programs from algebraic specifications, Acta Inform., 25, 233-281 (1988) · Zbl 0621.68004
[93] A. Socorro, Design, Implementation, and Evaluation of a Declarative Object Oriented Language, Ph.D. Thesis, Programming Research Group, Oxford University, 1994.; A. Socorro, Design, Implementation, and Evaluation of a Declarative Object Oriented Language, Ph.D. Thesis, Programming Research Group, Oxford University, 1994.
[94] J.M. Spivey, Understanding Z. Cambridge, 1988.; J.M. Spivey, Understanding Z. Cambridge, 1988.
[95] W. Tracz, Parameterized programming in LILEANNA; W. Tracz, Parameterized programming in LILEANNA
[96] Turi, D.; Plotkin, G., Towards a mathematical operational semantics, (Proc. Logic in Comput. Sci. (1997), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 280-291
[97] S. Veglioni, Integrating Static and Dynamic Aspects in the Specification of Open, Object-based and Distributed Systems. Ph.D. Thesis, Oxford University Computing Laboratory, 1997.; S. Veglioni, Integrating Static and Dynamic Aspects in the Specification of Open, Object-based and Distributed Systems. Ph.D. Thesis, Oxford University Computing Laboratory, 1997.
[98] van der Waerden, B., A History of Algebra (1985), Springer: Springer Berlin · Zbl 0569.01001
[99] Wand, M., Final algebra semantics and data type extension, J. Comput. System Sci., 19, 27-44 (1979) · Zbl 0418.68020
[100] A.N. Whitehead, A Treatise on Universal Algebra, with Applications, I. Cambridge, 1898. Reprinted 1960.; A.N. Whitehead, A Treatise on Universal Algebra, with Applications, I. Cambridge, 1898. Reprinted 1960.
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.