Уменьшение контрпримера: от тридцати отрезков до двух

Если ты умеешь автоматически уменьшать контрпример и знаешь, почему признак ошибки должен быть точным, листай до «Теперь сам».

Как думаешь, где ошибка

Функция считает длину объединения отрезков - сколько времени занят хоть один сервер. Стресс-тест нашёл расхождение с перебором на входе из тридцати отрезков от 0 до 47. Перебор говорит 44, быстрая функция - 40 (сами отрезки увидишь, если напечатаешь vhod в первой программе урока).

Где ошибка? Глядя на тридцать пар чисел, ответить невозможно (их строит генератор в первой программе урока, а 44 и 40 она печатает второй строкой). А теперь тот же дефект на двух отрезках: [1, 2) и [0, 3). Быстрая функция говорит 2, перебор - 3. Подумай до чтения, что пошло не так.

После сортировки первым идёт [0, 3), вторым - вложенный в него [1, 2). Функция «сливает» их и ставит конец объединения на конец второго - 2, хотя первый тянется до 3. Пропущен max.

На что это похоже

Поиск пробки в водопроводе. Не разбирают всю систему - перекрывают половину стояков и смотрят, течёт ли. Течёт - пробка в другой половине, нет - в этой. Делят дальше, пока не останется одна труба. Уменьшение контрпримера ищет так же: убирает куски входа и смотрит, держится ли ошибка.

Механизм: выбросить куски, уменьшить числа, держа признак

Алгоритм работает с двумя вещами: входом и признаком - функцией, которая отвечает, проявляется ли на входе та самая ошибка.

1. Выбросить куски. Попробовать удалить первую половину входа; если признак держится - удалить. Затем вторую половину, затем куски по четверти, и так до одного элемента. Это упрощённая идея алгоритма ddmin Зеллера и Хильдебрандта (2002).
2. Уменьшить числа. Каждое число пробовать заменить меньшим: сдвинуть отрезок к нулю, укоротить его. Если признак держится - оставить замену.
3. Повторять, пока что-то меняется.

Результат минимален в одну сторону относительно тех правок, которые алгоритм пробует: ни одна из них по отдельности не сохраняет ошибку. Но это верно, только если фазы повторяют, пока что-то меняется, - так делают настоящие инструменты, и правок они пробуют больше. Учебная программа ниже делает один проход «куски, потом числа» и из чисел пробует только сдвиг влево и укорачивание справа. Её результат минимален лишь относительно последней фазы: после уменьшения чисел выброс какого-то куска мог бы снова сохранить ошибку, а повторно она его не пробует. Это не обязательно самый маленький контрпример вообще, но почти всегда достаточно маленький, чтобы ошибка стала видна глазами.

Так же сжимают входы инструменты проверки свойствами - QuickCheck, Hypothesis: найдя падение, они сначала уменьшают вход и только потом показывают его человеку.

Правило

Найденный контрпример уменьшай программой: выбрасывай куски от половины до одного элемента, потом уменьшай числа, пока ошибка держится. Признак ошибки делай точным - «ошибка именно этого вида», а не «что-то не так»: иначе уменьшение уйдёт к другой ошибке.

Разбор: признак «ответы разошлись» уводит к другой ошибке

У функции две ошибки. Первая - пропущенный max при вложенном отрезке. Вторая - на пустом входе она возвращает −1 вместо 0. Стресс-тест нашёл тридцать отрезков; уменьшаем с признаком «ответы разошлись».

import random

def dlina_bystro(otrezki):
    # длина объединения отрезков [a, b) - с двумя ошибками
    if len(otrezki) == 0:
        return -1                  # ошибка 2: для пустого нужно 0
    o = sorted(otrezki)
    nach = o[0][0]
    kon = o[0][1]
    summa = 0
    for s in o[1:]:
        if s[0] <= kon:
            kon = s[1]             # ошибка 1: нужно max(kon, s[1])
        else:
            summa = summa + kon - nach
            nach = s[0]
            kon = s[1]
    return summa + kon - nach

def dlina_perebor(otrezki):
    # по определению (границы целые): сколько целых точек t покрыто
    # хоть одним [a, b)
    pokryto = set()
    for s in otrezki:
        for t in range(s[0], s[1]):
            pokryto.add(t)
    return len(pokryto)

# счётчик проверок признака - в списке: без объявления global функция
# не переприсвоит внешнюю переменную, а элемент внешнего списка изменит
vyzovov = [0]

def razoshlis(otrezki):
    vyzovov[0] = vyzovov[0] + 1
    return dlina_bystro(otrezki) != dlina_perebor(otrezki)

def umenshit(vhod, plohoj):
    # 1) выбрасываем куски: от половины списка до одного отрезка
    kusok = len(vhod) // 2
    while kusok >= 1:
        i = 0
        while i < len(vhod):
            proba = vhod[:i] + vhod[i + kusok:]
            if plohoj(proba):
                vhod = proba
            else:
                i = i + kusok
        kusok = kusok // 2
    # 2) уменьшаем числа: сдвиг влево и укорачивание, пока помогает
    menyalos = True
    while menyalos:
        menyalos = False
        for i in range(len(vhod)):
            a = vhod[i][0]
            b = vhod[i][1]
            for zamena in [[a - 1, b - 1], [a, b - 1]]:
                if zamena[0] >= 0 and zamena[1] > zamena[0]:
                    proba = vhod[:i] + [zamena] + vhod[i + 1:]
                    if plohoj(proba):
                        vhod = proba
                        menyalos = True
                        break
    return vhod

