Joseph A Goguen

- State of the art for formal methods in software engineering
- Lite formal methods
- BOBJ
- Kumo
- Hidden algebra
- Requirements Engineering
- Parameterized Programming and Software Architecture
- Institutions
- Data Integration

BOBJ is a new member of the OBJ family of algebraic specification languages. Like the other members of this family, it has a very powerful module system (based on parameterized programming), a parser for user defined mixfix syntax, a fast term rewriting engine, a strong but flexible type system, a rigorous algebraic semantics, and sufficient theorem proving capability to support rapid prototyping by symbolic execution. Our research has been mainly focused on implementation techniques, theorem proving algorithms, and applications to concurrent distributed systems.

The most innovative aspect of BOBJ is its behavioral (also called observational) semantics, which allows systems to be characterized through their responses to a selected set of experiments, rather than through an explicit description of how they represent and manipulate states; this has a mathematical basis in a new kind of equational logic, called hidden algebra, which gives a behavioral semantics for states. BOBJ's verification capability is mainly based on term rewriting and coinduction; its most powerful algorithm is discussed in the paper "Circular coinductive rewriting". BOBJ can also be used as an extremely high level programming language, due to its term rewriting (modulo attributes) operational semantics, a powerful form of pattern matching and subpattern replacement, which is nonetheless easy to learn and easy to use. Although slower than compiled languages, BOBJ's term rewriting engine is fast enough that BOBJ is suitable for many small and medium programming tasks, and for the rapid prototyping of larger systems.

BOBJ has all the power of higher order functional programming using only first order statements, through the use of parameterized modules, but it goes beyond functional programming in its ability to handle states, based on hidden algebra, and its ability to encapsulate, based on its module system. The paper "Higher order functions considered unnecessary for higher order programming" gives details about parameterized programming and functional programming. These ideas have influenced the module systems of Ada, C++, ML, and the Modula languages.

The BOBJ homepage has much more detail, including links to recent papers, and a collection of applications that illustrate how we are attempting to push the current envelope of algebraic specification.

Kumo is a theorem proving system that also generates websites that document its proofs. It uses first order logic with equality in both behavioral and non-behavioral modes, as opposed to the simpler equational behavioral logic of BOBJ; it also supports initial algebra semantics for specifying abstract data types. Although Kumo makes extensive use of BOBJ and its theorem proving algorithms, Kumo has a much more general logic, a completely different interface, and additional features to support the lite formal methods paradigm, including:

- parameterized programming, for modularization and reuse;
- integration of formal and informal methods, using a fuzzy logic to keep track of confidence levels;
- integration of informal proof explanations (including illustrative interactive applets) and links to tutorial material integrated with the proofs themseles, as well as pages that call remote theorem provers to execute certain key proof parts on demand; and
- design verification, which can range from fully formal to very informal.

The Kumo homepage gives more detail, including links to recent papers, and the Kumo examples page has links to a collection of websites generated by Kumo, arranged to form a tutorial on the system and its logic. There are also links to the user interface design principles that were used, based on algebraic semiotics.

Hidden algebra is a recent development in the tradition of algebraic specification, which makes it possible to handle states and to take a behavioral perspective on systems; both of these are needed for a smooth treatment of concurrent systems, as can be also seen in work from the foundational area of process algebra, as well as work on concrete applications such as communication protocols. The hidden algebra homepage gives a comprehensive introduction, including links to research papers where techncial details and many examples can be found; the BOBJ homepage also has many examples that illustrate various aspects of the theory.

In brief, the task of requirements engineering is to reconcile the technical necessities and possibilities for a project with the social necessities and possibilities of that project. This can be very difficult, because the two are often in conflict, and moreover, two different kinds of expertise are required, the first in traditional engineering, and the seconed in the social sciences, especially ethnography. See the Requirements Engineering homepage for much more detail, including links to several papers.

The basic idea of parameterized programming is to allow modules to have parameters that range over other modules, with interfaces that may include not only syntactic information, but also semantic constraints on the modules that are allowed to be substituted for formal parameters. Since a module may encapsulate any number of (closely related) types (or classes) and their associated procedures, this leads to a more powerful kind of higher order programming than is supported by traditional functional programming. Moreover, the statements in modules can be restricted to be first order without any loss of power, and they can also be imperative. In addition, so-called "views", which bind modules to the interfaces of other modules, are first class citizens, and they too can be parameterized. The paper "Higher order functions considered unnecessary for higher order programming" gives many details about this paradigm.

Not only is parameterized programming used in all the languages of the OBJ family, but it also provides a good basis for describing the large grain structure of software systems, i.e., for what is now called software architecture. The paper "Parameterized programming and software architecture" gives a good introduction to this approach, and BOBJ provides a complete implementation of parameterized programming, which makes it possible to conduct some interesting experiments.

The great diversity of logics used in computer science is a significant
challenge to those working in formal methods. One approach to bringing some
order to this chaos is to formalize the notion of "a logic" and then
systematically study general properties of logics using institutions,
including the representation, implementation, and inter-translation of logics.
This is the purpose of the theory of **institutions**, as developed and/or
applied in a literature that now has several hundred papers. The basics may
be found in the original paper, "Institutions:
Abstract model theory for Specification and programming", and our most
recent work is described in the paper, "Institution Morphisms".

Parameterized programming has been developed at the level of institutions, so that the powerful module systems that it supports can be used for any logical system; indeed, this was the main original application for institutions, and it is the basis for the module systems of all the languages in the OBJ family, noting that they each have somewhat different logics. These languages include OBJ3, CafeOBJ, Maude, CASL, and BOBJ.

Many areas of science, technology, commerce and government have a serious need to integrate data that comes from multiple sources, and which therefore may be stored and formatted in multiple incompatible ways, usually without adequate documentation of the underlying assumptions, let alone of the social context of use of the data. The problems that arise in this connection are formidable, but there are reasons to believe that this may be an ideal application area for lite formal methods. See the Data Integration homepage for more detail, including some code, and some links to related pages.

BACK | NEXT | LAST | MAIN |

Maintained by Joseph Goguen

Last modified: Wed Feb 5 19:40:18 PST 2003