• Claude Kirchner
  • Hélène Kirchner
  • Aristide Mégrelis
Part of the Advances in Formal Methods book series (ADFM, volume 2)


An interpreter for OBJ3 implemented in Common LISP has been designed using the language OBJ. This formal design is both an effective support of the programming task and a means of communication between different programmers and designers. In the light of this experiment, we propose some extensions to the language and also give a reflexive version of the interpreter.


Software Engineering Formal Design Design Language Exception Handling Error Handling 
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]
    G. Cousineau, P.-L. Curien, and M. Mauny. The categorical abstract machine. In Proceedings 2nd Conference on Functional Programming Languages and Computer Architecture, Nancy (France), volume 201 of Lecture Notes in Computer Science, pages 50–64. Springer-Verlag, 1985.Google Scholar
  2. [2]
    Department of Defense. Reference manual for the ADA programming language. Technical Report ANSI/MIL-STD-1815A, United States Government, 1980.Google Scholar
  3. [3]
    N. Dershowitz. Termination. In Proceedings 1st Conference on Rewriting Techniques and Applications, Dijon (France),volume 202 of Lecture Notes in Computer Science,pages 180–224, Dijon (France), May 1985. Springer-Verlag.Google Scholar
  4. [4]
    K. Futatsugi, J. A. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ-2. In B. Reid, editor, Proceedings 12th ACM Symp. on Principles of Programming Languages, pages 52–66. ACM, 1985.Google Scholar
  5. [5]
    I. Gnaedig. ELIOS-OBJ: Theorem proving in a specification language. In B. Krieg-Bruckner, editor, Proceedings of the 4th European Symposium on Programming, volume 582 of Lecture Notes in Computer Science, pages 182–199. Springer-Verlag, February 1992.Google Scholar
  6. [6]
    J. A. Goguen. Some design principles and theory for OBJ-0, a language for expressing and executing algebraic specifications of programs. In Proceedings of International Conference on Mathematical Studies of Information Processing, pages 429–475. IFIP Working Group 2. 2, Kyoto, Japan, 1978.Google Scholar
  7. [7]
    J. A. Goguen, Claude Kirchner, Hélène Kirchner, A. Mégrelis, J. Meseguer, and T. Winkler. An introduction to OBJ-3. In J.-P. Jouannaud and S. Kaplan, editors, Proceedings 1st International Workshop on Conditional Term Rewriting Systems, Orsay (France),volume 308 of Lecture Notes in Computer Science,pages 258–263. Springer-Verlag, July 1987. Also as internal report CRIN: 88-R-001.Google Scholar
  8. [8]
    J. A. Goguen, Claude Kirchner, and J. Meseguer. Concurrent term rewriting as a model of computation. In R. Keller and J. Fasel, editors, Proceedings of Graph Reduction Workshop, volume 279 of Lecture Notes in Computer Science, pages 53–93, Santa Fe (NM, USA), 1987. Springer-Verlag.Google Scholar
  9. [9]
    J. A. Goguen, J. Meseguer, and D. Plaisted. Programming with parameterized abstract objects in OBJ. Theory And Practice of Software Technology, pages 163–193, 1982.Google Scholar
  10. [10]
    J. A. Goguen and J. Tardo. An introduction to OBJ: A language for writing and testing software specifications. In M. K. Zelkowitz, editor, Specification of Reliable Softwarepages 170–189. IEEE Press, Cambridge (MA, USA), 1979. Reprinted in Software Specification TechniquesN. Gehani and A. McGettrick, editors, Addison-Wesley, 1985, pages 391–420. Google Scholar
  11. [11]
    J. A. Goguen and T. Winkler. Introducing OBJ3. Technical Report SRICSL-88–9, SRI International, 333, Ravenswood Ave., Menlo Park, CA 94025, August 1988.Google Scholar
  12. [12]
    Joseph Goguen, Andrews Stevens, Keith Hobley, and Hendrick Hilberdink. 2OBJ, a metalogical framework based on equational logic. Philosophical Transactions of the Royal Society, Series A, (339): 69–86, 1992.Google Scholar
  13. [13]
    Joseph A. Goguen and José Meseguer. Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 2 (105): 217–273, 1992.MathSciNetCrossRefGoogle Scholar
  14. [14]
    J.-P. Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing,15(4):1155–1194,1986. Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City (USA), 1984.Google Scholar
  15. [15]
    Claude Kirchner, Hélène Kirchner, and J. Meseguer. Operational semantics of OBJ-3. In Proceedings of 15th International Colloquium on Automata, Languages and Programming, volume 317 of Lecture Notes in Computer Science, pages 287–301. Springer-Verlag, 1988.Google Scholar
  16. [16]
    Claude Kirchner, Hélène Kirchner, and M. Vittek. Designing constraint logic programming languages using computational systems. In P. Van Hentenryck and V. Saraswat, editors, Principles and Practice of Constraint Programming. The Newport Papers., pages 131–158. The MIT press, 1995.Google Scholar
  17. [17]
    Donald E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, 1970.Google Scholar
  18. [18]
    B. H. Liskov, R. Atkinson, T. Bloom, E. Moss, J. Schaffert, B. Scheifler, and A. Snyder. CLU Reference Manual, volume 114 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1981.Google Scholar
  19. [19]
    J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96 (1): 73–155, 1992.MathSciNetzbMATHCrossRefGoogle Scholar
  20. [20]
    G. L. Steele. Common Lisp: The Language. Digital Press, 1984.Google Scholar
  21. [21]
    J. Tardo. The Design, Specification and Implementation of OBJT: A Language for Writing and Testing Abstract Algebraic Program Specifications. PhD thesis, UCLA, Computer Science Department, 1981.Google Scholar

Copyright information

© Springer Science+Business Media New York 2000

Authors and Affiliations

  • Claude Kirchner
    • 1
  • Hélène Kirchner
    • 1
  • Aristide Mégrelis
    • 2
  1. 1.INRIA Lorraine & CRINFrance
  2. 2.INRIA Lorraine & CRINVillers-lès-Nancy CedexFrance

Personalised recommendations