В индустрии программного обеспечения важную составляющую образует направление, связанное с разработкой формальных моделей автоматизируемых объектов. Такие модели создают основу для эффективной верификации и оптимизации программного кода. В настоящей работе рассматривается класс основанных на решетках алгебраических структур, описывающих семантику иерархии типов в объектно-ориентированной программной системе. Исследуются свойства таких структур, включая замкнутость, эквивалентность преобразований, существование логической редукции. Методология предназначена для верификации и модернизации иерархий типов, важным направлением которой является автоматизированное устранение избыточности кода. В результате обобщения теоретической модели получен и формализован новый метод рефакторинга - совмещение атрибутов.

Кратко обсуждаются вопросы компьютерной реализации.