kirancodes.me
To Proof Maintenance & Beyond!

An Object-Oriented Modeling Method for Algebraic Specifications in CafeOBJ

Shin Nakajima, Kokichi Futatsugi

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, GIL0-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.GIL0-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 GIL0-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 GIL0-2.

BibTeX
@inproceedings{Nakajima-Futatsugi:ICSE97,
  author    = {Shin Nakajima and
               Kokichi Futatsugi},
  title     = {An {Object-Oriented} Modeling Method for Algebraic Specifications in {CafeOBJ}},
  booktitle = {ICSE},
  pages     = {34--44},
  publisher = {{ACM}},
  year      = {1997},
}

Related papers