OberonCore

Фактически, формализм Хоара - это просто контекстно-свободные грамматики поведения системы. Т.е. грамматики для языка, алфавит которого - элементарные события, а слова - последовательность событий во времени.

В таких работах всегда присутствует со стороны авторов желание "сделать красиво".
А красиво -- значит, чтобы там была какая-нибудь алгебра (как дурацкие сигма-алгебры у Колмогорова в теории вероятностей) или тут, грамматика.

Когда чел видит нечто, похожее на "алгебру" или "грамматику" ... он возбуждается, и дальше уже подсознательно подгоняет проблему под этот формализм.

Опять же, и статьи можно гнать, и книги.

Ага, понятно, спасибо.

Хотя мне кажется, что попытки описать математически динамический процесс поведения программы - это не совсем то, что требуется.
Вот есть такая переводная книжка: Семантика языков программирования. Там масса математики - попытки описать семантику математическими средствами.
И есть статья Кнута о семантике контекстно-свободных языков. Где он как раз о работе аттрибутных грамматик пишет: унаследованные атрибуты, вычисляемый артибуты. Без особой математики, но в динамике на дереве.
ИМХО, гораздо ближе к истине.
Или Статья Дейкстры о взаимодействии последовательных процессов, написанная за 20 лет до Хоара, где он семафоры описывает. Или его же статья об алгоритме банкира.
Математики - ноль, а статьи - эпохальные.