Системы управления играют решающую роль в различных областях, требующих высокой надежности и подтверждения правильности работы программного обеспечения. Для решения этой проблемы используются формальные методы, такие как дедуктивная верификация, которые математически обеспечивают корректность программного обеспечения, критически важного для безопасности. Этот процесс включает в себя генерацию условий корректности на основе аксиоматической семантики программы и ее требований. Основным недостатком ручной генерации условий корректности является ее трудоемкость и подверженность человеческим ошибкам, что приводит к разработке автоматизированных генераторов условий проверки. Однако они создают избыточные или чрезмерно сложные условия проверки, которые неточно отражают возможные пути работы программы. Для устранения второй проблемы были введены предметно-ориентированные языки, такие как Reflex, которые используют процесс-ориентированную парадигму для оптимизации программирования и упрощения генерации условий проверки. Тем не менее, присущая Reflex структура switch-case может привести к увеличению числа условий корректности, усугубляя первую проблему и усложняя выбор подходящих. В данной статье предлагается простая система статического анализа, предназначенная для оптимизации генерации условий корректности для программ Reflex, что повышает эффективность процесса верификации. Она основана на привязке атрибутов к различным операторам. Затем на протяжении всего процесса генерации условий корректности эти атрибуты собираются и проверяются на совместимость с ранее собранными. Если атрибуты несовместимы, то условия корректности отбрасываются.