Я больше 15 лет при программировании использую логику Хоара и нахожу этот подход очень полезным и хочу поделится опытом. Естественно не надо «стрелять из пушки по воробьям», но при написании достаточно сложных алгоритмов или нетривиальных кусков кода применение логики Хоара сэкономит Ваше время и позволит внести элементы некоторого «промышленного» стандарта при программировании.
Логика Хоара содержит набор аксиом для основных конструкций императивного языка программирования: пустой оператор, оператор присваивания, составной оператор, оператор ветвления и цикл. В них много формул и чтобы они не вызвали отторжения я задам вначале небольшую задачку.
Рассмотрим рекурсивную версию. Будем считать задача имеет решение если a, n одновременно не равны нулю и n >= 0.
Я не люблю псеводок��д (возможно напишу отдельный топик почему), поэтому приведу пример решения на Python:
И на C/C++:
Теперь попробуйте написать не рекурсивную версию. В случае удачи попробуйте объяснить кому-нибудь как она работает.
Основная идея Хоара дать для каждой конструкции императивного языка пред и постусловие записанное в виде логической формулы. Поэтому и возникает в названии тройка — предусловие, конструкция языка, постусловие.
Правильно работающую программу можно написать очень многими способами, а также она в большом количестве случаев будет эффективной. Этот произвол и именно он усложняет программирование. Для этого вводят стиль. Но этого оказывается мало. Для многих программ (например, связанных косвенно с жизнью человека) нужно доказать и их корректность. Оказалось, что доказательство корректности делает программу дороже на порядок (примерно в 10 раз).
Хоар фактически предложил:
По поводу доказательства правильности алгоритма. Есть в математике набор инструментов позволяющий доказывать теоремы. Я назову общеизвестные: метод математической индукции, от противного. Так вот логика Хоара это инструмент доказательства корректности программ (правильнее частичной корректности, но это уже нюансы), который в принципе может быть использован и для доказательства корректности алгоритма, если он записан в основных конструкциях императивного программирования, для которых есть Тройки Хоара.
Попробуйте себя при решении очень похожей задачи бинарного поиска. Здесь a — линейно упорядоченный массив, v — элемент номер, которого мы ищем, l — нижняя граница с которой мы ищем (она входит), r — верхняя граница до которой мы ищем (она не входит). Для простоты предполагаем, что первый вызов bSearch не выходит за границы массива a. Возвращает -1, если не удалось найти, или номер найденного элемента >=0.
Напишите не рекурсивную версию c тройками Хоара.
Рассмотрим более сложные случае со вложенными циклами на примере разных алгоритмов сортировки.
Алгоритм пирамидальной сортировки для массива array из n-элементов состоит из двух основных шагов:
Это оригинальная статья автора алгоритма.
J. W. J. Williams. Algorithm 232 — Heapsort, 1964, Communications of the ACM 7(6): 347–348.
Это описание на вики
Попробуйте себя при решении очень похожей задачи сортировки методом Шелла.
Дан массив array из n-элементов. Массив разбивается на подмассивы с шагом k0
{a[0], a[k0], a[2k0], … }, {a[1], a[1+k0], a[1+2k0], … }, …, {a[k0-1], a[2k0-1], a[3k0-1], … }
и если соседние элементы в подмассиве нарушают порядок, то они меняются местами. Затем процедура повторяется с шагом k1 и т.д.
Последний шаг должен быть равен 1.
В качестве шагов можно взять, например, следующую последовательность
steps[16] = [1391376, 463792, 198768, 86961, 33936, 13776, 4592, 1968, 861, 336, 112, 48, 21, 7, 3, 1 ].
Это оригинальная статья автора алгоритма.
Donald Lewis Shell, A High-Speed Sorting Procedure, CACM, 2(7): 30-32, July 1959.
Это основная книга на русском
O.-J. Dahl, E. W. Dijkstra and C. A. R. Hoare, Structured Programming. Academic Press, 1972. ISBN 0-12-200550-3. Перевод: Дал У., Дейкстра Э., Хоор К., Структурное программирование. М.:«Мир», 1975.
Это первоначальная статья
C. A. R. Hoare. «An axiomatic basis for computer programming». Communications of the ACM, 12(10):576—580,583 October 1969. DOI:10.1145/363235.363259
С.А. Абрамов. Элементы программирования. — М.: Наука, 1982. С. 85-94.
В википедии Логика Хоара.
Из лекций ВМиК МГУ по «Технологии программирования».
Логика Хоара содержит набор аксиом для основных конструкций императивного языка программирования: пустой оператор, оператор присваивания, составной оператор, оператор ветвления и цикл. В них много формул и чтобы они не вызвали отторжения я задам вначале небольшую задачку.
Бинарный алгоритм возведения в степень
Рассмотрим рекурсивную версию. Будем считать задача имеет решение если a, n одновременно не равны нулю и n >= 0.
Я не люблю псеводок��д (возможно напишу отдельный топик почему), поэтому приведу пример решения на Python:
def power(a, n):
assert n > 0 or (a != 0 or n != 0)
if n == 0:
return 1
else:
a2 = power(a, n/2)
if n & 1:
return a*a2*a2
else:
return a2*a2
И на C/C++:
int power(int a, int n) {
assert(n > 0 || (a != 0 || n != 0));
if (n == 0)
return 1;
else {
int a2 = power(a, n/2);
if (n & 1)
return a*a2*a2;
else
return a2*a2;
}
}
Теперь попробуйте написать не рекурсивную версию. В случае удачи попробуйте объяснить кому-нибудь как она работает.
Основная идея Хоара дать для каждой конструкции императивного языка пред и постусловие записанное в виде логической формулы. Поэтому и возникает в названии тройка — предусловие, конструкция языка, постусловие.
- Ясно, что для пустого оператора пред и постусловия совпадают.
- Для оператора присваивания в постусловие кроме предусловия должно учитывать факт, что значение переменной стало другим.
- Для составного оператора (в Python это отступы, в C это {}) имеем цепочку пред и постусловий . В результате для составного оператора можно оставить первое предусловие и последнее постусловие.
- Правило вывода говорит, что можно усилить пред и ослабить постусловие если нам это понадобиться. Нет смысла волочь через всю программу какое-то утверждение, которое не помогает решить поставленную задачу.
- Оператор ветвления или просто if. Его условно можно разбить на две ветки then и else. Если к предусловию добавить истинность логического условия (то, что стоит под if), то после выполнения ветки then должно следовать постусловие. Аналогично, если к предусловию добавить отрицание логического условия (то, что стоит под if), то после выполнения ветки else должно следовать постусловие
- Оператор цикла. Это самое нетривиальное и сложное, поскольку цикл может выполняется много раз и даже не окончится. Чтобы решить проблему возможно многократного повтора тела цикла вводят инвариант цикла. Инвариант цикла это то, что истинно перед его выполнением, истинно после каждого выполнения тела цикла и следовательно истинно и после его окончания. Предусловие для оператора цикла это просто его инвариант цикла. Если истинно условие продолжения цикла (то, что стоит под while), то после выполнения тела цикла долж��а следовать истинность инвариант цикла. В результате после окончания цикла имеем в качестве постусловия истинность инвариант цикла и отрицание условия продолжения цикла.
- Оператора цикла с полной корректностью. Для этого к предыдущему пункту добавляют ограничивающую функцию, с помощью которой легко доказать, что цикл будет выполнятся ограниченное число раз. На нее накладывают условия, что она всегда >=0, строго убывает после каждого выполнения тела цикла и в точности =0, когда цикл заканчивается.
Правильно работающую программу можно написать очень многими способами, а также она в большом количестве случаев будет эффективной. Этот произвол и именно он усложняет программирование. Для этого вводят стиль. Но этого оказывается мало. Для многих программ (например, связанных косвенно с жизнью человека) нужно доказать и их корректность. Оказалось, что доказательство корректности делает программу дороже на порядок (примерно в 10 раз).
Хоар фактически предложил:
Давайте воспользуемся произволом при написании программ и будем их писать так, чтобы легче было доказать их корректность. В результате и программу легче написать, и доказательство корректности сразу получим.Это мои слова.
По поводу доказательства правильности алгоритма. Есть в математике набор инструментов позволяющий доказывать теоремы. Я назову общеизвестные: метод математической индукции, от противного. Так вот логика Хоара это инструмент доказательства корректности программ (правильнее частичной корректности, но это уже нюансы), который в принципе может быть использован и для доказательства корректности алгоритма, если он записан в основных конструкциях императивного программирования, для которых есть Тройки Хоара.
Полная версия
Я включил пред и постусловия в комментарии. Перед циклом я определяю через : инвариант_цикла и ограничивающая_функция и потом на них просто ссылаюсь. Python:
C/C++:
# -*- coding: utf-8 -*-
# Бинарный алгоритм возведения в степень
def power(a, n):
"""
Возводит a в степень n
"""
assert n > 0 or (a != 0 or n != 0)
r, a0, n0 = 1, a, n
# r == 1 and a0 == a and n0 == n and n >= 0
# инвариант_цикла: a0**n0 == r*a**n
# ограничивающая_функция(n): n
while n > 0:
# n > 0 and
# ограничивающая_функция(n) > 0 and
# инвариант_цикла
if n & 1:
r *= a
#(n - нечетно and a0**n0*a == r*a**n) or
# инвариант_цикла
n >>= 1
# ограничивающая_функция(n) > ограничивающая_функция(n/2) and
# a0**n0 == r*a**(2*n)
a *= a
# инвариант_цикла
# n == 0 and
# инвариант_цикла and
# ограничивающая_функция(n) == 0
# a0**n0 == r
return r
if __name__ == '__main__':
for i in range(14):
print "2**%d" % i ,"=", power(2, i)
print "2**%d" % i ,"=", power(-2, i)
C/C++:
#include <cassert>
#include <cstdlib>
#include <iostream>
// Бинарный алгоритм возведения в степень
int power(int a, int n) {
// Возводит a в степень n
assert(n > 0 || (a != 0 || n != 0));
int r = 1,
a0 = a,
n0 = n;
/* r == 1 and a0 == a and n0 == n and n >= 0
инвариант_цикла: a0**n0 == r*a**n
ограничивающая_функция(n): n */
while(n > 0) {
/* n > 0
and ограничивающая_функция(n) > 0
and инвариант_цикла */
if (n & 1)
r *= a;
/* (n - нечетно and a0**n0*a == r*a**n)
or инвариант_цикла */
n >>= 1;
/* ограничивающая_функция(n) > ограничивающая_функция(n/2) and
a0**n0 == r*a**(2*n) */
a *= a;
// инвариант_цикла
}
/* n == 0
and инвариант_цикла
and ограничивающая_функция(n) == 0 */
// a0**n0 == r
return r;
}
int main(int argc, char *argv[]) {
for(int i=0; i < 14; i++) {
std::cout << "2**" << i << " = " << power(2, i) << std::endl;
std::cout << "(-2)**" << i << " = " << power(-2, i) << std::endl;
}
return EXIT_SUCCESS;
}
Разумная версия
Ясно, что так подробно писать при обычном программирование нет смысла. Слишком громоздко, код захламляется комментариями и становится практически не читаемым. Все эти логические рассуждения нужно проводить у себя в голове, оставляя наиболее нетривиальные в виде комментариев. Тогда можно будет всегда при возвращении к коду быстро все рассуждения восстановить и самое главное. Другое программист владеющий этим подходом, точно также рассуждая и рассматривая Ваш код с оставленными наиболее важными комментариями сможет восстановить Ваши рассуждения и например найти в них ошибку или изменить код для новой постановки задачи. А это уже элементы промышленного подхода.
Самым важным и нетривиальным в примере с бинарным возведением в степень был инвариант цикла. Я бы написал следующим образом.
Python:
C/C++:
a0, n0 — это начальные значения. Внутри тела цикла r, a, n меняются таким образом, чтобы после выполнения тела цикла соотношение (инвариант цикла) a0**n0 == r*a**n было истинным. По окончание цикла a0**n0 == r*a**n истинно и n==0 значит a0**n0 == r и в r содержится ответ.
Написание утверждений в комментариях это конечно вопрос соглашения, но я не вижу смысла писать где-то еще. Утверждение лучше писать в комментариях непосредственно в том коде к которому они имеют непосредственное отношение и иногда, если можно, то их лучше заменять assert-ами.
Самым важным и нетривиальным в примере с бинарным возведением в степень был инвариант цикла. Я бы написал следующим образом.
Python:
# -*- coding: utf-8 -*-
# Бинарный алгоритм возведения в степень
def power(a, n):
"""
Возводит a в степень n
"""
assert n > 0 or (a != 0 or n != 0)
r = 1
# инвариант_цикла: a0**n0 == r*a**n
while n > 0:
if n & 1:
r *= a
n >>= 1
a *= a
return r
if __name__ == '__main__':
for i in range(14):
print "2**%d" % i ,"=", power(2, i)
print "2**%d" % i ,"=", power(-2, i)
C/C++:
#include <cassert>
#include <cstdlib>
#include <iostream>
// Бинарный алгоритм возведения в степень
int power(int a, int n) {
// Возводит a в степень n
assert(n > 0 || (a != 0 || n != 0));
int r = 1;
// инвариант_цикла: a0**n0 == r*a**n
while(n > 0) {
if (n & 1)
r *= a;
n >>= 1;
a *= a;
}
return r;
}
int main(int argc, char *argv[]) {
for(int i=0; i < 14; i++) {
std::cout << "2**" << i << " = " << power(2, i) << std::endl;
std::cout << "(-2)**" << i << " = " << power(-2, i) << std::endl;
}
return EXIT_SUCCESS;
}
a0, n0 — это начальные значения. Внутри тела цикла r, a, n меняются таким образом, чтобы после выполнения тела цикла соотношение (инвариант цикла) a0**n0 == r*a**n было истинным. По окончание цикла a0**n0 == r*a**n истинно и n==0 значит a0**n0 == r и в r содержится ответ.
Написание утверждений в комментариях это конечно вопрос соглашения, но я не вижу смысла писать где-то еще. Утверждение лучше писать в комментариях непосредственно в том коде к которому они имеют непосредственное отношение и иногда, если можно, то их лучше заменять assert-ами.
Бинарный поиск
Попробуйте себя при решении очень похожей задачи бинарного поиска. Здесь a — линейно упорядоченный массив, v — элемент номер, которого мы ищем, l — нижняя граница с которой мы ищем (она входит), r — верхняя граница до которой мы ищем (она не входит). Для простоты предполагаем, что первый вызов bSearch не выходит за границы массива a. Возвращает -1, если не удалось найти, или номер найденного элемента >=0.
Python
def bSearch(a, v, l, r):
if l >= r:
return -1
else:
m = (l + r)/2
assert l <= m < r
if v > a[m]:
return bSearch(a, v, m + 1, r)
elif v < a[m]:
return bSearch(a, v, l, m)
else:
assert v == a[m]
return m
C/C++
int bSearch(int *a, int v, int l, int r) {
if (l >= r)
return -1;
else {
int m=(l + r)/2;
assert(l <= m && m < r);
if (v > a[m])
return bSearch(a, v, m + 1, r);
else if (v < a[m])
return bSearch(a, v, l, m);
else {
assert(v == a[m]);
return m;
}
}
}
Напишите не рекурсивную версию c тройками Хоара.
Рассмотрим более сложные случае со вложенными циклами на примере разных алгоритмов сортировки.
Пирамидальная сортировка
Алгоритм пирамидальной сортировки для массива array из n-элементов состоит из двух основных шагов:
- Выстраиваем элементы массива в виде сортирующего дерева:
∀ i, 0 ≤ i ∧ (2i+1) < n ∧ array[i] ≥ array[2i+1],
∀ i, 0 ≤ i ∧ (2i+2) < n ∧ array[i] ≥ array[2i+2]. - Будем удалять элементы из корня по одному за раз и перестраивать дерево. Т.е. на первом шаге обмениваем array[0] и array[n-1] и преобразовываем array[0], …, array[n-2] в сортирующее дерево. Затем переставляем array[0] и array[n-2] и преобразовываем array[0], …, array[n-3] в сортирующее дерево. Процесс продолжается до тех пор, пока в сортирующем дереве не останется один элемент. Тогда array[0], …, array[n-1] — упорядоченная последовательность.
Это оригинальная статья автора алгоритма.
J. W. J. Williams. Algorithm 232 — Heapsort, 1964, Communications of the ACM 7(6): 347–348.
Это описание на вики
Python
# -*- coding: utf-8 -*-
# Cортирует a в порядке возврастания
def heapsort(a):
"""
Cортирует a применяя алгоритм пирамидальной сортировки
"""
k, n = 1, len(a)
# k == 1 and
# инвариант_цикла1: a[(i - 1)/2] >= a[i] для i=1..k
# ограничивающая_функция1(k, n): n - k
while k < n:
# k < n
# and инвариант_цикла1
# and ограничивающая_функция1(k, n) > 0
leaf = k
k += 1
# k <= n
# and инвариант_цикла1 кроме i == leaf
# and ограничивающая_функция1(k, n) > ограничивающая_функция1(k+1, n)
# инвариант_цикла2: инвариант_цикла1 кроме i == leaf
# ограничивающая_функция2(leaf): (инвариант_цикла1 то 0) иначе leaf-1
while leaf > 0:
# leaf > 0
# and инвариант_цикла2
# and ограничивающая_функция2(leaf) > 0
root = (leaf - 1)/2
if a[root] >= a[leaf]:
# инвариант_цикла2
# and инвариант_цикла1
# and ограничивающая_функция(child) == 0
break
else:
a[root], a[leaf] = a[leaf], a[root]
leaf = root
# ограничивающая_функция2(leaf) > ограничивающая_функция2((leaf - 1)/2)
# and инвариант_цикла2
# инвариант_цикла2
# and ограничивающая_функция2(child) == 0
# инвариант_цикла1
# k == n
# and инвариант_цикла1
# and ограничивающая_функция1(k, n) == 0
# инвариант_цикла3: a[(i - 1)/2] >= a[i] для i=1..k
# and a[j-1] <= a[j] для j=k..n
# and a[m] <= a[l] для m=0..k, l=k..n
# ограничивающая_функция3(k): k - 1
while k > 0:
# k > 0
# and инвариант_цикла3
# and ограничивающая_функция3(k) > 0
# and a[0] >= a[i] для i=0..k
k -= 1
a[k], a[0] = a[0], a[k]
# инвариант_цикла3 кроме i=0
# and ограничивающая_функция3(k) > ограничивающая_функция3(k-1)
root = 0
# инвариант_цикла4: инвариант_цикла3 кроме i=root
# ограничивающая_функция4(root, k): (инвариант_цикла3 то 0) иначе (k-(2*root+1))
while 2*root + 1 < k:
# 2*root + 1 < k
# and инвариант_цикла4
# and ограничивающая_функция4(root, k) > 0
leaf = 2*root + 1
# инвариант_цикла4
# and leaf == 2*root + 1
if (leaf + 1) < k and a[leaf] < a[leaf + 1]:
leaf += 1
# инвариант_цикла4
# and (2*((leaf-1)/2)+2 == k
# or a[leaf] == max(a[2*((leaf-1)/2)+1], a[2*((leaf-1)/2)+2]))
if a[root] >= a[leaf]:
# инвариант_цикла4
# and инвариант_цикла3
# and ограничивающая_функция4(root, k) == 0
break
else:
a[root], a[leaf] = a[leaf], a[root]
root = leaf
# инвариант_цикла4
# and ограничивающая_функция4(root, k) > ограничивающая_функция4(2*root + 1, k)
# инвариант_цикла4
# and ограничивающая_функция4(root, k) == 0
# инвариант_цикла3
# k == 0
# and инвариант_цикла3
# and ограничивающая_функция3(k) == 0
# a[j-1] <= a[j] для j=0..n
if __name__ == '__main__':
import random
a = map(lambda x: random.randint(-100, 100), range(20))
print a
heapsort(a)
print a
C/C++
#include <cassert>
#include <cstdlib>
#include <ctime>
#include <iostream>
// Cортирует a в порядке возврастания
void sortHeap(int *a, int n) {
// Cортирует a применяя алгоритм пирамидальной сортировки
assert(n >= 0);
int k = 1;
/* k == 1 and
инвариант_цикла1: a[(i - 1)/2] >= a[i] для i=1..k
ограничивающая_функция1(k, n): n - k */
while(k < n) {
/* k < n
and инвариант_цикла1
and ограничивающая_функция1(k, n) > 0 */
int leaf = k;
++k;
/* k <= n
and инвариант_цикла1 кроме i == leaf
and ограничивающая_функция1(k, n) > ограничивающая_функция1(k+1, n) */
/* инвариант_цикла2: инвариант_цикла1 кроме i == leaf
ограничивающая_функция2(leaf): (инвариант_цикла1 то 0) иначе leaf-1 */
while(leaf > 0) {
/* leaf > 0
and инвариант_цикла2
and ограничивающая_функция2(leaf) > 0 */
int root = (leaf - 1)/2;
if (a[root] >= a[leaf])
/* инвариант_цикла2
and инвариант_цикла1
and ограничивающая_функция(child) == 0 */
break;
else {
int tmp = a[root];
a[root] = a[leaf];
a[leaf] = tmp;
leaf = root;
/* ограничивающая_функция2(leaf) > ограничивающая_функция2((leaf - 1)/2)
and инвариант_цикла2*/
}
/* инвариант_цикла2
and ограничивающая_функция2(child) == 0 */
}
// инвариант_цикла1
}
/* k == n
and инвариант_цикла1
and ограничивающая_функция1(k, n) == 0 */
/* инвариант_цикла3: a[(i - 1)/2] >= a[i] для i=1..k
and a[j-1] <= a[j] для j=k..n
and a[m] <= a[l] для m=0..k, l=k..n
ограничивающая_функция3(k): k - 1 */
while(k > 0) {
/* k > 0
and инвариант_цикла3
and ограничивающая_функция3(k) > 0
and a[0] >= a[i] для i=0..k */
--k;
int tmp = a[k];
a[k] = a[0];
a[0] = tmp;
/* инвариант_цикла3 кроме i=0
and ограничивающая_функция3(k) > ограничивающая_функция3(k-1) */
int root = 0;
/* инвариант_цикла4: инвариант_цикла3 кроме i=root
ограничивающая_функция4(root, k): (инвариант_цикла3 то 0) иначе (k-(2*root+1)) */
while(2*root + 1 < k) {
/* 2*root + 1 < k
and инвариант_цикла4
and ограничивающая_функция4(root, k) > 0 */
int leaf = 2*root + 1;
/* инвариант_цикла4
and leaf == 2*root + 1 */
if ((leaf + 1) < k and a[leaf] < a[leaf + 1])
leaf += 1;
/* инвариант_цикла4
and (2*((leaf-1)/2)+2 == k
or a[leaf] == max(a[2*((leaf-1)/2)+1], a[2*((leaf-1)/2)+2])) */
if (a[root] >= a[leaf])
/* инвариант_цикла4
and инвариант_цикла3
and ограничивающая_функция4(root, k) == 0 */
break;
else {
int tmp = a[root];
a[root] = a[leaf];
a[leaf] = tmp;
root = leaf;
/* инвариант_цикла4
and ограничивающая_функция4(root, k) > ограничивающая_функция4(2*root + 1, k) */
}
/* инвариант_цикла4
and ограничивающая_функция4(root, k) == 0 */
}
// инвариант_цикла3
}
/* k == 0
and инвариант_цикла3
and ограничивающая_функция3(k) == 0 */
// a[j-1] <= a[j] для j=0..n
}
int main(int argc, char *argv[]) {
srand((unsigned)time(NULL));
const int n = 20;
int a[n];
for(int i=0; i < 20; i++)
a[i] = rand()/(RAND_MAX/200) - 100;
for(int i=0; i < 20; i++)
std::cout << a[i] << ' ';
std::cout << std::endl;
sortHeap(a, n);
for(int i=0; i < 20; i++)
std::cout << a[i] << ' ';
std::cout << std::endl;
return EXIT_SUCCESS;
}
Напоследок
Попробуйте себя при решении очень похожей задачи сортировки методом Шелла.
Дан массив array из n-элементов. Массив разбивается на подмассивы с шагом k0
{a[0], a[k0], a[2k0], … }, {a[1], a[1+k0], a[1+2k0], … }, …, {a[k0-1], a[2k0-1], a[3k0-1], … }
и если соседние элементы в подмассиве нарушают порядок, то они меняются местами. Затем процедура повторяется с шагом k1 и т.д.
Последний шаг должен быть равен 1.
В качестве шагов можно взять, например, следующую последовательность
steps[16] = [1391376, 463792, 198768, 86961, 33936, 13776, 4592, 1968, 861, 336, 112, 48, 21, 7, 3, 1 ].
Это оригинальная статья автора алгоритма.
Donald Lewis Shell, A High-Speed Sorting Procedure, CACM, 2(7): 30-32, July 1959.
Литература
Это основная книга на русском
O.-J. Dahl, E. W. Dijkstra and C. A. R. Hoare, Structured Programming. Academic Press, 1972. ISBN 0-12-200550-3. Перевод: Дал У., Дейкстра Э., Хоор К., Структурное программирование. М.:«Мир», 1975.
Это первоначальная статья
C. A. R. Hoare. «An axiomatic basis for computer programming». Communications of the ACM, 12(10):576—580,583 October 1969. DOI:10.1145/363235.363259
С.А. Абрамов. Элементы программирования. — М.: Наука, 1982. С. 85-94.
В википедии Логика Хоара.
Из лекций ВМиК МГУ по «Технологии программирования».
