An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks
Formal Engineering Methods, International Conference on (1997)
Nov. 12, 1997 to Nov. 14, 1997
K. Futatsugi , Graduate Sch. of Inf. Sci., Adv. Inst. of Sci. & Technol., Ishikawa, Japan
A. Nakagawa , Graduate Sch. of Inf. Sci., Adv. Inst. of Sci. & Technol., Ishikawa, Japan
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 an 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 networks, 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 cheeking/verifying CafeOBJ specifications, etc. Forsdonnet is designed to be based on already established standard network infrastructure components like HTML and Netscape Navigator. The paper gives an overview and design considerations of the CAFE environment, featuring mainly CafeOBJ and Forsdonnet languages.
algebraic specification; CAFE specification environment; algebraic approach; formal specifications; network based environment; algebraic specification language; CafeOBJ; algebraic specification paradigm; behavioral specifications; rewriting logic; behavioral hidden sorted algebra; language constructs; formal object oriented specifications; specification documents; document formatting language; Forsdonnet; FORmal Specification Document ON NETwork; HTML; informal specifications; standard network infrastructure components; Netscape Navigator
A. Nakagawa and K. Futatsugi, "An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks," Formal Engineering Methods, International Conference on(ICFEM), Hiroshima, JAPAN, 1997, pp. 170.