Тройки Хоара

Я больше 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 раз).

Хоар фактически предложил:

Давайте воспользуемся произволом при написании программ и будем их писать так, чтобы легче было доказать их корректность. В результате и программу легче написать, и доказательство корректности сразу получим.

Это мои слова.

По поводу доказательства правильности алгоритма. Есть в математике набор инструментов позволяющий доказывать теоремы. Я назову общеизвестные: метод математической индукции, от противного. Так вот логика Хоара это инструмент доказательства корректности программ (правильнее частичной корректности, но это уже нюансы), который в принципе может быть использован и для доказательства корректности алгоритма, если он записан в основных конструкциях императивного программирования, для которых есть Тройки Хоара.

Полная версия

Разумная версия

Бинарный поиск

Попробуйте себя при решении очень похожей задачи бинарного поиска. Здесь a — линейно упорядоченный массив, v — элемент номер, которого мы ищем, l — нижняя граница с которой мы ищем (она входит), r — верхняя граница до которой мы ищем (она не входит). Для простоты предполагаем, что первый вызов bSearch не выходит за границы массива a. Возвращает -1, если не удалось найти, или номер найденного элемента >=0.

Python

C/C++

Напишите не рекурсивную версию c тройками Хоара.

Рассмотрим более сложные случае со вложенными циклами на примере разных алгоритмов сортировки.

Пирамидальная сортировка

Алгоритм пирамидальной сортировки для массива array из n-элементов состоит из двух основных шагов:

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

C/C++

Напоследок

Попробуйте себя при решении очень похожей задачи сортировки методом Шелла. 

Дан массив 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.

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

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