Он отстал от жизни, был политически неграмотен, и молодые конкуренты легко его побивали. Они приносили в редакции задачи с такой прекрасной идеологической установкой, что старик, читая их, плакал от зависти.
И. Ильф, Е. Петров "Золотой теленок"
В современном программировании скорость разработки ценится, пожалуй, не меньше, чем скорость работы самих получающихся программ. Очень часто программисты используют стандартные компоненты, зная, что такое решение будет заведомо неэффективным с алгоритмической точки зрения, и это вполне объяснимо. Однако понятно, что, несмотря ни на какие изменения в технологии создания программ, требование эффективности остается первичным: прежде всего программа должна работать. Не менее очевидно и то, что чем глубже мы проникнем в суть проблемы, чем лучше изучим ее свойства, тем более надежную и эффективную программу сумеем построить.
Мало кто доказывает сейчас правильность своих программ. Это очень трудоемкая и, как следствие, дорогостоящая процедура, поэтому обычно разработчики ограничиваются более или менее подробным тестированием, которое, по справедливому замечанию Э. Дейкстры, "может вполне эффективно служить для демонстрации наличия ошибок, но, к сожалению, непригодно для доказательства их отсутствия"[1]. Однако при создании сложных систем с повышенными требованиями к надежности доказывание правильности может себя окупать (см., например, [2]), так что иметь представление об этой технике не помешает.
Эта статья посвящена разбору учебной задачи, на примере которой будет продемонстрировано нахождение эффективного алгоритма, построение программы и доказывание ее правильности. Эта задача была в свое время предложена автору на занятии специального курса "Построение и анализ алгоритмов" на мехмате МГУ; здесь ее формулировка приводится по книге [3].
Имеется n одинаковых на вид камней, некоторые из которых на самом деле различны по весу. Имеется прибор, позволяющий по двум камням определить, одинаковы они или различны (но не говорящий, какой тяжелее). Известно, что среди этих камней большинство (более n/2) одинаковых. Сделав не более n взвешиваний, найти хотя бы один камень из этого большинства. (Предостережение. Если два камня одинаковые, это не гарантирует их принадлежности к большинству.)
Неформальное решение
Обратим внимание на то, что в условие задачи специально введено ограничение, мешающее применению сортировки, мысль о которой приходит в голову первой: вместо весов, позволяющих легко упорядочить камни по весу, предлагается использовать прибор, не дающий этого сделать. Логичным будет поискать решение, не связанное с сортировкой.
Основная идея решения находится не логически, а путем догадки, и сводится к следующему: если два камня различны по весу, мы можем оба исключить из рассмотрения. Действительно, общее число камней при этом сократится на два, а число камней, составляющих большинство, либо не сократится (если оба камня к нему не принадлежат), либо сократится на один (если один принадлежит) и в обоих случаях окажется больше половины числа оставшихся камней.
Итак, будем отбрасывать пары неодинаковых камней. Нельзя ли организовать соответствующую процедуру, например, так? Возьмем любой камень и будем сравнивать его с другими, пока вес не окажется различным. Если мы проверим таким образом больше половины камней, то наш камень принадлежит к большинству, если же мы раньше встретим камень другого веса, отбросим оба и проделаем ту же процедуру с оставшимися камнями.
Увы, на нахождение ответа здесь нужно более n взвешиваний: уже при n=9 их число может оказаться равным 10 (4 взвешивания для первого камня, 3 для второго, 2 для третьего и 1 для четвертого). Несложно подсчитать, что максимальное число взвешиваний для n камней в случае применения описанного алгоритма определяется формулой (n2-1)/8, т. е. он выполняется за время, пропорциональное квадрату числа обрабатываемых элементов или, как еще говорят, имеет квадратичную сложность. В задаче же требуется, чтобы время обработки было пропорционально самому числу элементов, т. е. чтобы сложность алгоритма была линейной.
Попробуем оптимизировать наш алгоритм. Воспользуемся тем, что если мы сначала сравнили первый камень со вторым, а потом с третьим и в обоих случаях вес оказался одинаковым, то нет смысла после этого отдельно сравнивать второй камень с третьим: ведь результат уже известен. Если откладывать такие камни и сравнивать любой из них с одним из еще не проверенных, то число взвешиваний не превысит n, что и требовалось.
Модифицированная процедура приобретает следующий вид. Берем любой камень и, если ни один камень не отложен, откладываем его. Если же есть отложенные, берем любой из них, сравниваем с нашим и, если вес различается, отбрасываем оба камня, а если совпадает, присоединяем их к отложенным. Когда отложенных камней станет больше, чем оставшихся, это, очевидно, будет означать, что они составляют большинство, т. е. искомый камень -- любой из отложенных.
Программа
Переведем теперь наше решение на язык программирования. В действительности он может быть почти любым; мы воспользуемся языком, который применяется в книге [4] (с заменой некоторых специальных символов на имеющиеся в стандартном наборе).
Поскольку типа данных "камень" у нас нет, заменим камни целыми числами; значения их и будут "весами камней". Не забудем, что имеем право сравнивать их только на равенство -- неравенство; впрочем, другое сравнение и не потребуется. Множество камней представим как массив (это могла бы быть и последовательность заранее известной длины).
В новой терминологии задача будет выглядеть так:
Дан непустой целочисленный массив A из M элементов, пронумерованных от 0 до M - 1. Известно, что более половины элементов имеют одно и то же значение -- назовем его доминантой (например, для M = 5, A(0) = 7, A(1) = 5, A(2) = 7, A(3) = 7, A(4) = 8 доминантой будет число 7). Необходимо составить программу нахождения доминанты массива, такую, чтобы выборка значения любого элемента производилась не более одного раза.
Прежде, чем переходить непосредственно к программе, запишем ее функциональную спецификацию. В спецификации мы должны объявить переменные, характеризующие состояние системы до и после выполнения программы (соответствующие состояния называются начальным и конечным).
Текст спецификации принято заключать в скобки |[ ]| (открывающая читается как "начать", закрывающая как "завершить"). Буквой D обозначена искомая доминанта, N -- это квантор количества: запись (N i: 0 <= i обозначает число различных значений i в интервале 0 <= i < M, для которых выполнено условие B.
|[ M: int; A(i: 0 <= i < M): array of int; d: int
{(Nj: 0 <= j < M: A(j) = D) > (Nj: 0 <= j < M: A(j) != D)}
; доминанта
{d = D}
]|
В первой строке объявляются переменные программы: M -- число элементов массива, A -- сам массив и d -- переменная, в которой после исполнения программы будет находиться доминанта. Во второй в фигурных скобках записано предусловие, т. е. условие, которому должен удовлетворять массив перед исполнением программы. Третья строка содержит имя программы, отделенное от предшествующего текста точкой с запятой, четвертая -- постусловие (условие, которое должно выполняться после завершения программы).
Запишем, кроме того, логическое выражение для инварианта основного цикла программы, т. е. условия (обозначим его P), верного как до начала выполнения цикла, так и после его окончания. Для этого нам понадобится, дополнительно к переменным, объявленным в спецификации, еще массив F для множества отложенных камней, а также целочисленные переменные m и k соответственно для текущего числа еще не взвешенных и отложенных камней.
P: 0 <= m <= M
& (A i: 0 <=i < k: F(i) = F(0))
& (N j: 0 <= j < m: A(j) = D) + (N j: 0 <= j < k: F(j) = D) >
(N j: 0 <= j < m: A(j) != D) + (N j: 0 < =j < k: F(j) != D)
Иначе говоря, число еще не проверенных камней m находится в интервале от 0 до общего числа камней M, число отложенных камней k -- в интервале от 0 до числа еще не проверенных (как только они сравняются или k превысит m, доминанта найдена и выполнение цикла можно прекращать), все k элементов множества отложенных камней (массива F) имеют один и тот же вес, а общее число камней, имеющих вес D (отложенных и еще не проверенных), больше числа камней, имеющих другой вес.
Воспользовавшись тем, что вес всех отложенных камней одинаков, введем для него целочисленную переменную f.
Наконец, запишем саму программу. Комментарии пишутся в фигурных скобках.
В начале работы ни один камень не проверен (все числа находятся в массиве A; m = M) и ни один не отложен (массив F пуст; k = 0, значение f не определено). Значение m уменьшается на единицу, когда мы берем камень для проверки, т. е. при каждом выполнении цикла.
Когда массив F пуст (k = 0), мы не выполняем сравнение, а просто перемещаем очередной элемент из A в F, т. е. присваиваем его значение переменной f, а k становится равным 1. Когда F не пуст, мы сравниваем очередной элемент A с f и в зависимости от результата отбрасываем или откладываем наш камень -- уменьшаем или увеличиваем на единицу значение k.
|[ m, f, k: int; m, k := M, 0
{P стало истинным}
do m > k ->
|[ a: int; a := A(m - 1)
; if k = 0 -> f := a; k := 1
[] k > 0 -> if a = f -> k := k+1
[] a != f -> k := k - 1
fi
fi
; m := m - 1
]|
od
{P истинно и m < =k -- заканчиваем работу}
; d := f
{d=D}
]|
Интересно, что в результате массив для отложенных камней нам не понадобился -- хватило переменных f и k.
Доказательство правильности
Докажем теперь правильность нашей программы. Для этого необходимо показать, во-первых, что инвариант цикла остается истинным при всех преобразованиях, которые выполняются в процессе работы (сохранение инварианта), а во-вторых, что эта работа рано или поздно завершится (сходимость программы). Начнем с сохранения инварианта.
При k = 0, а также при a = f мы просто перемещаем элемент из A в F. При этом истинность P, очевидно, сохраняется. Подробно имеет смысл разбирать только последний случай -- a! = f, когда мы исключаем по элементу из A и из F. Покажем, что и здесь P останется истинным, рассмотрев последовательно члены P.
0 <= m <= M
Если P было истинным до начала выполнения тела цикла, то значение m не превышало M, а при выполнении m := m - 1 оно могло только уменьшиться. Однако m не могло стать меньше 0, поскольку m было больше k, а k было положительным (сравнение выполняется только при положительном k).
0 <= k < m
Так как неравенство k < m было верным перед присваиванием k := k - 1 и m := m - 1, оно будет верно и после этого. Значение k уменьшается на единицу только при положительном k, поэтому неравенство 0 <= k также останется истинным.
(A i: 0 <= i < k: F(i) = F(0))
Все элементы F были равны, и новые элементы к F не добавлялись, поэтому истинность этого члена также сохраняется.
(N j: 0 <= j < m: A(j) = D) + (N j: 0 <= j (N j: 0 <= j < m: A(j) != D) + (N j: 0 <= j < k: F(j) != D)
Поскольку a != f, из утверждений a = D и f = D истинным может быть не более чем одно. Если a != D и f != D, правый член неравенства уменьшается на 2, а левый не меняется, следовательно, неравенство сохраняется. При a = D и f != D, а также при a! = D и f = D оба члена неравенства уменьшаются на 1 и оно также сохраняется.
Таким образом, все конъюнктивные члены утверждения P останутся истинными после уменьшения k и m на единицу, следовательно, оно тоже останется истинным.
Рассмотрим теперь вопрос о сходимости. В качестве критерия сходимости удобно рассмотреть значение переменной m. Перед каждым выполнением тела цикла m > k, а поскольку k >= 0, то m > 0. При каждом таком выполнении значение m уменьшается на 1 и, если бы программа зациклилась, оно в какой-то момент стало бы меньше 0. Таким образом, мы пришли к противоречию. Следовательно, выполнение программы обязательно завершится.
Примечание 1. Можно преобразовать конструкцию выбора:
if k = 0 -> f := a; k := 1
[] k > 0 -> if a = f -> k := k + 1
[] a!=f -> k := k - 1
fi
fi
к другому виду. Для начала вынесем наружу проверку на равенство переменных a и f:
if k = 0 -> f := a; k := 1
[] k > 0 & a = f -> k := k + 1
[] k > 0 & a != f -> k := k - 1
fi
Теперь заменим в первой команде k := 1 на k := k+1 (мы можем это сделать, поскольку условие выполнения команды -- k = 0) и разобьем ее на две, добавив сравнение переменных a и f:
if k = 0 & a! = f -> f := a; k := k + 1
[] k = 0 & a=f -> f := a; k := k + 1
[] k > 0 & a=f -> k := k + 1
[] k > 0 & a != f -> k := k - 1
fi
Из второй строки, очевидно, можно убрать присваивание f := a -- оно выполняется при условии a=f и, значит, ничего не изменит. После этого мы можем объединить ее с третьей строкой, причем выражение k = 0 | k > 0 опускается, поскольку k >= 0 по условию P:
if k = 0 & a != f -> f := a; k := k + 1
[] a=f -> k := k + 1
[] k > 0 & a != f -> k := k - 1
fi
Поменяв местами две первые строки и занеся внутрь проверку k на равенство с нулем, получим следующее:
if a = f -> k := k + 1
[] a != f -> if k = 0 -> f := a; k := 1
[] k > 0 -> k := k - 1
fi
fi
Примечание 2. Если доминанты не существует, программа все равно завершит работу, но найденное ею значение будет бессмысленным. Однако если мы не знаем, имеет ли массив доминанту, то, поочередно сравнив его элементы с найденным значением, мы сможем это выяснить.
Использованная литература
1. Э. Дейкстра. Дисциплина программирования. М:"Мир", 1978, с. 40.
2. Дж.П. Боуэн, М.Дж. Хинчи. Десять заповедей формальных методов. "Мир ПК", N 6/97, 7/97.
3. А. Шень. Программирование: теоремы и задачи. М:"???", 1996, с.
4. Edsger W. Dijkstra, W.H.J. Fejjen. A Method of Programming. Addison-Wesley, 1988.