[recovery mode] Тройки Хоара Опции

[Decker]

Программирование*
Я больше 15 лет при программировании использую логику Хоара и нахожу этот подход очень полезным и хочу поделится опытом. Естественно не надо «стрелять из пушки по воробьям», но при написании достаточно сложных алгоритмов или нетривиальных кусков кода применение логики Хоара сэкономит Ваше время и позволит внести элементы некоторого «промышленного» стандарта при программировании.



Логика Хоара содержит набор аксиом для основных конструкций императивного языка программирования: пустой оператор, оператор присваивания, составной оператор, оператор ветвления и цикл. В них много формул и чтобы они не вызвали отторжения я задам вначале небольшую задачку.




Бинарный алгоритм возведения в степень


Рассмотрим рекурсивную версию. Будем считать задача имеет решение если 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

# -*- 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.

Pythondef 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-элементов состоит из двух основных шагов:

1. Выстраиваем элементы массива в виде сортирующего дерева:
   
   ∀ i, 0 ≤ i ∧ (2i+1) < n ∧ array[i] &geq; array[2i+1],
   
   ∀ i, 0 ≤ i ∧ (2i+2) < n ∧ array[i] &geq; array[2i+2].
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.



В википедии Логика Хоара.



Из лекций ВМиК МГУ по «Технологии программирования».



Original source: habrahabr.ru (comments, light).

Читать дальше