The Japanese government has awarded contracts totaling about $3.2 million to a consortium of major Japanese companies, with subcontracts to universities around the world, to build an industrial strength implementation and support environment for the OBJ language, originally designed by Prof. Joseph Goguen, of the Computer Science and Engineering Department at UCSD.
The purpose of the project, called CafeOBJ, is to make formal methods accessible to practicing software engineers. Formal methods involve making mathematical models of software and deriving properties of the software from the models. This parallels practice in other areas of engineering, but is more difficult for software, due to the extreme complexity of modern software systems, and the unfamiliarity of engineers with the complex discrete mathematics required. The CafeOBJ language enriches the original OBJ with features for distributed object oriented systems.
Over a 1.5 year period, the CafeOBJ consortium will build an abstract machine based compiler, plus an environment to support distributed cooperative specifying, writing, and verifying of programs over the world wide web. Formal verification usually means proving properties of specifications. The CafeOBJ system architecture calls for proof editors at distributed software development sites linked with distributed proof servers; proof servers accept proof tasks in appropriate logics, and will be chosen from among the best available in the world.
Prof. Goguen's Meaning and Computation Lab at UCSD is building the proof editor, called Kumo (Japanese for spider) to populate the library with interesting examples. The team consists of Prof. Goguen, two CSE graduate students, a Postdoc from Japan, a Visiting Scholar from Japan, and a Professor of Ethnomethodology on sabbatical from Australia. About 40 individuals are working on the CafeOBJ project around the world, mostly in Japan.
The Kumo proof editor takes a novel approach. First, its code is not written directly by humans, but rather by a proof editor generator, called Duck, based on a high level specification; at a later phase, even Duck will be generated from a specification. Second, Kumo will implement a truth maintenance protocol to allow multiple versions of proofs at multiple sites, including incomplete and even incorrect proofs; failed proof attempts can motivate more subtle proofs that overcome the failure.
Perhaps the most exciting results coming out of the Meaning and Computation Lab concern a new approach to designing user interfaces that takes account of the content and structure of information, not just its representation. This is important to the CafeOBJ project, because it aims at ordinary software engineers, not just specialists in formal methods. The new approach, called "algebraic semiotics" (semiotics is the theory of signs), is being used to help design interfaces for presenting and building proofs. This approach combines technical and social aspects of system design, and also uses ideas from cinema and narratology. Although traditional theories from ergonomics, HCI (human computer interface), and cognitive science can help with keyboard layout, window color choice, font size, etc., they are not so useful for more semantic problems like linking background tutorial information and informal explanations to formal proof steps.
Prototype systems using Java applets to illustrate software proofs are currently running in the lab, and are accessible over the web, from http://www.cs.ucsd.edu/groups/tatami/.