OBJ3 Release

[joyce!csl!winkler@ames.arpa (Timothy Winkler)]

Dear Colleagues:

Release 1.0 of OBJ3 is now available!

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, and it has the following properties:

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

     * statements in OBJ3 programs are sentences in L,

     * the denotational semantics of an OBJ3 program P is an initial model
        of P, and

     * operational semantics is given by (efficient) deduction in L.

     This allows OBJ3 to be used as a theorem prover for L.  (In fact, the
     logical system L for OBJ3 is order sorted equational logic; see below.)

  2. OBJ3 has parameterized programming, which allows very flexible program
     structuring and reuse, giving the expressive power of higher order
     programming while retaining a first order logic, and supporting the
     following features:

     * objects to contain executable code, and theories to define properties;
     
     * parameterized modules, with theories to define interfaces;

     * views to define instantiation (binding) of parameterized modules, and
       to assert properties of modules, and

     * module expressions, which describe complex (sub)system as
       interconnections of given modules (possibly parameterized), and then
       actually constructs them when evaluated.

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

     * user-definable subtypes

     * exception handling

     * multiple inheritance

     * operation overloading and

     * retracts a form of run time type checking that supports a
       strong typing which is as flexible as weak typing.

  5. OBJ3 has user-definable evaluation strategies, which

     * can be eager, lazy, or more exotic combinations, 

     * are user definable for each operation separately (rather than
       globally), and are computed by default (using strictness analysis)
       if not given explicitly.

  6. OBJ3 has pattern matching modulo associativity and/or commutativity,
     plus identity by completion.

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

  1. software design

  2. software specification

  3. rapid prototyping

  4. theorem proving

  5. hardware verification

  6. functional programming.

Here is a cute little proof in OBJ3:
############################################################################
---> /dir/goguen/obj/proofs/mmm.obj
---> Fermat's "little theorem": m**p=m(mod p), for p=3

obj NAT is sort Nat .
  op 0 : -> Nat .
  op s_ : Nat -> Nat [prec 1] .
  ops (_+_)(_*_) : Nat Nat -> Nat [assoc comm] .
  vars L M N : Nat .
  eq M + 0 = M .
  eq M + s N = s(M + N) .
  eq M * 0 = 0 .
  eq M * s N = (M * N)+ M .
  eq L * (M + N) = (L * M)+(L * N) .
  eq M + M + M = 0 .
endo

---> base case, m = 0
reduce 0 * 0 * 0 == 0 .

---> induction variable and hypothesis
obj VARS is extending NAT .
  op m : -> Nat .
  eq m * m * m = m .
endo
---> induction step
reduce (s m)*(s m)*(s m) == s m .
---> QED
############################################################################

OBJ3 is written in Kyoto Common Lisp (KCL) and has been compiled on Sun3's;
presumably, it can be compiled on any machine with a Common Lisp compiler.  We
can send you an executable form of OBJ3 for Sun3's, which occupies about 4
Mbytes of disk space, or you can build OBJ3 yourself from sources, which will
require about 1 Mbyte disk space for the sources and up to 3 Mbyte for the
construction.  You will also need a license for KCL, or some other Common
Lisp.  KCL needs 4 Mbytes for its sources, up to 10 Mbytes for construction,
and its executable occupies about 2 Mbytes.  Our distribution media are Sun
cartridges, and 1/2in. tape at 1600 bpi in Unix tar format.  Our shipment will
include a file of OBJ3 examples and some documentation.

If you wish to receive the OBJ3 distribution tape, please send a request to:

	   Judith Burgess, Librarian
           Computer Science Laboratory
           SRI International
           333 Ravenswood Ave.
           Menlo Park, CA 94025, USA

           Telephone: (415) 859-5924
           ARPAnet:   burgess@csl.sri.com

Judith will then send you the OBJ3 Information Form, and License Agreement,
with instructions on how to fill them out.  When you return them to us,
appropriately filled out and signed, with a check or money order for $150 in
US dollars payable to SRI International, we can then send you the tape and
documentation.

Sincerely yours,

Joseph Goguen, Jose Meseguer, and Timothy Winkler
Computer Science Laboratory
SRI International
333 Ravenswood Ave.
Menlo Park, California 94025, USA