An Overview of CAFE Specification Environment (abstract)
Kokichi Futatsugi and Ataru Nakagawa
CAFE is the name of a network based environment now under
development for supporting systematic creation, checking,
verification, and maintenance of formal specifications. CAFE has
an algebraic specification language called CafeOBJ as its main
specification language, and adopts algebraic specification paradigm as
its foundation. CafeOBJ is a successor of the OBJ language,
and has important new features for concurrency and behavioral specifications.
Concurrency and behavior are specified based on rewriting logic and
behavioral (hidden-sorted) algebra respectively. These new features
make it possible to provide powerful language constructs for formal
object-oriented specifications.
CAFE is designed to be a network based environment. For sharing
specification documents systematically over the network, a new
document formatting language called Forsdonnet (FORmal Specification
Document ON NETwork) is designed by extending HTML. Forsdonnet
includes constructs for formal and informal specifications, commands
for executing (prototyping) and checking/verifying CafeOBJ
specifications, etc. Forsdonnet is designed to be based on already
established standard network infrastructure components like HTML and
Netscape.
This paper gives an overview and design considerations of the CAFE
environment, featuring mainly CafeOBJ and Forsdonnet
languages.
Back to CafeOBJ Home Page