Programming in OBJ and Maude

  • Tim Winkler
Part of the Lecture Notes in Computer Science book series (LNCS, volume 693)


This is a introduction to the gentle art of programming in OBJ and Maude. The features of OBJ that are highlighted are its logic— ordersorted equational logic— connections of this logic with unsorted first-order equational logic, newer features of the language, and parameterized programming. The language Maude— which contains OBJ as its functional sublanguage and extends OBJ to include object-oriented programming and concurrent systems programming— is briefly introduced with a focus on its logic and some simple examples.


Operational Semantic Deductive System Equational Logic Equational Reasoning Structural Axiom 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Hitoshi Aida, Joseph Goguen, and José Meseguer. Compiling concurrent rewriting onto the rewrite rule machine. In S. Kaplan and M. Okada, editors, Conditional and Typed Rewriting Systems, Montreal, Canada, June 1990, pages 320–332. Springer LNCS 516, 1991.Google Scholar
  2. 2.
    Hitoshi Aida, Sany Leinwand, and José Meseguer. Architectural design of the rewrite rule machine ensemble. To appear in J. Delgado-Frias and W.R. More, editors, Proc. Workshop on VLSI for Artificial Intelligence and Neural Networks, Oxford, September 1990; also, Tech. Report SRI-CSL-90-17, December 1990.Google Scholar
  3. 3.
    K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.Google Scholar
  4. 4.
    A. A. Faustini and R. Jagannathan. Indexical lucid. In R. Jagannathan, editor, Proceedings, 4th International Symposium on Lucid and Intensional Programming, pages 19–34. SRI International, 1991.Google Scholar
  5. 5.
    J.A. Goguen, S. Leinwand, J. Meseguer, and T. Winkler. The rewrite rule machine, 1988. Technical Report PRG-76, Oxford University, Programming Research Group, 1989.Google Scholar
  6. 6.
    J.A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud. Introducing OBJ. Technical report, Computer Science Lab, SRI International, 1992. To appear in J.A. Goguen, D. Coleman and R. Gallimore, editors, Applications of Algebraic Specification Using OBJ, Cambridge University Press.Google Scholar
  7. 7.
    Joseph Goguen. Higher-order functions considered unnecessary for higher-order programming. In David Turner, editor, Proc, University of Texas Year of Programming, Institute on Declarative Programming. Addison-Wesley, 1988. Preliminary version as SRI Tech. Rep. SRI-CSL-88-1, January 1988.Google Scholar
  8. 8.
    Joseph Goguen. OBJ as a theorem prover with application to hardware verification. In P.S. Subramanyam and G. Birtwistle, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 218–267. Springer-Verlag, 1989.Google Scholar
  9. 9.
    Joseph Goguen. Principles of parameterized programming. In Ted Biggerstaff and Alan Perlis, editors, Software Reusability, Volume I: Concepts and Models, pages 159–225. Addison-Wesley, 1989.Google Scholar
  10. 10.
    Joseph Goguen and José Meseguer. Equality, types, modules and generics for logic programming. In S.-A. Tärnlund, editor, Proc. 2nd Intl. Logic Programming Conf., Uppsala, July 2–6, 1984, pages 115–125. Uppsala University, 1984.Google Scholar
  11. 11.
    Joseph Goguen and José Meseguer. Completeness of many-sorted equational logic. Houston Journal of Mathematics, 11(3):307–334, 1985. Preliminary versions have appeared in: SIGPLAN Notices, July 1981, Volume 16, Number 7, pages 24–37; SRI Computer Science Lab Technical Report CSL-135, May 1982; and Report CSLI-84-15, Center for the Study of Language and Information, Stanford University, September 1984.Google Scholar
  12. 12.
    Joseph Goguen and José Meseguer. Eqlog: Equality, types, and generic modules for logic programming. In Douglas DeGroot and Gary Lindstrom, editors, Logic Programming: Functions, Relations and Equations, pages 295–363. Prentice-Hall, 1986. An earlier version appears in Journal of Logic Programming, Volume 1, Number 2, pages 179–210, September 1984.Google Scholar
  13. 13.
    Joseph Goguen and José Meseguer. Models and equality for logical programming. In Hartmut Ehrig, Giorgio Levi, Robert Kowalski, and Ugo Montanari, editors, Proceedings, 1987 TAPSOFT, pages 1–22. Springer-Verlag, 1987. Lecture Notes in Computer Science, Volume 250; extended version to appear in J. Logic Programming.Google Scholar
  14. 14.
    Joseph Goguen and José Meseguer. Software for the rewrite rule machine. In Proceedings of the International Conference on Fifth Generation Computer Systems, Tokyo, Japan, pages 628–637. ICOT, 1988.Google Scholar
  15. 15.
    Joseph Goguen and José Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Technical Report SRI-CSL-89-10, SRI International, Computer Science Lab, July 1989.Google Scholar
  16. 16.
    Joseph Goguen, Andrew Stevens, Keith Hobley, and Hendrik Hilberdink. 2OBJ, a meta-logical framework based on equational logic, 1991. To appear, Philosophical Transactions of the Royal Society.Google Scholar
  17. 17.
    Joseph Goguen, James Thatcher, and Eric Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. Technical Report RC 6487, IBM T. J. Watson Research Center, October 1976. Appears in Current Trends in Programming Methodology, IV, Raymond Yeh, Ed., Prentice-Hall, 1978, pages 80–149.Google Scholar
  18. 18.
    Joseph Goguen, James Thatcher, Eric Wagner, and Jesse Wright. Initial algebra semantics and continuous algebras. Journal of the Association for Computing Machinery, 24(1):68–95, January 1977.Google Scholar
  19. 19.
    Joseph Goguen and Timothy Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI International, Computer Science Lab, August 1988. Revised version to appear with additional authors José Meseguer, Kokichi Futatsugi and Jean-Pierre Jouannaud, in Applications of Algebraic Specification using OBJ, edited by Joseph Goguen, Derek Coleman and Robin Gallimore, Cambridge, 1992.Google Scholar
  20. 20.
    Joseph A. Goguen. Proving and rewriting. In Proc. Conf. on Algebraic and Logic Programming, Nancy, Springer LNCS 463, 1990.Google Scholar
  21. 21.
    Leon Henkin. On mathematical induction. American Mathematical Monthly, 67:323–338, 1960.Google Scholar
  22. 22.
    Leon Henkin. The logic of equality. American Mathematical Monthly, 84:597–612, 1977.Google Scholar
  23. 23.
    Jieh Hsiang. Refutational Theorem Proving using Term Rewriting Systems. PhD thesis, Univeristy of Illinois at Champaign-Urbana, 1981.Google Scholar
  24. 24.
    Claude Kirchner, Hélène Kirchner, and José Meseguer. Operational semantics of OBJ3. In T. Lepistö and A. Salomaa, editors, Proceedings, 15th Intl. Coll. on Automata, Languages and Programming, Tampere, Finland, July 11–15, 1988, pages 287–301. Springer-Verlag, Lecture Notes in Computer Science No. 317, 1988.Google Scholar
  25. 25.
    S. Leinwand, J.A. Goguen, and T. Winkler. Cell and ensemble architecture for the rewrite rule machine. In Proceedings of the International Conference on Fifth Generation Computer Systems, Tokyo, Japan, pages 869–878. ICOT, 1988.Google Scholar
  26. 26.
    V. Manca, A. Salibra, and G. Scollo. Equational type logic. Theoretical Computer Science, 77:131–159, 1990.Google Scholar
  27. 27.
    Alain J. Martin. The limitations to delay-insensitivity in asynchronous circuits. In William J. Dally, editor, Advanced research in VLSI: proceedings of the sixth MIT conference, pages 263–278. MIT Press, 1990.Google Scholar
  28. 28.
    J. Meseguer and T. Winkler. Parallel Programming in Maude. In J.-P Banâtre and D. Le Mètayer, editors, Research Directions in High-level Parallel Programming Languages, pages 253–293. Springer-Verlag, 1992. Lecture Notes in Computer Science, Volume 574; also, SRI Technical Report SRI-CSL-91-08, November 1991.Google Scholar
  29. 29.
    José Meseguer. A logical theory of concurrent objects. In ECOOP-OOPSLA'90 Conference on Object-Oriented Programming, Ottawa, Canada, October 1990, pages 101–115. ACM, 1990.Google Scholar
  30. 30.
    José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992. also, SRI International, Computer Science Laboratory technical report SRI-CSL-91-05, February, 1991.Google Scholar
  31. 31.
    José Meseguer and Joseph Goguen. Initiality, induction and computability. In Maurice Nivat and John Reynolds, editors, Algebraic Methods in Semantics, pages 459–541. Cambridge University Press, 1985.Google Scholar
  32. 32.
    J. Donald Monk. Mathematical Logic. Springer-Verlag, 1976.Google Scholar
  33. 33.
    Werner Nutt, Pierre Réty, and Gert Smolka. Basic narrowing revisited. J. Symbolic Computation, 7:295–317, 1989.Google Scholar
  34. 34.
    Axel Poigné. Once more on order-sorted algebras. In A. Tarlecki, editor, Proceedings, Mathematical Foundations of Computer Science, pages 397–405. Springer-Verlag, 1991. Lecture Notes in Computer Science, Volume 520.Google Scholar
  35. 35.
    Gert Smolka, Werner Nutt, Joseph Goguen, and José Meseguer. Order-sorted equational computation. In Maurice Nivat and Hassan Aït-Kaci, editors, Resolution of Equations in Algebraic Structures, volume 2, pages 297–367. Academic Press, 1989.Google Scholar
  36. 36.
    Raymond M. Smullyan. First-Order Logic. Springer-Verlag, 1968. Ergebnisse der Mathematik und ihrer Grenzgebiete, Band 43.Google Scholar
  37. 37.
    W. W. Wadge and E. A. Ashcroft. Lucid, the Dataflow Programming Language. Academic Press, 1985.Google Scholar
  38. 38.
    Timothy Winkler, Sany Leinwand, and Joseph Goguen. Simulation of concurrent term rewriting. In Steven Kartashev and Svetlana Kartashev, editors, Proceedings, Second International Supercomputing Conference, Volume I, pages 199–208. International Supercomputing Institute, Inc., 1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Tim Winkler
    • 1
  1. 1.SRI InternationalMenlo ParkUSA

Personalised recommendations