Свойства вместо примеров: инварианты и метаморфные отношения

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

Как думаешь, как это проверить

Новый алгоритм маршрутизации на графе из миллиона вершин. Перебора нет, сертификата алгоритм не выдаёт, правильных ответов не знает никто. Можно ли поймать его на ошибке?

Ответь себе до чтения. Можно, если сравнивать не ответ с эталоном, а ответы между собой. Добавь в граф ребро - кратчайший путь не может удлиниться, ведь все старые пути на месте. Увеличь все веса вдвое - путь обязан удвоиться. Ни одного правильного ответа знать не нужно: нарушение отношения само доказывает ошибку.

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

Проверка весов в магазине без эталонной гири. Положи пакет - 2 кг. Положи два таких пакета - должно быть 4. Положи пакет на другую чашу - должно быть те же 2. Ни одна проверка не говорит, сколько пакет весит на самом деле, но если два пакета весят 5, весы врут - это видно без гири.

Механизм: три вида свойств

Инвариант - условие на внутреннее состояние структуры, верное после каждой операции: у кучи родитель не больше детей, у дерева поиска левое поддерево меньше узла, у АВЛ-дерева высоты поддеревьев отличаются не больше чем на 1 (у красно-чёрного инвариант свой - про цвета и чёрную высоту). Проверка инварианта после каждой операции ловит ошибку в той операции, которая её внесла, а не там, где она впервые испортила ответ.

Свойство ответа - верное для любого входа: результат сортировки упорядочен, decode(encode(x)) = x, повторная сортировка ничего не меняет. Инструменты проверки свойствами - QuickCheck для Haskell (Классен и Хьюз, 2000), Hypothesis для Python - генерируют входы, проверяют свойство и уменьшают найденный контрпример, как в прошлом уроке.

Метаморфное отношение - связь ответов на два входа, полученных один из другого: f(вход) и f(изменённый вход). Для кратчайшего пути: умножение весов умножает ответ; новое ребро не удлиняет; переименование вершин не меняет длину, а путь переименовывает вместе с вершинами. Для поиска: добавление в список элемента, который не подходит под запрос, не меняет набор найденного. Идею назвали метаморфным тестированием Чен, Чунг и Ю (1998) - для задач, где правильный ответ неизвестен.

Правило

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

Разбор: инвариант кучи указывает на виновника

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

import random

