Fun with BOBJ
Fun with BOBJ
This is the BOBJ homepage, devoted to introducing and illustrating the BOBJ
system for rapid prototyping, behavioral specification, computation, and
verification. This page gives a brief orientation to BOBJ, with links to a
number of examples. Some familiarity with hidden algebra and OBJ3 is assumed; the bottom of this
page gives some references and links to information on these, as well as to
some more specific aspects of the theory and implementation of BOBJ.
BOBJ is UCSD's implementation of next generation technology for
prototyping and algebraic specification and verification. It extends OBJ3
with support for behavioral specification and verification, and in
particular, it provides circular coinductive rewriting with case
analysis for conditional equations over behavioral theories, as well
as behavioral rewriting over order sorted theories, modulo attributes that
can be any combination of associative, commutative and identity. BOBJ also
supports concurrent connection of behavioral theories, cobasis declaration,
default cobasis generation, operations with multiple hidden arguments,
non-congruent operations, higher order parameterized programming (with
modules parameterized by modules, and instantiated with morphisms), sort
constraints, and membership equational logic. In addition, BOBJ, like
OBJ3, supports ordinary rewriting for order sorted equational logic (modulo
attributes), as well as first order parameterized programming. These
features are illustrated in examples below. BOBJ is written in pure Java
and so should run on any machine.
BOBJ syntax is almost the same as that of OBJ3, with exceptions that
include the following: term syntax is more flexible, due to using JavaCC for
parsing; in addition to the OBJ3 keywords "th" and "obj",
BOBJ modules can also begin with the keywords "dth" for data theories
(equivalent to "obj"), which have initial semantics, and
"bth" for behavioral theories, which have hidden semantics; any
module can be closed with the keyword "end"; operations within
behavioral theories are considered congruent unless they are given the
attribute "ncong"; the automatically generated cobasis for the
currently selected module can be seen with the command "show
cobasis", and circular coinductive rewriting is invoked with the command
"cred", whereas "red" invokes behavioral rewriting without
circularity (which is ordinary rewriting for visible sorts).
Several data types and many equations are "builtin," i.e., are available
without having to be defined by the user. These include the data types
BOOL of Booleans, NAT of naturals, INT of
integers, and FLOAT of floating point numbers; moreover,
BOOL is automatically imported into every module; these modules
have many builtin equations. Users can see what a module MOD
provides with the command "show MOD ." ; this works for builtin as
well as user supplied modules. For example, "show TRUTH" will
reveal the builtin conditional if_then_else_fi, and the builtin
operation == which tries to check equivalence of arbitrary terms
(TRUTH does not include any other Boolean operations). The
command "set cred trace on" causes BOBJ to output information
about circular coinductive rewriting. The occurrence of a circularity in a
cred computation is signalled by an occurrence of the keyword
"deduced" in its trace, whereas "reduced" appears when
there are no circularities. The command "set trace on" causes
extensive information about rewriting to be produced.
The concurrent connection of systems is an important operation
for constructing complex systems from components. It is supported in BOBJ
by a binary associative infix operator "||" that takes two (or
more) modules as arguments, and it is implemented by creating a new hidden
sort that is the tupling of the principal sorts of the component modules;
this has been proved behaviorally equivalent to concurrent connection
defined in a more abstract (category theoretic) way that more clearly
exhibits its concurrent nature. The code below is equivalent to what BOBJ
provides for the case of n=2 modules; note that the projection
operations are noncongruent, that the n-tuple sort is named
"Tuple" (for all n), and that the so-called "untupling
equation" is the last one. The sort Tuple is always hidden, even
when the module is instantiated with all component sorts visible.
bth 2[1 2 :: TRIV] is sort Tuple .
op < _,_ > : Elt.1 Elt.2 -> Tuple .
op 1* _ : Tuple -> Elt.1 [ncong].
op 2* _ : Tuple -> Elt.2 [ncong].
var E1 : Elt.1 . var E2 : Elt.2 . var T : Tuple .
eq 1* < E1, E2 > = E1 .
eq 2* < E1, E2 > = E2 .
eq < 1* T, 2* T > = T .
end
Tupling is a prime example of a congruent operation having multiple hidden
arguments, and untupling is a prime example of a noncongruent operation. The
BOBJ algorithm that computes cobases for specifications using congruence
criteria takes account of the untupling equation to simplify cobases when
concurrent connection is used; this is important for many applications.
The BOBJ syntax for visible tupling differs from that for concurrent
connection; it is like that of OBJ3, supporting modules named
nTUPLE that provide n-tuples; but whereas OBJ3
provides only a few of these as builtin modules, BOBJ generates the
necessary tupling and untupling operations on an as-needed basis, for any
n > 1. The tuple sort is TUPLEn, and the tuple
constructor is <<_;_;...;_>>, while the n selectors are
the same as for the concurrent connection, namely 1*_,
2*_, etc.
The implementation of BOBJ is entirely due to Kai
Lin and includes innovative techniques for speeding up rewriting and for
implementing behavioral and circular coinductive rewriting, extending earlier
research by Grigore Rosu and Joseph Goguen. We were partially inspired to
proceed with implementing BOBJ by the success of the CafeOBJ system, which combines ordinary
(order sorted) equational logic with both rewriting logic and a somewhat
different version of hidden algebra.
Examples
The following examples can be found on this site; most of them use circular
coinductive rewriting. They are roughly ordered by the features of BOBJ that
they introduce. Taken together, these examples demonstrate the surprising
power of the combination of operations with multiple hidden arguments,
cobases, circular coinductive rewriting, the cobasis algorithm, the concurrent
connection operation, case analysis, and higher order parameterized
programming.
- Some Simple Vending Machines gives
behavioral specifications and behavioral proofs for some simple properties of
some simple vending machines, illustrating the main behavioral features of
BOBJ.
- Sets Are Behavioral illustrates some
basic features of BOBJ with the important and suggestive example of sets,
showing in particular that sets can be implemented with lists.
- Lazy Functional Programming Examples is a
collection of proofs about properties of streams, such as might arise arise
in correctness proofs of lazy functional programs, all using circular
coinductive rewriting, with no user intervention.
- Implementing Stack with Pointer and Array
gives a behavioral refinement proof for the correctness of this well known
way of implementing stacks.
- Equivalence of Regular Expressions is a
behavioral specification of regular expressions with some proofs of
equivalences of regular languages; this example makes especially good use of
parameterized modules.
- Meta-programming and Sort Constraints
illustrates the use of BOBJ's metaprogramming features to define and use
"sort constraints," a concept from order sorted algebra which allows defining
subsorts by predicates; the examples are bounded stacks, the subsort of even
numbers, and the theories of categories and of paths in a graph.
- Correctness of a Hardware Retiming
Transformation: a simple case analysis in circular coinductive
rewriting algorithm, showing correctness of a "retiming" transformation, from
one hardware circuit with a feedback loop to another.
- Correctness of the Alternating Bit
Protocol, illustrating many distinctive features of BOBJ, especially
conditional circular coinductive rewriting, as well as case analysis, and
some specification tricks, including a simple new algebraic approach to
fairness.
- Higher Order Parameterized Programming
gives some examples of parameterized modules and views, illustrating the very
powerful module system that parameterized programming makes possible (these
examples do not use hidden algebra). BOBJ is the first language to implement
higher order parameterized programming.
- Fun with Streams and Buffers is a
collection of behavioral specifications and proofs for some simple
combinations of streams and buffers. Using streams for the sender process,
and a one item buffer for the receiver process, seems very natural for
communication systems in a behavioral setting.
- Multiple Representation and Coercion
illustrates how sort constraints and retracts can be used to
provide multiple representations for a single abstract type, with
coercions that change representation automatically when needed. The
example used is Cartesian and polar representations of points (or vectors
from the origin) in the plane.
- Correctness of Petersen Critical Section
Algorithm. This example builds on techniques developed for the
Alternating Bit Protocol, but the proof makes especially good use of the
product of case analyses. There are 10 binary cases splits, and hence 1024
cases altogether. Although roughly a quarter of the cases are automatically
eliminated, the output is still very voluminous, since the reason for each
failure is documented.
- Correctness of a Real Time Data Transfer
Protocol: illustrates BOBJ's case analysis construct on a real time
asynchronous data transmission protocol; the spec and proof are due to
Kokichi Futatsugi, but our method greatly simplifies its presentation, by
relying on products of cases and excluded cases. This example does not use
hidden algebra.
Some References
We first mention two books about OBJ3, which provide a good starting
point for those not already familiar with the algebraic specification and
the OBJ family; a link is also given to the OBJ3 manual, which is a chapter
in the first book.
- Software Engineering with OBJ: algebraic specification in
action, edited with Grant
Malcolm, Kluwer, 2000, ISBN 0-7923-7757-5.
- Algebraic Semantics of Imperative
Programs, by Joseph Goguen and Grant Malcolm, MIT Press, 1997; ISBN
0-262-07172-X.
- The official OBJ3 manual, with much tutorial material and many
examples, as revised and extended August 1999, is Introducing OBJ by Joseph Goguen, Timothy
Winkler, José Meseguer, Kokichi Futatsugi and Jean-Pierre
Jouannaud, which appears in Software Engineering with OBJ: algebraic
specification in action.
- A detailed treatment of the use of OBJ in education is given in An Executable Course in the Algebraic
Semantics of Imperative Programs, by Joseph Goguen and Grant Malcolm, in Teaching and
Learning Formal Methods, edited by Michael Hinchey and C. Nevill Dean,
Academic Press, 1996, pages 161-179.
Much more information about and background for BOBJ, its algorithms, its
underlying hidden algebraic semantics, and the Tatami project of which it is a
part, can be found in our papers, including the following:
- [New] Specifying, Programming and Verifying
with Equational Logic, by Joseph Goguen and Kai Lin, in We Will Show Them! Essays in Honour of
Dov Gabbay, Vol. 2, edited by Sergei Artemov, Howard Barringer, Artur
d'Avila Garcez, Luis Lamb and John Woods, College Publications 2005, pages
1-38. In a logical programming language, a program is a theory over a
formal logic, and its computation is deduction in that theory. As a
consequence, specification, programming and verification all fit a single
unified framework. The OBJ languages are logical programming languages,
based on various extensions of first order equational logic. Everything
in these languages is logic-based, including their powerful module
systems, which provide a convenient language for software architecture. A
new feature introduced in this paper is mutual coinduction, illustrated
with inductive proof schemes. Two theoretical contributions are a new
formalization of logical programming, and a new semantics for higher order
modules. A postscript version
is also available.
- Behavioral Verification
of Distributed Concurrent Systems with BOBJ, by Joseph Goguen and
Kai Lin. Keynote lecture for Conference on Quality Software, Dallas
TX, 5-6 November 2003. In Proceedings, Conference on Quality
Software, IEEE Press 2003, pages 216-235. A postscript version, and the slides for a lecture are also
available, although these are much less technical than the paper, which
proves correctness of the alternating bit protocol making strong use of
recent features of BOBJ, especially
conditional circular coinductive rewriting with case analysis. An early
version of this paper is A Hidden
Proof of the Alternating Bit Protocol, by Kai Lin and Joseph Goguen. See also the brief early
web note Correctness of the
Alternating Bit Protocol.
- Semiotic Morphisms,
Representations, and Blending for User Interface Design, by
Joseph Goguen. Keynote lecture, in Proceedings, AMAST Workshop on
Algebraic Methods in Language Processing, AMAST Press, 2003, pages
1-15 (held Verona, Italy, 25 - 27 August 2003). This paper extends
algebraic semiotics to handle interaction by using hidden algebra; some
examples are given in detail. A post
script version of the paper, and the slides for the talk are also
available (you may have to change the orientation to swap landscape).
- Conditional Circular Coinductive
Rewriting with Case Analysis, by Joseph Goguen, Kai Lin and Grigore Rosu, given at 16th Workshop on
Algebraic Development Techniques, Frauenchiemsee, Germany, 24-27
September 2002. The slides are
also available, but you may have to reorient them to "seascape". This
describes the extension of BOBJ's circular coinductive rewriting algorithm to
conditional equations, and allowing "splits" for case analyses.
- Web-based Support for
Cooperative Software Engineering, by Joseph Goguen and Kai Lin. In
Annals of Software Engineering, volume 12, 2001, a special issue on
multimedia software engineering, edited by Jeffrey Tsai. A gzipped postscript version is also
available. This is an overview of the Tatami project, featuring version 4 of
the Kumo proof assistant and website generator, and focusing on its design
decisions, its use of multimedia web capabilities, and its integration of
formal and informal methods for software development in a distributed
cooperative environment.
- An Induction Scheme in Higher
Order Parameterized Programming, by Joseph Goguen and Kai Lin. A "programming pearl" using induction schema to
illustrate higher order modules and higher order views in BOBJ.
- Circular Coinduction
by Grigore Rosu and Joseph Goguen, in Proceedings, International Joint
Conference on Automated Deduction, Sienna, June 2001. Proves correctness
of circular coinduction, and draws consequences including various congruence
criteria.
- Circular Coinductive
Rewriting by Joseph Goguen, Kai Lin, and Grigore Rosu, in
Proceedings, Automated Software Engineering '00 (Grenoble France),
September 2000, IEEE Press, pages 123-131. Using many examples, this paper
introduces the BOBJ system for behavioral
specification and computation, and its surprisingly powerful circular
coinductive rewriting algorithm for proving behavioral equalitites, which
combines behavioral rewriting with circular coinduction. A gzipped postscript version is also
available.
- Behavioral and Coinductive
Rewriting, by Joseph Goguen, Kai Lin, and Grigore Rosu. Keynote
address, in Proceedings, Rewriting Logic Workshop, 2000 (Kanazawa,
Japan), edited by Kokichi Futatsugi, Japan Advanced Institute of Science and
Technology, September 2000, pages 1-22. A somewhat informal summary of
results up to mid-2000, including simulating behavioral rewriting with
standard rewriting, and circular coinductive rewriting, which is a
surprisingly effective algorithm for proving behavioral equalities.
- An Overview of the Tatami
Project, by Joseph Goguen, Kai Lin, Grigore Rosu, Akira Mori and
Bogdan Warinschi, in Cafe: An Industrial-Strength Algebraic Formal
Method, edited by Kokichi Futatsugi, Tetsuo Tamai and Ataru Nakagawa,
Elsevier, 2000, pages 61-78. This is a high level snapshop of the UCSD Tatami project as of late 1999. See also the
brief report by Prof. Rod Burstall,
the brief summary of results as of Sept.
2001, and the one page progress summary for our NSF grant up to October
1999, Hidden Algebra and Concurrent
Distributed Software, which appeared in Software Engineering Notes.
- The hidden algebra homepage.
- The OBJ3 section of the
OBJ language family homepage, which gives brief descriptions and references
for OBJ3 and the other members of this language family.
- BOBJ ftp site,
at
ftp://ftp.cs.ucsd.edu/pub/fac/goguen/bobj/
, for the (more or
less) most recent version of BOBJ, including its Java source code.
WARNING: This ftp website now requires host authentication, so you
probably cannot use it from a laptop over a wireless network.
To the Tatami project homepage
Maintained by Joseph Goguen
Last modified: Wed Feb 1 10:44:20 PST 2006