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.


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


Full Text: DOI


[1] Abramsky, S., Interaction categories and communicating sequential processes, (), 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.
[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.
[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 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.
[10] Burstall, R.; Diaconescu, R., Hiding and behaviouran institutional approach, (), 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.
[12] Button, G.; Sharrock, W., Occasioned practises in the work of implementing development methodlogies, (), 217-240
[13] 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.
[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.
[16] 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, (), 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. · Zbl 0912.68092
[19] 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.
[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. · 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.
[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. · 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.
[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.
[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.
[30] Goguen, J., Higher-order functions considered unnecessary for higher-order programming, (), 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.
[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. · 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.
[34] Goguen, J., Requirements engineering as the reconciliation of social and technical issues, (), 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.
[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.
[37] 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.
[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, (), 1-29 · Zbl 0941.68637
[42] Goguen, J.; Malcolm, G., Proof of correctness of object representation, (), 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.
[44] Goguen, J.; Malcolm, G., Algebraic semantics of imperative programs, (1996), 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. · 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.
[47] Goguen, J.; Malcolm, G.; Kemp, T., A hidden Herbrand theorem, (), 445-462 · Zbl 0926.03034
[48] Goguen, J.; Meseguer, J., Universal realization, persistent interconnection and implementation of abstract modules, (), 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.
[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. · Zbl 0796.68144
[52] Goguen, J.; Meseguer, J., Unifying functional, object-oriented and relational programming, with logical semantics, (), 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. · Zbl 0778.68056
[54] Goguen, J.; Meseguer, J.; Plaisted, D., Programming with parameterized abstract objects in OBJ, (), 163-193
[55] Goguen, J.; Lin, K.; Mori, A.; Roşu, G.; Sato, A., Distributed cooperative formal methods tools, (), 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.
[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, (), 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.
[61] Goguen, J.; Winkler, T.; Meseguer, J.; Futatsugi, K.; Jouannaud, J.P., Introducing OBJ, ()
[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. · Zbl 0635.03024
[63] 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.
[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, (), 140-157
[67] 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, (), 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, (), 245-260
[72] Jacobs, B., Objects and classes, coalgebraically, (), 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.
[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, (), 359-378
[76] 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. · 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. · Zbl 0752.68037
[80] 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. · 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). · Zbl 0846.68070
[83] 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)\) 52-64. Special issue of papers from ICRE ’96.
[85] 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.
[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.
[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.
[90] 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, (), 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.
[94] J.M. Spivey, Understanding Z. Cambridge, 1988.
[95] W. Tracz, Parameterized programming in {\scLILEANNA}, in: Proc., 2nd Internat. Workshop on Software Reuse, Lucca, Italy, March 1993.
[96] Turi, D.; Plotkin, G., Towards a mathematical operational semantics, (), 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.
[98] van der Waerden, B., A history of algebra, (1985), 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.
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.