Как доказать, что программа верна, не запуская её на всех входах? Логика Хоара отвечает тройкой {P} C {Q}: если до выполнения истинно предусловие P и команда C завершилась, после истинно постусловие Q. Сердце метода — инвариант цикла. Это прямой мост от логики к корректности.
Запись $\{P\}\ C\ \{Q\}$ читается так: если перед командой $C$ истинно предусловие $P$ и $C$ завершается, то после неё истинно постусловие $Q$. Это контракт: что требуется на входе и что гарантируется на выходе.
$\{\,x \ge 0\,\}\quad y := \sqrt{x}\quad\{\,y\cdot y = x \wedge y \ge 0\,\}$
Доказательство корректности — это вывод: показать, что из $P$ через шаги $C$ логически получается $Q$, по правилам для каждой конструкции языка.
$\{Q[x:=e]\}\ x:=e\ \{Q\}$ — чтобы после было $Q$, до должно быть $Q$ с подстановкой нового значения. Работаем «справа налево».
Из $\{P\}\,C_1\,\{R\}$ и $\{R\}\,C_2\,\{Q\}$ следует $\{P\}\,C_1;C_2\,\{Q\}$ — промежуточное условие $R$ склеивает шаги.
В каждой ветви if к предусловию добавляется условие (или его отрицание); обе ветви должны привести к одному $Q$.
$\dfrac{\{I\wedge b\}\ C\ \{I\}}{\{I\}\ \textbf{while}\ b\ \{I\wedge\neg b\}}$ — если тело сохраняет инвариант $I$, то после цикла верны $I$ и отрицание условия.
Пример: сумма чисел от 0 до n−1. Инвариант — «sum равна сумме первых i чисел». Он верен в начале (i=0, sum=0), сохраняется телом и на выходе (i=n) даёт нужный результат:
Логика Хоара доказывает программу снаружи: пишем код, затем доказываем тройку. Соответствие Карри-Ховарда из главы VII идёт дальше — встраивает утверждение прямо в тип, и тогда доказательством служит сама программа, а проверку ведёт компилятор. Это два пути к одному: программа, корректность которой установлена не испытанием, а выводом.
Обе идеи — продолжение главы о логике: корректность есть теорема, а теорему доказывают.