def vverh(h, i):
    while i > 0 and h[(i - 1) // 2] > h[i]:
        r = (i - 1) // 2
        t = h[r]
        h[r] = h[i]
        h[i] = t
        i = r

def vniz(h, i):
    # ошибка: спускаемся всегда в левого ребёнка, а не в меньшего
    while 2 * i + 1 < len(h):
        c = 2 * i + 1
        if h[c] >= h[i]:
            return
        t = h[c]
        h[c] = h[i]
        h[i] = t
        i = c

def dostat(h):
    m = h[0]
    h[0] = h[len(h) - 1]
    h.pop()
    if len(h) > 0:
        vniz(h, 0)
    return m

def invariant(h):
    # каждый родитель не больше своих детей
    for i in range(1, len(h)):
        if h[(i - 1) // 2] > h[i]:
            return False
    return True

random.seed(8)
h = []
model = []      # то же содержимое простым списком - эталон извлечений
slomalsya = -1
oshibsya = -1
for op in range(1, 61):
    do = h[:]
    if len(h) == 0 or random.random() < 0.6:
        x = random.randint(1, 50)
        h.append(x)
        vverh(h, len(h) - 1)
        model.append(x)
        chto = "вставка " + str(x)
    else:
        chto = "извлечение"
        m = dostat(h)
        if oshibsya == -1 and m != min(model):
            oshibsya = op
        model.remove(min(model))
    if slomalsya == -1 and not invariant(h):
        slomalsya = op
        print("операция", op, "-", chto)
        print("   куча до:   ", do)
        print("   куча после:", h)
print("инвариант сломан на операции", slomalsya)
print("первый неверный ответ на операции", oshibsya)

операция 11 - извлечение
   куча до:    [9, 15, 32, 25, 15, 46, 42, 32, 26, 33]
   куча после: [15, 25, 32, 32, 15, 46, 42, 33, 26]
инвариант сломан на операции 11
первый неверный ответ на операции 14

Инвариант сломался на операции 11 - это извлечение: на место корня встал последний элемент 33, и спуск менял его всегда с левым ребёнком. Первый обмен, с 15, верен; на втором шаге у 33 были дети 25 и 15, и спуск взял левого, 25, хотя меньший - правый. В распечатке «после» 25 стоит над 15 - инвариант нарушен. Неверный ответ появился только на операции 14: испорченная куча некоторое время ещё выдаёт правильные минимумы. Сверка с моделью нашла бы ошибку, но указала бы на 14-ю операцию, где ничего не ломалось, а только проявлялось. Инвариант указал на 11-ю - на ту, где сработал ошибочный спуск.

Разбор: метаморфное отношение без эталона

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

import random

BESK = 10 ** 9

def zhadnyj_put(n, rebra, s, t):
    # «быстрый» путь: каждый раз к ближайшему непосещённому соседу.
    # Эталона на больших графах нет - проверяем только отношения.
    # Возвращает [длина, путь]; длина BESK - путь не найден
    byl = [False] * n
    v = s
    dlina = 0
    put = [s]
    byl[s] = True
    while v != t:
        luchshee = -1
        cena = BESK
        for r in rebra:
            if r[0] == v and not byl[r[1]] and r[2] < cena:
                luchshee = r[1]
                cena = r[2]
        if luchshee == -1:
            return [BESK, put]
        byl[luchshee] = True
        dlina = dlina + cena
        v = luchshee
        put.append(v)
    return [dlina, put]

random.seed(3)
narushenij_masshtab = 0
narushenij_rebro = 0
proveryaemyh = 0    # графов, где путь был: только там отношения
                    # о чём-то говорят
primer = []
for test in range(150):
    n = 6
    rebra = []
    for k in range(14):
        rebra.append([random.randint(0, 5), random.randint(0, 5),
                      random.randint(1, 9)])
    bylo = zhadnyj_put(n, rebra, 0, 5)
    d = bylo[0]
    # отношение 1: все веса вдвое - ответ вдвое
    vdvoe = []
    for r in rebra:
        vdvoe.append([r[0], r[1], 2 * r[2]])
    d2 = zhadnyj_put(n, vdvoe, 0, 5)[0]
    if d < BESK:
        proveryaemyh = proveryaemyh + 1
        if d2 != 2 * d:
            narushenij_masshtab = narushenij_masshtab + 1
    # отношение 2: новое ребро не может удлинить кратчайший путь
    novoe = [random.randint(0, 5), random.randint(0, 5),
             random.randint(1, 9)]
    stalo = zhadnyj_put(n, rebra + [novoe], 0, 5)
    d3 = stalo[0]
    if d3 > d:
        narushenij_rebro = narushenij_rebro + 1
        if len(primer) == 0:
            primer = [d, novoe, d3, bylo[1], stalo[1], sorted(rebra)]
print("вдвое тяжелее -> вдвое длиннее: нарушений", narushenij_masshtab,
      "из", proveryaemyh)
print("новое ребро не удлиняет:        нарушений", narushenij_rebro,
      "из", proveryaemyh)
stalo = primer[2]
if stalo == BESK:
    stalo = "пути нет"
print("пример: было", primer[0], "| добавили", primer[1],
      "| стало", stalo)
print("   путь до:   ", primer[3])
print("   путь после:", primer[4], "- тупик")
print("   рёбра графа [откуда, куда, вес]:")
print("  ", primer[5][:5])
print("  ", primer[5][5:10])
print("  ", primer[5][10:])

вдвое тяжелее -> вдвое длиннее: нарушений 0 из 83
новое ребро не удлиняет:        нарушений 7 из 83
пример: было 19 | добавили [2, 1, 6] | стало пути нет
   путь до:    [0, 2, 4, 5]
   путь после: [0, 2, 1, 3] - тупик
   рёбра графа [откуда, куда, вес]:
   [[0, 1, 5], [0, 2, 3], [0, 5, 6], [1, 3, 6], [2, 4, 8]]
   [[3, 0, 6], [3, 1, 2], [3, 1, 9], [3, 3, 4], [4, 0, 4]]
   [[4, 2, 3], [4, 3, 8], [4, 4, 5], [4, 5, 8]]

Отношение «вдвое тяжелее - вдвое длиннее» жадный алгоритм выполняет всегда: удвоение весов не меняет того, какой сосед ближайший, - и ошибку не видит. Отношение «новое ребро не удлиняет» нарушено семь раз, и пример красноречив: путь был длины 19, добавили ребро 2 → 1 - и жадный пошёл по нему в тупик и сообщил, что пути нет. Рёбра напечатаны, и по ним видно ещё одно: жадный ошибался и до добавления - прямое ребро 0 → 5 стоит 6, а не 19. Из 150 случайных графов путь из 0 в 5 нашёлся в 83 - на остальных отношения проверять не на чем. Это граница правила: отношение ловит только те ошибки, которые его нарушают. Масштабирование проверяет арифметику весов, а ошибку в выборе направления видно только отношению, которое меняет структуру графа.

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

Ошибку ищут там, где она проявилась. Отладка на 14-й операции кучи, хотя сломала её 11-я.

«Без эталона не проверить». Новый алгоритм уходит в работу без единого теста на больших входах - их «нечем проверить», хотя отношения проверяются всегда.

Одно слабое отношение. Масштабирование прошло 83 проверки из 83 - и алгоритм объявлен проверенным.

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

Метаморфные отношения - основной способ тестировать то, у чего нет правильного ответа: поисковую выдачу (добавил документ без слов запроса - найденные остались в выдаче), компиляторы (отключил оптимизацию - вывод программы тот же), численные расчёты (повернул систему координат - расстояния те же). Отношение выбирают по устройству системы, а не по желанию: если оценка документа зависит от всей коллекции (редкость слова среди всех документов), новый документ сдвигает оценки, и требовать прежнего порядка нельзя. Так же с машинным обучением: «переставил строки выборки - предсказания те же» верно для модели, обучение которой от порядка не зависит, а обучение, которое идёт по строкам по очереди и подстраивает модель после каждой, даст другую модель. Инварианты в самих структурах - это assert в отладочной сборке, который включают на тестах и выключают в бою.

Теперь сам

1. Придумай два метаморфных отношения для функции «наибольшая сумма подотрезка».
2. Какой инвариант проверять у двоичного дерева поиска после каждой вставки и удаления?
3. Функция сжатия szhat и распаковки raspakovat. Какое свойство ответа проверять на каждом входе?