Что значит «алгоритм верен»

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

Как думаешь, чего не хватает этой проверке

def maksimum(a):
    m = a[0]
    for x in a:
        if x > m:
            m = x
    return m

Функцию прогнали на [1, 5, 3], [7], [2, 2, 2] и [-4, -9] - все ответы верны. Вопрос: доказано ли, что она работает? Нет. Доказано, что она работает на четырёх входах. Утверждение «работает на всех непустых списках» из четырёх примеров не следует, и никакое конечное число примеров его не даст.

Две половины правильности

Утверждение «алгоритм верен» распадается на два независимых:

Частичная корректность. Если алгоритм завершился, его результат удовлетворяет постусловию. Слово «если» здесь существенно: программа, которая зацикливается всегда, частично корректна - она никогда не выдаёт неверного ответа, потому что не выдаёт никакого.

Завершаемость. Алгоритм завершается на любом входе, допущенном предусловием.

Вместе они дают полную корректность. Разделение не педантизм: доказывают эти две вещи разными приёмами. Частичную корректность - инвариантом: утверждением о переменных, которое верно перед каждым кругом цикла. Завершаемость - мерой: целой неотрицательной величиной, которая строго убывает на каждом круге и потому не может убывать вечно. Оба приёма разбираются дальше в этой главе, каждый своим уроком.

Разбор: три способа сломать «максимум»

Возьмём ту же функцию и посмотрим, чем именно её можно испортить.

m = 0                    # (1)
for x in a:
    if x > m:
        m = x

Строка m = 0 ломает частичную корректность на списке из отрицательных чисел: на [-4, -9] вернётся 0, а такого элемента в списке нет. Постусловие требует не «число не меньше всех», а «элемент списка, не меньший всех».

m = a[0]
for x in a[1:]:
    if x >= m:           # (2)
        m = x

Здесь всё верно: замена > на >= меняет, какой из равных максимумов запомнится, но постусловие свободу оставило. Дефекта нет - и это важно различать: не всякое изменение кода является ошибкой.

m = a[0]
i = 0
while i < len(a):        # (3)
    if a[i] > m:
        m = a[i]

А здесь ломается завершаемость: i не растёт, цикл крутится вечно. Частичная корректность при этом формально не нарушена. Пользы от неё ноль.

Разбор: контрпример как доказательство неверности

Доказать, что алгоритм верен, примерами нельзя. А доказать, что он неверен, одним примером можно - и это единственная асимметрия, которой стоит пользоваться.

Алгоритм: «чтобы разменять сумму наименьшим числом монет, бери самую крупную монету, которая не превосходит остатка». На монетах 1, 5, 10 он работает. Контрпример: монеты 1, 3, 4 и сумма 6. Жадный берёт 4, потом 1, потом 1 - итого три монеты. Оптимум - две монеты по 3.

Один вход, шесть строк рассуждения, и утверждение опровергнуто окончательно. К жадным алгоритмам и условиям, при которых они всё-таки верны, вернёмся в отдельном разделе; здесь важен приём: прежде чем доказывать, потрать минуту на поиск контрпримера. Если он находится, доказывать нечего.

Где искать контрпример

Порядок, который экономит время:

• пустой вход и вход из одного элемента;
• все элементы одинаковые;
• отсортированный вход и отсортированный в обратную сторону;
• отрицательные числа и ноль, если про знак ничего не сказано;
• совпадение с границей: элемент, равный порогу, а не больше и не меньше.

Заготовка задачи прошлой главы падала ровно на двух пунктах этого списка - «все элементы одинаковые» и «элемент, равный порогу».

Теперь сам

Алгоритм: «чтобы найти второй по величине элемент, найди максимум, удали его, найди максимум снова». Верен ли он? Если нет - предъяви контрпример.