@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%