OBJ3 Release 2.0

OBJ embodies basic design choices that are quite different from those
of other programming languages, even other functional programming
languages.  

OBJ3 is the latest in a series of systems consisting of an interpreter
and an environment, having the following properties:


  1.OBJ3 is logical in the sense that there is a logical system L such that

      o statements in OBJ3 programs are sentences in L,
      o the denotational semantics of an OBJ3 program P is:

          - an initial model of P, if P is an "object" (i.e. has
initial semantics; and
          - the "variety" of models of P, if P is a "theory" (i.e. has
loose semantics).
      o operational semantics is given by (efficient) deduction in L.

  2.OBJ3 has parameterized programming, which supports very flexible
program reuse and program structuring, giving the expressive power of
higher order programming using only a first order logic, through the
following features: 

      o objects which contain executable code, and theories which
define properties; 
      o parameterized modules, with theories to define interfaces;
      o views to define instantiation (binding) of generic modules and
to assert properties of modules, and
      o module expressions, which describe complex (sub)system as
interconnection of given modules (possibly parameterized), and then
actually construct them when evaluated.

  3.OBJ3 is based on order sorted equational logic, which provides a
rigorous basis for

      o user-definable subtypes
      o exception handling
      o multiple inheritance
      o operation overloading and
      o retracts a form of run time type checking that supports a
strong typing which is as flexible as weak typing.

  4.OBJ3 has user-definable evaluation strategies, which

      o can be eager, lazy, or more exotic combinations,
      o are user definable for each operation separately (rather than
globally), and 
      o are computed by default (using strictness analysis) if not
given explicitly. 

  5.OBJ3 has pattern matching modulo associativity and/or
commutativity, and identity by completion. (New: the system
automatically computes conditions for rules that are used to prevent
obvious non-termination problems.) 
  6.New: version 2 of OBJ3 has a facility for controlled rewriting.
This provides substantially increased support for the use of the
system for equational theorem proving. 


OBJ3 also has some features that are unusual but not unique, including


  1.user definable mixfix syntax, with precedence,
  2.user-optional memoisation on an operation-by-operation basis,
  3.user-definable built-in modules for efficient implementation of
basic abstract data types, such as numbers and characters, and
  4.module import hierarchies.


OBJ3 has been successfully used for a variety of applications,
including research and teaching in software design, software
specification, rapid prototyping, theorem proving, hardware
verification, and functional programming.

Improvements in this version include some language extensions and
additional theorem proving features. In addition, an effort has been
made to speed up the implementation; rewriting is often twice as fast
as in the orginal implementation. We have also decided to include the
AKCL patches from the University Texas at Austin in the distribution,
which are necessary for maintaining the portability of OBJ3 and also
improve its efficiency. In addition, we will be distributing a SPARC
version of OBJ3. 

OBJ3 is written in Austin Kyoto Common Lisp (AKCL) and has been
compiled on Sun 3's, SPARCs, Dec3100s, and VAXes; it is relatively
portable and can probably be complied on other machines with 
a Common Lisp compiler. We can provide an executable form of OBJ3 for
SPARCs, which occupies about 5.9 Mbytes of disk space. If you build
OBJ3 from sources, you will need about 1.1 Mbyte disk space for the
sources and up to 10 Mbyte for the construction. You will not need a
license for KCL or AKCL. AKCL needs 7 Mbytes for its sources, 16
Mbytes for construction, and its executable occupies about 2.7
Mbytes. Our distribution media are 1/4 inch cartridges or 8mm
cartridges. Some examples are included on the tape.


Jos'e Meseguer and Patrick Lincoln       Joseph A. Goguen
Computer Science Laboratory              Programming Research Group
SRI International                        Computing Laboratory, Oxford University
333 Ravenswood Ave.                    11 Keble Road
Menlo Park, CA 94025, USA               Oxford OX1 3QD, UK

If you wish to receive an OBJ3 distribution tape, please fill out the
OBJ3 Information Form, have the cognizant authority at your
institution fill out and sign OBJ3 license agreement and send these to
the address given on the form. Our shipment will include the tape, the
executed OBJ3 license, an invoice for $150.00 plus any required taxes,
and some documentation.  If you already have an OBJ3 license, you will
not need a new one, but we are still requesting that you pay the
distribution fee. 

To obtain forms through ftp:

ftp ftp.csl.sri.com
login: anonymous
password: your net address
cd pub/rewriting
get license.dvi and info-form.dvi quit

or through World Wide Web:

http://www.csl.sri.com/rewriting/license.dvi
http://www.csl.sri.com/rewriting/info-form.dvi

or directly through mail or fax:

Judith Burgess
burgess@csl.sri.com, Phone: 1-415/859-5924, fax: 1-415/859-2844.