In the information system industry an important direction is connected with the development of formal models for programming objects. Such models provide a basis for automated 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 existence of logical reduction are studied. The methodology is designed to verify and upgrade type hierarchies and is focused on elimination of code redundancy. Proofs of the results obtained are given for the first time.