Busy Bees!

[zccap74]

For those that haven't looked at maude or cafeOBJ recently, this is what people
have been up to...
What I'd STILL like to know is; what can these two languages NOT do? What makes
them unsuitable as languages for tunes? Personally, I can't see anything that
makes them unsuitable. They implement good reflection, coinductive and
inductive
techniques, and can support any logic mentioned in the posts over the last few
months. I guess what I'm trying to get is a response from someone saying either
'yes I'll look at it' or 'it's not suitable for these reasons'
The ball is in your court guys!



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/


                   Present: Maude as a Means to and End

   Maude is both a fruit of, and a means to advance, the research of the
   Logic and Specification Group, that focuses on:

     * Formal Executable Specification and Verification

     * Software Composition, Reflection, and Metaprogramming

     * Object-Oriented Specification and Software Architecture

     * Concurrent, Distributed, and Mobile Computing

     * Logical Frameworks and Formal Interoperability

     * Logical and Semantic Foundations
     
              Present (IV): Performance and Applications

   Currently, Maude is the fastest rewriting logic interpreter in the
   world. Typical performance is 800K-840K rewrites per second for
   standard term rewriting, and 30K-110K rewrites per second for
   associative-commutative rewriting on a 300 Mhz Pentium II.

   The most interesting applications of Maude are metalanguage
   applications in which Maude is used to implement many other logics,
   formal tools,  specification languages, and programming languages.  So
   far we have developed:

     * Full Maude (7,000 lines of Maude code)

     * An inductive theorem prover and a Church-Rosser Checker
 
     * Translations between different logics (formal interoperability)

     * Executable environments for several architectural description
       languages

     * Several language interpreters and a supercompiler

     * Formal specifications of communication protocols and network
       algorithms.

   After the release of Maude 1.0 we expect that many other applications
   will be developed.
   
                              Future Plans

     * Release of Maude 2.0: built-in objects, unification and narrowing,
       efficient search.

     * A book on Maude, simultaneous with Maude 2.0

     * Mobile Maude

     * Mature formal tools: Inductive Theorem Prover, Knuth-Bendix and
       Coherence Completion and Checking, etc.

     * Maude Compiler