random.seed(5)
vhod = []
for k in range(30):
    a = random.randint(0, 40)
    vhod.append([a, a + random.randint(1, 10)])
print("найден стресс-тестом: 30 отрезков, разошлись:", razoshlis(vhod))
print("    перебор:", dlina_perebor(vhod), "| быстро:",
      dlina_bystro(vhod))
print("после уменьшения:", umenshit(vhod, razoshlis), "| проверок",
      vyzovov[0])

найден стресс-тестом: 30 отрезков, разошлись: True
    перебор: 44 | быстро: 40
после уменьшения: [] | проверок 3

Три проверки - и вход пуст. Первым же шагом уменьшение попробовало выбросить половину отрезков, расхождение осталось, потом вторую половину - и пустой список тоже даёт расхождение: −1 против 0. Признак «разошлись» честно выполнен, но это другая ошибка. В документации к инструментам проверки свойствами такое называют проскальзыванием (slippage): уменьшение «соскальзывает» с одной ошибки на другую, более простую. Тридцать отрезков указывали на вложенность, а результат - на пустой вход.

Разбор: точный признак держит ошибку

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

import random

def dlina_bystro(otrezki):
    # длина объединения отрезков [a, b) - с двумя ошибками
    if len(otrezki) == 0:
        return -1                  # ошибка 2: для пустого нужно 0
    o = sorted(otrezki)
    nach = o[0][0]
    kon = o[0][1]
    summa = 0
    for s in o[1:]:
        if s[0] <= kon:
            kon = s[1]             # ошибка 1: нужно max(kon, s[1])
        else:
            summa = summa + kon - nach
            nach = s[0]
            kon = s[1]
    return summa + kon - nach

def dlina_perebor(otrezki):
    # по определению (границы целые): сколько целых точек t покрыто
    # хоть одним [a, b)
    pokryto = set()
    for s in otrezki:
        for t in range(s[0], s[1]):
            pokryto.add(t)
    return len(pokryto)

vyzovov = [0]

def nedoschityvaet(otrezki):
    # признак ИМЕННО первой ошибки: вход непустой,
    # а быстрый ответ меньше верного
    vyzovov[0] = vyzovov[0] + 1
    if len(otrezki) == 0:
        return False
    return dlina_bystro(otrezki) < dlina_perebor(otrezki)

def umenshit(vhod, plohoj):
    # 1) выбрасываем куски: от половины списка до одного отрезка
    kusok = len(vhod) // 2
    while kusok >= 1:
        i = 0
        while i < len(vhod):
            proba = vhod[:i] + vhod[i + kusok:]
            if plohoj(proba):
                vhod = proba
            else:
                i = i + kusok
        kusok = kusok // 2
    # 2) уменьшаем числа: сдвиг влево и укорачивание, пока помогает
    menyalos = True
    while menyalos:
        menyalos = False
        for i in range(len(vhod)):
            a = vhod[i][0]
            b = vhod[i][1]
            for zamena in [[a - 1, b - 1], [a, b - 1]]:
                if zamena[0] >= 0 and zamena[1] > zamena[0]:
                    proba = vhod[:i] + [zamena] + vhod[i + 1:]
                    if plohoj(proba):
                        vhod = proba
                        menyalos = True
                        break
    return vhod

random.seed(5)
vhod = []
for k in range(30):
    a = random.randint(0, 40)
    vhod.append([a, a + random.randint(1, 10)])
print("найден стресс-тестом: 30 отрезков, недосчитывает:",
      nedoschityvaet(vhod))
mal = umenshit(vhod, nedoschityvaet)
print("после уменьшения:", mal, "| проверок", vyzovov[0])
print("быстро:", dlina_bystro(mal), "перебор:", dlina_perebor(mal))

найден стресс-тестом: 30 отрезков, недосчитывает: True
после уменьшения: [[1, 2], [0, 3]] | проверок 56
быстро: 2 перебор: 3

56 проверок - и два отрезка, вложенные друг в друга. Дальше уменьшать нельзя: если сдвинуть [1, 2) к нулю, он станет первым после сортировки и ошибка пропадёт; если укоротить [0, 3), он перестанет выступать за вложенный. Такой вход объясняет дефект без отладчика. Граница правила видна в обоих разборах: уменьшение находит то, что описывает признак, - не больше и не меньше. Вторая ошибка тоже настоящая, и её стоит уменьшить отдельно, своим признаком.

Что ломается без этого

Отладка по большому входу. Час с отладчиком на тридцати отрезках вместо минуты на двух.

Проскальзывание. Исправили «найденную» ошибку пустого входа, перезапустили стресс-тест - и через минуту снова падение: настоящая ошибка осталась.

Ручное уменьшение. Человек убирает элементы «на глаз», устаёт на пятой итерации и останавливается на входе из восьми элементов.

Зачем это в работе

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

Теперь сам

1. Уменьшение выбрасывает куски от половины до одного элемента. Сколько проверок потребуется в лучшем случае, чтобы из 32 элементов оставить один, если ошибку вызывает именно он? Считай по программе урока.
2. Признак: «программа упала с исключением». Почему он склонен к проскальзыванию?
3. Почему результат уменьшения не обязательно самый маленький контрпример вообще?