Коротко о сути: логика Хоара формализует доказательства корректности программ через тройки Хоара $\{P\}C\{Q\}$, где $P$ — предусловие, $C$ — команда, $Q$ — постусловие. Правила: аксиома присвоения $\{P[E/x]\}x:=E\{P\}$, правил составления, следствия (уплотнение/ослабление), правило ветвления и циклa. Для циклов ключевая конструкция — инвариант $I$ и правило (частичная корректность):
$$\text{если}\{I\wedge B\}C\{I\}\text{, то}\{I\}\text{while}B\text{do}C\{I\wedge \neg B\}.$$ Для тотальной корректности дополнительно требуется убывающий вариант (меря), показывающий завершение.
Пример (сумма первых $n$ чисел):
Программа
$$i:=0;s:=0;\text{while}(i<n)\{i:=i+1;s:=s+i\}$$ Предполагаем предусловие $n\ge 0$. Хотим получить постусловие $s=\frac{n(n+1)}{2}$.
Выберем инвариант
$$I:s=\frac{i(i+1)}{2}\wedge 0\le i\le n.$$
Проверки:
1) Инициация (после инициализаций): после $i:=0;s:=0$ имеем $i=0,s=0$, значит
$$s=\frac{0\cdot (0+1)}{2}\wedge 0\le 0\le n,$$ то есть $I$ выполняется при предусловии $n\ge 0$.
2) Сохранение (тело цикла): предположим $I\wedge i<n$. После первой команды $i:=i+1$ новое значение $i$ равно старому $i_{old}+1$; запись инварианта сразу после первой команды даёт
$$s=\frac{(i-1)i}{2}\wedge 1\le i\le n.$$ Перед второй командой имеем это как предусловие для $s:=s+i$. По аксиоме присвоения, после $s:=s+i$ $$s=\frac{(i-1)i}{2}+i=\frac{i(i+1)}{2},$$ и сохраняется $0\le i\le n$. Следовательно $I$ возвращается в конце тела.
3) Постусловие цикла: по правилу цикла из $I$ и $\neg (i<n)$ получаем
$$I\wedge \neg (i<n)\Rightarrow s=\frac{i(i+1)}{2}\wedge i\ge n.$$ В сочетании с частью $i\le n$ инварианта даёт $i=n$ и тогда $s=\frac{n(n+1)}{2}$ — требуемое постусловие.
(Для тотальной корректности добавляем меру $n-i$, которая неотрицательна и уменьшается на $1$ при каждом проходе, следовательно цикл завершается.)
Итог: доказательство корректности строится подбором инварианта $I$ и проверкой инициации, сохранения и (при необходимости) убывающей меры для завершения.