Статья 469

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