kind rel="help" href="https://www.kindsoftware.com/about/" title="Site Information" />

OBJ3 FAQ

If you have any questions that you'd like added to this FAQ, please email your suggestions to kiniry@acm.org. Thanks!

  1. What is OBJ3?

    From the OBJ3 release:

    "OBJ" refers to the language family, while "OBJ2", "OBJ3", "CafeOBJ", "BOBJ" etc. refer to particular members. The OBJ languages are broad spectrum algebraic programming and specification languages, based on order sorted equational logic, generally enriched with some other logic, such as rewriting logic or hidden equational logic.

    All the OBJ languages are rigorously based upon a logical system; more precisely, they are logical languages, in the sense that their programs are sets of sentences in some logical system, and their operational semantics is given by deduction in that logical system. All recent OBJ languages use order sorted algebra, which also provides a rigorous basis for user definable sub-types, exception handling, multiple inheritance, overloading, multiple representations, coercions, and more. All recent OBJ languages provide parameterized programming, with parameterized modules, module instantiation, views, module expressions, etc., to support very flexible program structuring and reuse. In general, they also support user definable mixfix syntax, user definable execution strategies, rewriting modulo standard equational theories (associative, commutative, etc.), and selective memoization.

    OBJ3 is based on order sorted equational logic, and has been successfully used for research and teaching in software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among other things. It was the first language to implement parameterized programming and its module system influenced the designs of the Ada, C++ and ML module systems.

  2. Where did the name "OBJ3" come from?

    OBJ3 is the third of a series of implementations of the same basic ideas; "OBJ" is not an acronym, but rather is a contraction from "object," since the intent from the beginning was to capture the ideas that later turned out, by some strange coincidence, to be called "object oriented."

  3. What is the OBJ3 license like?

    OBJ3 was originally distributed from SRI International, and later from Oxford, and then UCSD. Originally a license from SRI was required to obtain the OBJ3 source code, but this is no longer the case. This new version of OBJ3 (2.06 onward) is released under a BSD-like license.

  4. What is the history of OBJ3?

    The first implementation of initial algebra semantics via term rewriting appeared in the earliest versions of OBJ, from the mid 1970s. The characteristic OBJ syntax first appeared in the paper Abstract Errors for Abstract Data Type, by Joseph Goguen in 1977. The idea of using term rewriting to implement initial algebra semantics evolved out of work done in the ADJ group in the early 1970s. The OBJ module system ideas are a further development of ideas pioneered in the Clear language, in joint work of Joseph Goguen and Rod Burstall in the 1970s. Most of the programming for OBJ3 was done by Timothy Winkler, first at SRI International, and then later at Oxford; several small enhancements and some bug fixes were later done by students at Oxford and UCSD, the last of which appear in version 2.04. Then, Joe Kiniry stepped in and created a modern open source release, which began with version 2.05. Lutz Hamel graciously integrated his TRIM system, resulting in version 2.08.

  5. How do I get the source for OBJ3 or pre-built executables?

    You can download the latest OBJ3 source code and via the OBJ3 release home page, or one of its mirrors. We do not currently provide pre-built executables for OBJ3. Development of OBJ3 is hosted at GitHub.

  6. Are previous versions of OBJ3 available?

    A snapshot of OBJ3 version 2.04 is available via our archives. It includes a SPARC SunOS 4.x executable, but does not contain much coherent documentation.

  7. How can I contribute?
    • OBJ3 is not under active development at this time.
    • A branch of OBJ3, called OBJ4, might become available from Sula Ma at Oxford. Please do not email Sula about OBJ3.
    • BOBJ is now available from the Meaning and Computation Lab in the UCSD Dept. of Computer Science and Engineering. BOBJ is written in Java, thus runs on numerous platforms. Once a stable release has been achieved, additional developers and maintainers would be welcome. This system should eventually be fully upward compatible with OBJ3, with considerable additional support for behavioral specification, computation, and verification.
  8. What tools are used to develop OBJ3?

    This release of OBJ3 was built using GNU Common Lisp 2.6.3 (ANSI), CMU Common Lisp 19a+, Steel Bank Common Lisp 0.8.16, CLISP 2.33.2, GCC 3.3, and FSF Emacs versions 21.2.1 and 21.3.50 using SLIME version 1.0. We have built this release on a Linux Fedora Core 3 (kernel version 2.6.10, glibc version X) system on the x86 architecture and on a Mac OS X 10.3 system.

  9. What is the primary documentation on OBJ3?

    We suggest you read the following documents, in order, to learn more about OBJ3:

    And, for those interested in the extending OBJ3:

    Many other OBJ-related documents are referenced in the included OBJ bibliography.

  10. If I want to learn about (OBJ3 | rewriting systems | (Many) Order Sorted Algebra | Hidden Algebra), where should I look?

    The first place to look is Joseph Goguen's OBJ home page, from which many other references can be found. In particular, see [Goguen78, GoguenDiaconescu94, GoguenMeseguer89] , and any of the GoguenMalcolm papers on Hidden Algebra (particularly [GoguenMalcolm97] for an excellent though outdated review); the latest paper is Circular Coinductive Rewriting, by Joseph Goguen, Kai Lin and Grigore Rosu.

  11. Which Lisp interpreters can I use to build/use OBJ3?

    Currently, GCL and CMU Common Lisp are supported. OBJ3 has been built successfully in the past with AKCL and Lucid CL as well. We are currently working on building OBJ3 on CLISP and SBCL. We would like to try building on Allegro CL as well, but Allegro's policies and licensing prohibit such. We suggest you email Allegro and express your discontent with the current state of affairs.

  12. What systems have been built on top of OBJ3?

    A partial (alphabetical) list includes the following:

    Joseph Kiniry is compiling several of these packages into a new, supported software release.

  13. What systems/models/theories have been influenced by OBJ?

    A partial list includes the following:

    • CafeOBJ - CafeOBJ is a new generation algebraic specification language being developed in Japan with support from MITI through IPA (Japan). The CafeOBJ team is lead by Prof Prof. Kokichi Futatsugi, at JAIST (Japan), who is one of the original developers of OBJ2. CafeOBJ preserves the distinctive useful features of OBJ3, including mix-fix syntax, subtyping by ordered sorts, modules with parameterized programming, and it adds new logics and features to handle the object paradigm, including hidden algebra and rewriting logic, and their combinations with order sorted algebra. This multi-paradigm approach has an elegant mathematical semantics based on multiple institutions, due to Razvan Diaconescu. Some theorem proving capabilities are also supported.
    • OBJ is used in the Tatami project, which is developing the Kumo proof assistant and proof website generator. The project is now preparing Kumo to use the BOBJ system.
    • Maude - Maude incorporates most features of OBJ3, sometimes with small syntactic changes, and adds an implementation of rewriting logic, using a new and more powerful rewriting engine, and using the membership equational logic generalization of order sorted equational logic. The Computer Science Lab at SRI International has a Maude homepage; see also the SRI CSL rewriting logic homepage. Maude is particularly good for applications that involve logical reflection and meta-logical programming.
    • The module systems of Ada, ML, C++ and Lotos have all been influenced by the OBJ module system; Lotos also uses the initial algebra semantics that was pioneered by OBJ.

  14. What is the state of research in Hidden Algebra?

    Hidden algebra and its implementation technology are evolving rapidly at this time. For the latest information on this and related topics, check Joseph Goguen's "What's New" link at the top of his homepage, and/or browse through his rather extended website. Kumo is a major focus for current research in the "Tatami" project.

  15. What is the future of OBJ3?

    OBJ or its derivatives are currently being used for a number of active research projects including (partial list):

    • The above mentioned related projects: CafeOBJ, Tatami, and Kumo.
    • BOBJ is expected to become the next generation system used at UCSD, since it should eventually be fully upward compatible with OBJ3, it supports the most recent ideas in behavioral specification, computation, and verification, and it will be integrated with Kumo.