Верификация: ящик инструментов от свойств до доказательств

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

Обычный тест проверяет точку: вот вход, вот ожидаемый выход. Три теста, это три точки. А между точками лежит поле входов, в которое ты не заглядывал, и баг обычно сидит именно там: на пустом массиве, на отрицательном нуле, на строке из одних суррогатных пар. Этот урок про инструменты, которые проверяют не точки, а пространства: property-based тестирование, фаззинг, статический анализ, логика Хоара и model checking. Это обзорная карта: к каждому инструменту мы дадим достаточно, чтобы ты понял, что он умеет и когда за ним идти, а глубокие погружения ждут в разделе про тестирование.

Лестница строгости

Все инструменты верификации можно расставить по одной оси: насколько сильную гарантию они дают и сколько за неё просят.

Ступень	Что проверяет	Цена	Гарантия
Типы и линтер	Форму данных и опасные конструкции	Почти бесплатно	Слабая, зато всюду
Тесты на примерах	Конкретные точки	Дёшево	Только проверенные точки
Property-based	Свойство на тысячах сгенерированных входов	Умеренно	Сильная уверенность, не доказательство
Фаззинг	Программа не падает на миллионах входов	Умеренно, нужно время на прогон	Отсутствие падений на найденных путях
Контракты в рантайме	Пред- и постусловия на каждом вызове в проде	Дёшево написать, платишь в рантайме	Нарушение видно сразу, но уже в проде
Model checking	Все состояния модели, исчерпывающе	Дорого: нужна отдельная модель	Доказательство, но для модели, не для кода
Refinement types и доказательства	Свойства самого кода, математически	Очень дорого	Полная, в пределах спецификации

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

Property-based: свойства вместо примеров

Возьмём функцию сортировки массива по возрастанию. Какие у неё есть свойства, истинные для любого входа?

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

Заметь: ни одно из свойств не упоминает конкретных чисел. Это утверждения обо всех входах сразу. Хочется проверить их для любых данных, но перебирать все массивы всех длин утомительно даже для компьютера.

Property-based тестирование предлагает компромисс. Ты описываешь контракт генерации входных данных, а инструмент проверяет свойство на срезе этих данных: не один раз, а тысячи. Это не бесконечность, но несравнимо лучше трёх точек, написанных руками. Сверху инструмент добавляет две хитрости:

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

В JS/TS экосистеме стандарт это fast-check. Живую практику с ним, включая интерактивный виджет про shrinking, ты найдёшь в уроке про property и snapshot. Здесь мы посмотрим на другой угол: откуда брать генераторы, чтобы не описывать данные дважды.

Схема как генератор: Effect Schema и Arbitrary

Задача из адвента fast-check: рассортировать письма детей, сначала по возрасту, при равном возрасте по имени. Имя: непустая строка из строчных латинских букв. Возраст: целое от 7 до 77.

Контракт данных у нас в курсе уже есть чем описать: Schema из Effect. Казалось бы, схема нужна для сериализации и валидации. Но схема, это просто декларативное описание контракта, и из него можно вывести не только декодер, но и генератор: Arbitrary.schema превращает схему в Arbitrary, источник произвольных значений со встроенным shrinking. Движок property-тестов в Effect 4 свой, ставить fast-check для этого не нужно.

import { Arbitrary, Schema } from 'effect';

// возраст из условия задачи: целое от 7 до 77
const Age = Schema.Int.check(Schema.isBetween({ minimum: 7, maximum: 77 }));

// имя: непустая строка из строчных латинских букв;
// генератор читает шаблон и выдаёт только такие строки
const Name = Schema.String.check(Schema.isPattern(/^[a-z]+$/));

const Letter = Schema.Struct({ name: Name, age: Age }).annotate({
  // аннотация форматирования: как сущность печатается при отладке
  toFormatter: () => ({ name, age }) => `${name}=${age}`,
});

const Letters = Schema.Array(Letter);

const lettersArb = Arbitrary.schema(Letters); // Arbitrary<Letter[]>
const letterPretty = Schema.toFormatter(Letter); // (letter) => string

Обрати внимание: отдельного генератора для имени писать не пришлось. Проверки вроде isPattern, isBetween и isMinLength генератор понимает сам и строит значения, которые им удовлетворяют, а не отбрасывает лишние. Контракт описан один раз, и валидатор с генератором из него выведены одинаково. toFormatter задаёт, как значение превращается в строку для отладки и логов: в своих сообщениях об ошибке ты напечатаешь читаемое anya=12, а не простыню JSON.

Дальше обычный vitest, а проверку запускает Arbitrary.checkEffect:

import { Arbitrary, Effect } from 'effect';
import { describe, expect, it } from 'vitest';

const sortedProperly = (unsorted: ReadonlyArray<typeof Letter.Type>) => {
  const letters = sortLetters(unsorted);
  for (let i = 1; i < letters.length; i++) {
    const prev = letters[i - 1]!;
    const curr = letters[i]!;
    if (prev.age > curr.age) return false;
    if (prev.age === curr.age && prev.name > curr.name) return false;
  }
  return true;
};

describe('сортировка писем', () => {
  it('упорядочивает по возрасту, при равенстве по имени', async () => {
    const result = await Effect.runPromise(
      Arbitrary.checkEffect(lettersArb, sortedProperly, { runs: 1000 }), // количество прогонов
    );
    expect(Arbitrary.formatCheckFailure(result)).toBeUndefined();
  });
});

Свойство это обычная функция: вернула false, и проверка считается упавшей. checkEffect запускает её на сгенерированных входах и принимает настройки: количество прогонов, seed генератора случайных чисел, лимит отброшенных значений. Ответ это значение, а не исключение. formatCheckFailure превращает провал в отчёт с минимальным контрпримером после shrinking и токеном Replay, по которому падение воспроизводится детерминированно, а для успешной проверки возвращает undefined. Сломай сортировку, убрав сравнение имён, и отчёт покажет два письма одного возраста, например aa и a: shrinking сжимает случайный массив до самого короткого контрпримера. Потыкаться в живой код можно в песочнице Effect.

Главная выгода подхода: контракт описан один раз. Та же схема Letter валидирует данные на границе системы, генерирует тестовые входы и печатает значения при отладке. Когда контракт меняется, генератор и валидатор меняются синхронно, им неоткуда разъехаться.

С чего начать, когда инварианты не видны

Частая претензия к property-based подходу: непонятно, какие свойства формулировать. Команда Hypothesis, главного PBT-инструмента в Python, советует входить инкрементально.

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

Шаг один: round-trip. Найди в кодовой базе пары превращений туда и обратно: сериализация и разбор, кодирование и декодирование, две формы представления одних и тех же данных в разных частях программы. Свойство: композиция туда-обратно, это тождественная функция. Round-trip ловит несимметричности, о которых никто не думал: потерю таймзоны, обрезание точности, экранирование.

Шаг два: доменные инварианты. Сумма операций равна балансу, скидка не делает цену отрицательной, у отсортированного массива длина не меняется. Это уже свойства из контрактов, которые ты выписывал в прошлом уроке.

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