Object-oriented modeling method for algebraic specifications in CafeOBJ

Abstract

A scenario-based object-oriented modeling method for algebraic specifications is proposed. The method is based on the integration of a new algebraic specification language, CafeOBJ, and a multiparadigm design notation, GILO-2 (Generic Interaction Language for Objects). CafeOBJ is a successor of the algebraic specification language OBJ and supports object-oriented formal specifications based on hidden order sorted rewriting logic. GILO-2 provides collaborations as well as classes of objects to capture behavioral aspects of scenarios in object-oriented modeling. Given a problem description of the system to develop, the proposed method provides guidelines for decomposing the problem into executable CafeOBJ specification modules through scenario-based object-oriented design in GILO-2; the decomposition reflects the structure of the problem domain. The proposal also indicates how formal executable specification in CafeOBJ can be systematically obtained from the design in GILO-2.