Documentation

Several pieces of documentation come with this OBJ3 release, including a FAQ, Release Notes, a TODO list, a known bug list, and some introductory OBJ3 papers.

The two canonical references for learning OBJ3 are the classic Algebraic Semantics of Imperative Programs by Joseph A. Goguen and Grant Malcolm published by MIT Press, and the new Software Engineering with OBJ: Algebraic Specification in Action, edited by Joseph A. Goguen and Grant Malcolm, published by Kluwer Academic Publishers in 2Q, 2000 [GoguenMalcolm96-ASoIP, GoguenMalcolm00]. The new book compiles many of the seminal OBJ3-related papers into one complete reference text --- we highly recommend it!

Building OBJ3

Thanks go primarily to Sula Ma at Oxford for this OBJ3 port to GCL 2.2.2. Sula is preparing a new branch of OBJ called "OBJ4", and this port was part of that work.

Please see the source README for information on building OBJ3.

Using OBJ3

The best references for getting up-to-speed with OBJ3 are listed in the OBJ3 FAQ and are indexed in the OBJ/Algebra bibliography included with this release. We strongly suggest reading the Introducing OBJ paper (a draft is available via Joseph Goguen's OBJ web page) and the two Goguen-Malcolm books. Most academic libraries should already have a copy of the Algebraic Semantics text [GoguenMalcolm96]. Encourage your library to purchase a copy of the new Software Engineering with OBJ text [GoguenMalcolm00]. Finally, a good overview of the use of OBJ3 in teaching formal methods can be found in Teaching And Learning Formal Methods [GoguenMalcolm96].

For those primarily interested in parameterized programming, the paper An Implementation-Oriented Semantics for Module Composition is a must-read [GoguenTracz97]. For those interested in higher-order logics/programming/rewriting, More Higher Order Programming with OBJ3 is a good start [GoguenMalcolm00-HOP]. Other references include [Wolfram93] and [Goguen90-HOP].

For users interested in extending the OBJ3 system, please see [Winkler-NewFeatures] and [WinklerMeseguer-Builtins], both of which are included in this release.

Questions or comments?

Please email kiniry@acm.org if you have any questions, comments, or other feedback about this release. General OBJ3 questions should be addressed to kiniry@acm.org.