Japan Advanced Institute of Science and Technology
3pm Monday 4 August 2003
Room 2511, JCMB, King's Buildings
Formal methods are still expected to improve the practice of software engineering. Formal methods are better supported by formal specification languages equipped with formal verification capability.
CafeOBJ is a formal specification language equipped with verification methodologies based on algebraic specification technique. CafeOBJ is an executable wide spectrum language based on multiple logical foundations; mainly based on initial and hidden algebras. Static aspects of systems are specified in terms of initial algebras, and dynamic aspects of systems are specified in terms of coherent hidden algebras.
CafeOBJ is the first algebraic specification language which incorporates observational (or behavioral) specifications based on coherent hidden algebras. Observational specifications in CafeOBJ can be seen as a nice combination of static and dynamic specifications, and facilitate natural and transparent specification and verification of complex systems.
This talk gives an overview of CafeOBJ language/system and an interactive equational proof method based on CafeOBJ.