OBJ3 Summary

"OBJ" refers to the language family, while "OBJ2", "OBJ3", "CafeOBJ", etc. refer to particular members. The OBJ languages are broad spectrum algebraic programming and specification languages, based on order sorted equational logic, possibly enriched with other logics, 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. They also support user definable mixfix syntax, user definable execution strategies, rewriting modulo standard equational theories (associative, commutative, etc.), and selective memoization.

All recent OBJ languages provide parameterized programming, with parameterized modules, module instantiation, views, module expressions, etc., to support very flexible program structuring and reuse.

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.

This is OBJ3 version 2.10, an evolution of a cleaned-up release of OBJ3 2.04 from 1992. This version is pre-built for Fedora Core 3 on the x86 architecture and for Mac OS X 10.3.

The TRIM compiler system by Lutz Hamel is included with OBJ3. He kindly integrated the TRIM system into our OBJ3 2.06 release - thanks Lutz! The original 2.05 update was engineered by Sula Ma. All later updates were engineered by Joseph Kiniry.

This release was built and is supported by Joseph Kiniry and runs under GNU Common Lisp, CMU Common Lisp, Steel Bank Common Lisp, and CLISP on ix86/Linux and PPC/Darwin (Mac OS X).