Fun with 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.

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.

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.

1. 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.
    
2. 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.
    
3. 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.
    
4. Implementing Stack with Pointer and Array gives a behavioral refinement proof for the correctness of this well known way of implementing stacks.
    
5. 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.
    
6. 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.
    
7. 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.
    
8. 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.
    
9. 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.
    
10. 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.
     
11. 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.
     
12. 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.
     
13. 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.

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.

1. Software Engineering with OBJ: algebraic specification in action, edited with Grant Malcolm, Kluwer, 2000, ISBN 0-7923-7757-5.
2. Algebraic Semantics of Imperative Programs, by Joseph Goguen and Grant Malcolm, MIT Press, 1997; ISBN 0-262-07172-X.
3. 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.
4. 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.

1. [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.
2. 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.
3. 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).
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.
11. The hidden algebra homepage.
12. 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.
13. 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.