Domain-specific Semantics and Data Refinement of Object Models

This paper shows how a domain-specific semantics for object models can be used to support the development of transformations that reflect a particular implementation strategy. The semantics captures model constraints and domain assumptions in terms of abstract data types, and a transformation is correct if and only if it corresponds to a data refinement. The transformations represent development steps, involving the completion of method descriptions, and validity checks, addressing issues of definedness and consistency. The paper shows how compositions of transformations may be used for the automatic generation of working systems from formal, object-oriented designs.