CafeOBJ

The purpose of the CafeOBJ project 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.¹

The Munich group is especially concerned with case studies. These comprise:

• Implementation of the case studies of the fOOSE-project in CafeOBJ
• Development and testing of a CafeOBJ specification of the "Munich Airport"
• Formalization of a semantics of the object-oriented, concurrent programming language Java in CafeOBJ

Contact person: Alexander Knapp.

More information to this project at The CafeOBJ Home Page.