@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Name: OBJ3 Keywords: order-sorted equational logic, parameterized modules, rewriting Description: Semantics: the underlying logic, order-sorted equational logic Deductive machinery: reduction or controlled deduction; proofs are scripts and are not manipulatable objects Dynamics: modules are collections of equational assertions, new modules can be defined, assertions can be temporarily added to a module Persistence: limited capacity to save state OBJ3 is based on order-sorted equational logic. Organized in modules, which may be parameterized. object modules encapsulate executable code, have inital semantics theory modules specify syntax and semantics of modules and module interfaces Computation/deduction is via rewriting modulo associative, commutative, and/or identity equations. The following paper gives a number of results and applies them to show how many proving problems in first and higher-order logic can be systematically reduced to equational problems that can be solved by the OBJ rewriting facility. Joseph A. Goguen OBJ as a Theorem Prover with Hardware Verification Applications SRI International Technical Report SRI-CSL-88-4R2, 1988. Contact persons: kiniry@acm.org goguen@cs.ucsd.edu User group: OBJ3 has been distributed to over 100 research sites all over the world; other versions of OBJ also exist in North America, Europe, and Japan. Pragmatics: Clear simple mathematical semantics; modularity and flexibility; flexible approach to syntax; relatively small implementation; easy to extend and to build other systems on top of. Documentation: Primary documentation on OBJ3: "Introducing OBJ", J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud. In _Software Engineering with OBJ: Algebraic Specification in Action_, Kluwer, 2000. Also Computer Science Laboratory Technical Report SRI-CSL-88-9, 1988. Mathematical Semantics: Order-sorted Algebra I, J. Goguen and Jose Meseguer, Technical Report SRI-CSL-89-10, SRI International, Computer Science Lab, July 1989. More on operational Semantics: "Operational Semantics of OBJ3", Claude Kirchner, Helene Kirchner, and Jose Meseguer. In Proceedings, 15th Intl. Coll. on Automata, Languages and Programming, Tampere, Finland, July 11-15, 1988, editors Lepisto and A. Salomaa, Springer-Verlag, Lecture Notes in Computer Science Number 317, pp. 287-301, 1988. Theorem Proving Applications: "Proving and rewriting", Joseph Goguen. In Proceedings, Second International Conference on Algebraic and Logic Programming, pages 1--24. Springer, 1990. Lecture Notes in Computer Science, Volume 463. also, see above mentioned paper "OBJ as a Theorem Prover with Hardware Verification Applications" A full bibliography for OBJ is available at http://www.kindsoftware.com/products/opensource/OBJ3/docs/obj_bib.html Extensions/enhancements: In the context of theorem proving and specification, OBJ3 was used as the basis for implementing the following systems. See http://www.kindsoftware.com/products/opensource/OBJ3/faq.html for more information on all of them. Eqlog: A logic programming language, implemented by enriching OBJ3 with order sorted unification and backtracking. FOOPS: a declarative object oriented language built on top of OBJ3. Kumo: a proof assistant for first order hidden logic, that also generates websites that document its proofs. OOZE: An Object-Oriented Z Environment. TOOR: a requirements management system built on top of FOOPS. TRIM: an optimizing compiler for OBJ, proved correct using hidden algebra. 2OBJ: a meta-logical framework based on equational logic. KTT: a logic for capturing reusable knowledge. In addition, OBJ has been used as the functional sublanguage of several language definitions extending OBJ to: logic programming (Eqlog: Equality, types, and generic modules for logic programming, Joseph Goguen and Jose Meseguer, In Douglas DeGroot and Gary Lindstrom, editors, Logic Programming: Functions, Relations and Equations, pages 295-363 Prentice-Hall, 1986); object-oriented programming (Unifying functional, object-oriented and relational programming, with logical semantics, Joseph Goguen and Jose Meseguer, In Bruce Shriver and Peter Wegner, editors, Research Directions in Object-Oriented Programming, pages 417-477, MIT, 1987); and concurrent programming--including object-oriented programming--Parallel Programming in Maude, J. Meseguer and T. Winkler, In J.-P Banatre and D. Le Metayer, editors, Research Directions in High-level Parallel Programming Languages, pages 253-293, Springer-Verlag Lecture Notes in Computer Science 574, 1991). Resource requirements: implementation language: Common Lisp environment support required: GCL 2.2.2 through 2.4 Where-to-get-it: The full OBJ3 system is available from KindSoftware: http://www.kindsoftware.com/products/opensource/OBJ3/ Recent distributions include some of the aforementioned extensions. [Info source/date] Joseph Kiniry, December, 2001 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%