Логика Хоара содержит набор аксиом для основных конструкций императивного языка программирования: пустой оператор, оператор присваивания, составной оператор, оператор ветвления и цикл. В них много формул и чтобы они не вызвали отторжения я задам вначале небольшую задачку.
Бинарный алгоритм возведения в степень
Рассмотрим рекурсивную версию. Будем считать задача имеет решение если 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 раз).
Хоар фактически предложил:
Давайте воспользуемся произволом при написании программ и будем их писать так, чтобы легче было доказать их корректность. В результате и программу легче написать, и доказательство корректности сразу получим.Это мои слова.
По поводу доказательства правильности алгоритма. Есть в математике набор инструментов позволяющий доказывать теоремы. Я назову общеизвестные: метод математической индукции, от противного. Так вот логика Хоара это инструмент доказательства корректности программ (правильнее частичной корректности, но это уже нюансы), который в принципе может быть использован и для доказательства корректности алгоритма, если он записан в основных конструкциях императивного программирования, для которых есть Тройки Хоара.
# -*- 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:
# -*- 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.
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
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.
Это описание на вики
# -*- 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
#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.
В википедии Логика Хоара.
Из лекций ВМиК МГУ по «Технологии программирования».
Комментарии (20)
mayorovp
01.10.2015 13:31+3Если бы я не знал троек Хоара, то бы ничего из этой статьи не понял.
Кстати, алгоритм быстрого возведения в степень куда проще объясняется при помощи инварианта, чем тройками Хоара.PavelSandovin
01.10.2015 13:38Не удивительно, последовательное изложение этой темы занимает половину семестра.
fareloz
01.10.2015 13:45+3Тогда видимл автору нужно было писать цикл статтей, а не сухую заметку на полях.
rafuck
02.10.2015 03:11А разве тут инвариант не указан в комментарии к коду?
mayorovp
02.10.2015 06:02Указан, да не совсем он. Автор определяет инвариант цикла как некоторое высказывание, верное на каждой итерации:
a0**n = r * a**n
При использовании метода инварианта, инвариант — это любое математическое выражение, которое сохраняет свое значение на каждой итерации:r * a**n = const
PavelSandovin
01.10.2015 13:41+1На лекциях по Computer Science в 1999-м году в СГУ «логику Хоара» нам преподавали под названием «теория аксиоматической верификации программ». А на практике предупреждали, что это «университетское программирование, которое в жизни не встретить и не очень нужно» :)
А Вы используете его в какого рода проектах, и в каком объеме — в каких-то критических участках кода я полагаю?
teleavtomatika
01.10.2015 14:29+4Я тут не поленился и заглянул в приведенную в начале статьи ссылку на википедию. Ваша статья скопирована из википедии чуть менее чем полностью.
teleavtomatika
01.10.2015 15:19+2Похоже, что автор не ответит. Он в глубоком нокауте: habrahabr.ru/company/pvs-studio/blog/268001/#comment_8596923
roman_kashitsyn
01.10.2015 14:54Интересующимся могу посоветовать статью про бинарный поиск из Programming Pearls Бентли (Жемчужины программирования). Бентли горячо рекомендовал The Science of Programming, предисловие к которой написал Dijkstra. Книга довольно интересная, но её сложно назвать лёгким чтивом.
GraDea
(a != 0 or n != 0) — здесь разве не and должен быть?
MaximChistov
он уже в RO :)
qw1
00 — математическая неопределённость,
01, 10 — можно вычислить