Software Engineering with OBJ:

Algebraic Specification in Action

Joseph A. Goguen and Grant Malcolm (eds.), Kluwer Academic Publishers, Boston, 2000.

ISBN: 0-7923-7757-5

This book presents case studies in the use of OBJ by leading practitioners in the fields of formal methods and software engineering. The book is novel in concentrating on the use of the executable specification language OBJ which, in contrast to most other popular approaches to formal methods, is an executable algebraic specifiction language with a simple yet rigorous mathematical foundation. The book gives a detailed introduction to the language, including such features as its support for error handling, overloading, and its powerful generic modules which support large grain `hyperprogramming', reusablity and software composition. The case studies cover such diverse application areas as computer graphics, hardware development and verification, concurrent systems, and an interpreter for OBJ designed using OBJ itself.

The book consists of an introduction and nine papers.

Introduction by Joseph A. Goguen and Grant Malcolm.

Part I: A Comprehensive Introduction to OBJ

Introducing OBJ3, by Joseph Goguen, Timothy Winkler, José Meseguer, Kokichi Futatsugi and Jean-Pierre Jouannaud.

Part II: Specifications in OBJ

Specifying in OBJ, verifying in REVE, and Some Ideas on Time, by Victoria Stavridou.
A Practical Guide for Constructing a Graphics System, by Ataru Nakagawa, Kokichi Futatsugi, S. Tomura and T. Shimizu.
Specification of Computer Graphics Standards, by David Duce.

Part III: Semantics in OBJ

Semantic Specifications for the Rewrite Rule Machine, by Joseph Goguen.
OBJ for OBJ, by Claude Kirchner, H\'el\`ene Kirchner and Aristide M\'egrelis.
OBJSA Nets: OBJ and Petri Nets for Specifying Concurrent Systems, by Eugenio Battison, Fiorella de Cindio and Gian-Carlo Mauri.

Part IV: Parameterized Programming

A LOTOS Simulator, by Kazuhito Ohmaki, Koichi Takahashi and Kokichi Futatsugi.
More Higher Order OBJ, by Joseph Goguen and Grant Malcolm.

Back to my home page.

Grant Malcolm