23 сент. 2025 г.·8 мин
Идеи Тони Хоара о корректности: от логики к безопасному коду
Узнайте, как работы Тони Хоара — логика Хоара, Quicksort и мышление о безопасности — сформировали практические приёмы написания и ревью корректного ПО.
Узнайте, как работы Тони Хоара — логика Хоара, Quicksort и мышление о безопасности — сформировали практические приёмы написания и ревью корректного ПО.
Когда люди говорят, что программа «корректна», они часто имеют в виду: «я запустил её пару раз, и вывод выглядел верным». Это полезный сигнал, но это не то же самое, что корректность. Проще говоря, корректность означает, что программа соответствует своей спецификации: для каждого допустимого входа она выдаёт требуемый результат и соблюдает правила по изменению состояния, времени работы и обработке ошибок.
Подводный камень в том, что «соответствует спецификации» сложнее, чем кажется.
Во‑первых, спецификации часто неоднозначны. Бизнес-требование может сказать «отсортировать список», но это значит стабильную сортировку? Что с дубликатами, пустыми списками или несравнимыми элементами? Если спецификация не уточняет, разные люди сделают разные допущения.
Во‑вторых, крайние случаи не редки — они просто реже тестируются. Null-значения, переполнение, ошибки на границах (off-by-one), необычные последовательности действий пользователя и неожиданные внешние отказы могут превратить «кажется, работает» в «упало в проде».
В‑третьих, требования меняются. Программа может быть корректной относительно вчерашней спецификации и некорректной относительно сегодняшней.
Главный вклад Тони Хоара не в том, чтобы требовать доказательства для всего подряд. Он предложил мысль: можно точнее формулировать, что должен делать код, и рассуждать об этом дисциплинированно.
В этой статье мы проследуем три связанные нити:
Большинство команд не будут писать полные формальные доказательства. Но даже частичное, «в духе доказательства», мышление помогает находить баги, делать ревью более точными и прояснять поведение до релиза.
Тони Хоар — один из тех редких учёных по информатике, чьи идеи не остались только в статьях. Он работал и в академии, и в индустрии и задавался практическим вопросом, который до сих пор важен: как мы знаем, что программа делает то, что мы думаем — особенно когда ставки высоки?
Мы сосредоточимся на нескольких идеях Хоара, которые регулярно встречаются в кодовой базе:
{P} C {Q}.Здесь не будет глубокой математической формализации и мы не будем проводить полное машинно-проверяемое доказательство Quicksort. Цель — сделать понятия доступными: дать достаточно структуры, чтобы прояснить рассуждения, но не превращать ревью в семинар для аспирантов.
Идеи Хоара переводятся в обычные решения: какие допущения функция делает, что она гарантирует вызывающим, что должно оставаться верным в середине цикла и как заметить «почти корректные» изменения на ревью. Даже если вы не пишете {P} C {Q} явно, мышление в таком ключе улучшает API, тесты и обсуждения сложного кода.
С точки зрения Хоара, корректность строже, чем «прошло несколько примеров»: это соответствие согласованному обещанию, а не то, что выглядит правильно на небольшой выборке.
Баги часто возникают, когда команда пропускает средний шаг: перепрыгивает от требований к коду, оставляя обещание расплывчатым.
Часто смешивают два утверждения:
Для реальных систем «никогда не завершить» может быть так же вредно, как «завершить с неверным ответом».
Утверждения о корректности никогда не универсальны; они опираются на допущения о:
Явное указание допущений превращает «работает у меня» в то, что другие могут проверить.
Рассмотрим функцию sortedCopy(xs).
Полезная спецификация: «Возвращает новый список ys такой, что (1) ys отсортирован по возрастанию, (2) ys содержит ровно те же элементы, что и xs (с теми же количествами), и (3) xs не изменён».
Тогда «корректность» значит, что код выполняет эти три пункта при указанных допущениях — а не только что вывод «выглядит отсортированным» в быстром тесте.
Логика Хоара — способ говорить о коде с той же ясностью, что и о контракте: если вы стартуете из состояния, удовлетворяющего некоторым допущениям, и выполните этот фрагмент кода, вы окажетесь в состоянии, удовлетворяющем определённым гарантиям.
Основная запись — тройка Хоара:
{precondition} program {postcondition}
Предусловие говорит, что должно быть истинно до запуска фрагмента. Это не то, чего вы надеетесь — это то, что коду действительно нужно.
Пример: функция возвращает среднее двух чисел без проверок на переполнение.
a + b помещается в тип целого числаavg = (a + b) / 2avg равно математическому среднему a и bЕсли предусловие не выполняется (возможен переполнение), обещание постусловия больше не в силе. Тройка заставляет проговорить это вслух.
Постусловие говорит, что будет истинно после выполнения кода — при условии, что предусловие было выполнено. Хорошие постусловия конкретны и проверяемы. Вместо расплывчатого «результат валиден» лучше сказать, что означает «валиден»: отсортирован, неотрицателен, в рамках диапазона, изменены только конкретные поля и т.д.
Логика Хоара масштабируется от простых выражений до многошагового кода:
x = x + 1 какие факты про x теперь истинны?Смысл не в том, чтобы везде писать фигурные скобки. Смысл — сделать намерение читаемым: ясные допущения, ясные результаты и меньше разговоров «кажется, работает» на ревью.
Инвариант цикла — это утверждение, истинное до старта цикла, остающееся истинным после каждой итерации и истинное при выходе из цикла. Простая идея с большим выигрышем: она заменяет «кажется, работает» на утверждение, которое можно проверять на каждом шаге.
Без инварианта ревью часто сводится к «мы итерируем по списку и постепенно что‑то делаем». Инвариант требует точности: что именно уже верно прямо сейчас, хотя цикл ещё не завершён? Как только вы можете это ясно сформулировать, ошибки на границах и off-by-one становятся проще в обнаружении, потому что они проявляются как моменты, когда инвариант нарушается.
Большинство повседневного кода покрывается несколькими надёжными шаблонами.
Держите индексы в безопасном диапазоне.
0 <= i <= nlow <= left <= right <= highТакой инвариант хорош для предотвращения доступа за границы и для конкретизации рассуждений о массивах.
Разделите данные на область «сделано» и «ещё не сделано».
a[0..i) просмотрены.»result, удовлетворяет предикату фильтра.»Это превращает расплывчатый прогресс в чёткий контракт о том, что значит «обработано».
Часто встречается при сортировках, слияниях и разбиениях.
a[0..i) отсортирован.»a[0..i) <= pivot, а в a[j..n) >= pivot.»Даже если весь массив ещё не отсортирован, вы зафиксировали, что именно уже выполнено.
Корректность — это не только «правильно», но и «закончится». Простой способ аргументировать это — назвать меру (вариант), которая уменьшается при каждой итерации и не может уменьшаться бесконечно:
n - i уменьшается на 1 каждый раз»Если вы не можете найти уменьшающуюся меру, возможно, вы наткнулись на реальный риск: зацикливание на некоторых входах.
Quicksort даёт простое обещание: для заданного сегмента массива переставить элементы так, чтобы они оказались в неубывающем порядке, не потеряв и не придумав новых значений. Высокоуровневая форма алгоритма проста:
Это отличный учебный пример корректности: достаточно маленький, чтобы держать в голове, но богатый местами, где неформальные рассуждения дают сбой. Quicksort, который «кажется правильным» на случайных тестах, может быть неверен на специальных входах или границах.
Несколько проблем дают большинство багов:
В рассуждениях в духе Хоара обычно выделяют две части:
Это разделение делает рассуждение управляемым: добейтесь корректности partition, а затем постройте на этом корректность сортировки.
Скорость Quicksort зависит от одиной крошечной рутины: partition. Если partition хоть немного неверна, Quicksort может неправильно сортировать, зациклиться или упасть на граничных случаях.
Возьмём классическую схему Хоара (два указателя, движущихся навстречу).
Вход: фрагмент массива A[lo..hi] и выбранный pivot (часто A[lo]).
Выход: индекс p такой, что:
A[lo..p] <= pivotA[p+1..hi] >= pivotОбратите внимание, что не гарантируется: что pivot окажется именно на позиции p, и что равные pivot элементы сгруппированы в одной стороне. Это нормально — Quicksortу достаточно корректного разделения.
Когда алгоритм продвигает два индекса — i слева и j справа — полезно думать о том, что уже «зафиксировано». Практичный набор инвариантов:
A[lo..i-1] <= pivot (левая часть "чиста")A[j+1..hi] >= pivot (правая часть "чиста")A[i..j] — не классифицировано (ещё не проверено)Когда находят A[i] > pivot и A[j] < pivot, их обмен сохраняет инварианты и сужает неклассифицированную середину.
i дойдёт вправо; partition всё равно должен завершиться и вернуть осмысленное p.j сойдёт влево; та же проблема завершения.< vs <=), указатели могут застрять. Схема Хоара полагается на согласованное правило, чтобы был прогресс.Существуют разные схемы partition (Lomuto, Hoare, трёхпутёвое). Ключ в том, чтобы выбрать одну, явно задать её контракт и ревьюить код в соответствии с этим контрактом.
Рекурсию легче доверять, когда вы можете ясно ответить на два вопроса: когда она останавливается? и почему каждый шаг корректен? Мышление в духе Хоара помогает, потому что заставляет вас проговорить, что должно быть истинно до вызова и что будет истинно после возвращения.
Рекурсивная функция нуждается как минимум в одном базовом случае, где она не делает рекурсивных вызовов и при этом удовлетворяет обещанному результату.
Для сортировки типичный базовый случай — «массивы длины 0 или 1 уже отсортированы». Здесь «отсортирован» нужно явным образом: для отношения ≤ массив считается отсортированным, если для любых индексов i < j выполняется a[i] ≤ a[j]. (Сохранение исходного порядка равных элементов — отдельное свойство, называемое стабильностью; Quicksort обычно нестабилен, если специально не проектировать его иначе.)
Каждый рекурсивный шаг должен вызывать себя на строго меньшем вводе. Это «сжатие» — ваш аргумент завершения: если размер уменьшается и не может стать меньше нуля, бесконечной рекурсии не будет.
Уменьшение важно и для безопасности стека. Даже корректный код может упасть, если глубина рекурсии станет слишком большой. В Quicksort неудачно сбалансированные разбиения могут дать большую глубину рекурсии. Это — аргумент о завершении плюс практическое напоминание о худшем случае.
Худший случай Quicksort может стать O(n²) при очень несбалансированных разбиениях, но это уже проблема производительности, а не корректности. Цель рассуждений: при условии, что partition сохраняет элементы и правильно делит их относительно pivot, рекурсивная сортировка поддиапазонов приводит к тому, что весь диапазон соответствует определению отсортированности.
Тестирование и доказательное мышление стремятся к одной цели — уверенности — но идут к ней разными путями.
Тесты отлично ловят конкретные ошибки: off-by-one, забытые крайние случаи, регрессии. Но набор тестов лишь выбирает точки входного пространства. Даже «100% покрытие» не значит «все поведения проверены»; это чаще значит «выполнены все строки».
Доказательное рассуждение (в духе Хоара) начинает с спецификации и задаёт вопрос: если эти предусловия держатся, всегда ли код достигает постусловий? Хорошо выполненное рассуждение не просто находит баг — часто оно устраняет целую категорию ошибок (например, «доступ за границы невозможен» или «инвариант partition сохраняется»).
Чёткая спецификация сама по себе генерирует идеи для тестов.
Если ваше постусловие — «выход отсортирован и является перестановкой входа», вы автоматически получаете кейсы для тестирования:
Спецификация говорит, что значит «корректно», а тесты проверяют, что это совпадает с реальностью.
Property-based тестирование — это середина между доказательствами и примерами. Вместо ручного выбора случаев вы формулируете свойства, а инструмент генерирует множество входов.
Для сортировки два простых свойства дают большую уверенность:
Эти свойства — по сути постусловия, записанные в исполняемой форме.
Лёгкая рутина, масштабируемая в командной работе:
Если хотите институционализировать это, добавьте «спецификация + заметки по рассуждению + тесты» в шаблон PR или чеклист ревью (см. /blog/code-review-checklist).
Если вы используете workflow типа vibe-coding (генерация кода через чат-интерфейс), дисциплина та же — даже важнее. В Koder.ai, например, можно начать в Planning Mode, зафиксировать предусловия/постусловия до генерации кода, а затем итерировать с snapshot/rollback, добавляя property-based тесты. Инструмент ускоряет реализацию, но спецификация остаётся тем, что не даёт «быстро» превратиться в «хрупко».
Корректность — это не только «программа возвращает правильное значение». Мышление о безопасности задаёт другой вопрос: какие исходы недопустимы, и как мы их предотвращаем — даже когда код перегружен, неправильно используется или частично выходит из строя? На практике безопасность — это корректность с приоритетами: некоторые ошибки просто неприятны, другие приводят к финансовым потерям, утечкам приватных данных или физическому вреду.
Баг — дефект в коде или дизайне. Опасность (hazard) — ситуация, которая может привести к недопустимому исходу. Один баг может быть безвреден в одном контексте и опасен в другом.
Пример: off-by-one в галерее фото может неправильно помечать картинку; тот же баг в калькуляторе дозирования лекарств может навредить пациенту. Мышление о безопасности заставляет связывать поведение кода с последствиями, а не только с «выполнением спецификации».
Не нужны тяжёлые формальные методы, чтобы получить немедленный выигрыш в безопасности. Команды могут принять небольшие, повторяемые практики:
Эти приёмы хорошо сочетаются с логикой Хоара: явные предусловия (какие входы допустимы) и постусловия, включающие свойства безопасности (чего никогда не должно происходить).
Проверки ради безопасности стоят чего-то — процессорного времени, сложности или ложных отклонений.
Мышление о безопасности не про доказательство элегантности, а про предотвращение тех отказов, которых вы не можете себе позволить.
Ревью кода — место, где мышление о корректности уже быстро окупается, потому что вы можете заметить пропущенные допущения задолго до продакшена. Основной приём Хоара — проговорить «что должно быть истинно до» и «что будет истинно после» — легко превращается в вопросы ревью.
Когда вы читаете изменение, попробуйте сформулировать каждую ключевую функцию как маленькое обещание:
Простая привычка ревьюера: если вы не можете сказать предусловия/постусловия в одном предложении, вероятно, код нуждается в более явной структуре.
Для рискованных или центральных функций добавьте небольшой комментарий с контрактом прямо над сигнатурой. Делайте его конкретным: входы, выходы, побочные эффекты и возможные ошибки.
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer > 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
Такие комментарии не формальные доказательства, но дают ревьюеру что именно сверить с реализацией.
Будьте особенно внимательны при ревью кода, который касается:
Если изменение касается чего‑то из этого, спросите: «Какие предусловия и где они проверяются?» и «Какие гарантии сохраняются даже при ошибке?»
Формальное рассуждение не обязано превращать весь код в математическую статью. Цель — потратить дополнительные усилия там, где они окупаются: в местах, где «в тестах выглядит хорошо» недостаточно.
Они хорошо подходят для маленьких критичных модулей, от которых зависит всё остальное (аутентификация, правила оплаты, права доступа, блокировщики безопасности), или для сложных алгоритмов, где ошибки на границах живут месяцами (парсеры, планировщики, эвикшн-кешей, примитивы конкурентности, разбиения и трансформации с множеством границ).
Правило: если баг может привести к реальному вреду, значительным финансовым потерям или скрытой порче данных — нужен уровень гарантий выше, чем обычный набор ревью+тесты.
От «лёгких» до «тяжёлых», и часто лучший результат — их комбинация:
Решение о глубине формализма основано на оценке:
На практике «формальность» может наращиваться постепенно: начните с явных контрактов и инвариантов, затем добавляйте автоматизацию, которая будет следить за ними. Для команд, быстро строящих на Koder.ai (генерация интерфейса на React, бэкенда на Go и схемы Postgres в tight loop), snapshot/rollback и экспорт кода облегчают быструю итерацию при сохранении контрактов через тесты и статический анализ в CI.
Используйте это как быстрый «нужно ли формализовать дальше?» шлюз на этапе планирования или ревью:
Дальнейшее чтение: design-by-contract, property-based testing, model checking для автоматов состояний, статические анализаторы для вашего языка и вводные материалы по proof assistants и формальной спецификации.
Корректность означает, что программа выполняет согласованную спецификацию: для каждого допустимого входа и релевантного состояния системы она выдаёт требуемые выходы и побочные эффекты (и обрабатывает ошибки так, как обещано). «Кажется, работает» обычно значит, что вы проверили лишь несколько примеров, а не всё пространство входных данных или сложные граничные случаи.
Требования — это бизнес-цель в простых словах («отсортировать список для отображения»). Спецификация — это точное, проверяемое обещание («возвращает новый список, отсортированный по возрастанию, с тем же мультимножеством элементов, исходный список не менялся»). Реализация — это код. Ошибки часто возникают, когда команда прыгает прямо от требований к коду, не записав проверяемое обещание.
Частичная корректность: если код возвращает результат, то он корректен. Полная корректность: код гарантированно завершится и вернёт корректный результат — то есть завершение само по себе часть утверждения.
На практике полная корректность важна там, где «зависнуть навсегда» — это видимая пользователем ошибка, утечка ресурсов или риск для безопасности.
Тройка Хоара {P} C {Q} читается как контракт:
P (предусловие): что должно быть истинно перед выполнением CC: фрагмент кодаПредусловия — это то, что коду нужно (например, «индексы в диапазоне», «элементы сравнимы», «замок удерживается»). Если предусловие может быть нарушено вызывающим кодом, то следует либо:
Иначе ваши постусловия станут желаемыми утверждениями, а не гарантиями.
Инвариант цикла — утверждение, которое истинно до начала цикла, остаётся истинным после каждой итерации и истинно после завершения цикла. Полезные шаблоны:
0 <= i <= n)Если вы не можете сформулировать инвариант, это признак того, что цикл делает слишком много или границы неочевидны.
Обычно вы называете меру (вариант), которая уменьшается при каждой итерации и не может уменьшаться бесконечно, например:
n - i уменьшается на 1Если невозможно найти убывающую меру, возможно, вы обнаружили реальный риск бесконечного цикла (особенно при дубликатах или «застоявшихся» указателях).
В Quicksort функция partition — маленькая рутина, от которой зависят остальные части. Если partition немного неверна, вы можете получить:
Поэтому полезно явно сформулировать контракт partition: что истинно в левой части, что — в правой, и что элементы лишь переставляются (перестановка).
Дубликаты и обработка «равно опорному» — частая причина ошибок. Практические правила:
Если дубликатов много, рассмотрите трёхпутёвое разбиение — оно уменьшает и глубину рекурсии, и вероятность ошибок.
Тесты находят конкретные ошибки; рассуждение по образцу доказательства исключает целые классы ошибок (безопасность границ, сохранение инвариантов, завершение). Практический гибридный подход:
Для сортировки два высокоценных свойства: отсортированность (non-decreasing) и перестановочность (те же элементы с теми же счётами).
Q (постусловие): что будет истинно после завершения C, при условии, что P было истинноНет необходимости писать эту нотацию в коде — использовать структуру «что требуется на входе — что гарантируется на выходе» в ревью уже даёт практическую пользу.