In the software industry an important direction is connected with the development of formal models for automated objects. Such models provide a basis for effective verification and optimization of the program code. In this paper a class of lattice-based algebraic structures describing semantics of a type hierarchy in an object-oriented system is considered. The properties of such structures, including closedness, equivalent transformations, and existence of logical reduction are studied. The methodology is designed to verify and upgrade type hierarchies and is focused on automatic elimination of code redundancy. As a result of the generalized theoretical model a new refractoring method of attribute joining is obtained and formalized.

Implementation issues are briefly discusses.