Тони Хоар и корректность ПО: логика Хоара и Quicksort

Почему Хоар важен для разговоров о корректности

Имя Тони Хоара часто появляется рядом со словом «корректность» не потому, что он «просто придумал ещё одну теорию», а потому что предложил удобный язык, на котором можно обсуждать правильность программ без гадания и расплывчатых формулировок. Его подход помогает превратить вопрос «похоже, работает» в вопрос «какое именно обещание даёт этот код — и выполняет ли он его при заданных условиях».

Что здесь называется «корректностью»

В этой статье корректность — это не мифическое состояние «без багов вообще». Это гораздо практичнее: программа корректна, если она соответствует спецификации (явной или подразумеваемой). То есть:

• при определённых входных данных (и состоянии системы) она делает ровно то, что от неё ожидают;
• и делает это в рамках оговорённых ограничений (например, по обработке ошибок, форматам данных, правам доступа).

Такое определение сразу снимает часть споров: мы сравниваем не «ощущение качества», а поведение кода с договорённостью.

Где это реально важно

Корректность имеет значение не только в «критичных системах». Ошибка в бизнес‑логике может стоить денег и доверия (неверные начисления, скидки, статусы заказов). Ошибка в инфраструктуре или безопасности — привести к потере данных, простоям и инцидентам. Чем дороже последствия, тем полезнее уметь формулировать и проверять обещания кода.

Как устроен разбор дальше

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

Что такое корректность программ простыми словами

Корректность программы — это не про то, «запускается ли она» и даже не про то, «проходит ли тесты». В самом простом виде корректность означает: программа делает ровно то, что было обещано, для всех ситуаций, которые входят в её условия использования.

«Работает на моих данных» vs «работает по определению»

Фраза «у меня работает» обычно означает: вы попробовали несколько примеров — и увидели ожидаемый результат. Это полезно, но не гарантирует ничего за пределами этих примеров.

«Работает по определению» — это когда поведение программы следует из чёткой формулировки того, что она должна делать, и из аргумента (или доказательства), что код этому следует. Тогда вас меньше удивляют редкие случаи: пустой ввод, повторяющиеся элементы, очень большие числа, неожиданные форматы.

Корректность всегда относительно спецификации

Нельзя доказать корректность «вообще». Корректность всегда звучит как утверждение вида:

• если вход удовлетворяет некоторым условиям,
• то результат будет обладать заданными свойствами.

Эти условия и свойства и есть спецификация (пусть даже короткая, на уровне комментария или постановки задачи). Без спецификации нечего доказывать: у кода нет «обещаний», а значит любое поведение можно объявить приемлемым задним числом.

Пример спецификации для функции сортировки: «на выходе элементы идут по неубыванию и это ровно те же элементы, что были на входе». Это уже два конкретных обещания.

Частичная и полная корректность

Частичная корректность отвечает на вопрос: если программа завершилась, верен ли результат?

Полная корректность добавляет ещё один слой: она не только выдаёт правильный результат, но и обязательно завершается (для всех входов, которые допускает спецификация).

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

Корректность, надёжность и безопасность — не одно и то же

• Корректность — соответствие спецификации.
• Надёжность — способность стабильно работать в реальных условиях (сбои сети, нехватка памяти, ошибки интеграций).
• Безопасность — устойчивость к злоупотреблениям и атакам.

Корректность помогает всем трём, но не заменяет их: можно корректно реализовать неверную спецификацию или корректно обработать вход «как задумано», но при этом оставить уязвимость в другом месте.

Логика Хоара: идея «договоров» для кода

Логика Хоара часто звучит как «формальные методы для математиков», но в основе у неё очень бытовая идея: у любого фрагмента кода есть условия, при которых он обязан работать, и обещания, которые он должен выполнить. Это и есть «договор» между кодом и его окружением — другими функциями, пользователем, базой данных, системой.

Формула {P} C {Q}: как читать без «математики для посвящённых»

Запись Хоара выглядит так: {P} C {Q}.

• C — команда/фрагмент программы: функция, цикл, несколько строк.
• P — что должно быть истинно до выполнения C.
• Q — что будет истинно после выполнения C, если C завершилась.

Её можно читать по‑человечески так: «Если перед запуском кода выполняется условие P, то после выполнения кода будет гарантирован результат Q».

Предусловие (P): какие входы и состояние допустимы

Предусловие — это не «каприз автора», а способ честно сказать: «Вот при каких входных данных и состоянии системы мой код берёт на себя ответственность».

Простой пример: функция, которая берёт элемент массива по индексу.

• P: индекс находится в диапазоне массива.
• Без P код может аварийно завершиться или вернуть мусорный результат.

Важно: предусловие относится не только к аргументам функции. Оно может включать состояние — например, «соединение с базой открыто» или «пользователь аутентифицирован».

Постусловие (Q): что гарантируется после выполнения

Постусловие — это обещание кода. Оно описывает результат и изменения состояния.

Например, для функции сортировки:

• Q: «массив отсортирован по неубыванию»
• и дополнение, которое часто критично: «и содержит те же элементы, что и до сортировки» (чтобы исключить незаметные потери/дублирования).

Хорошее постусловие отвечает на вопрос: «Как мне проверить, что код сделал ровно то, что нужно — не больше и не меньше?»

Почему это похоже на «договор» между кодом и окружением

Договор полезен тем, что разделяет ответственность:

• Окружение (вызывающая сторона) обязуется соблюсти P.
• Код обязуется обеспечить Q.

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

Предусловия и постусловия на бытовых примерах

Предусловие — это «что должно быть верно до вызова функции», постусловие — «что гарантированно станет верно после». Вместе они работают как договор: вызывающая сторона обещает входные условия, а функция — результат.

Пример контракта: сортировка

Функция sort(items).

Предусловие (простыми словами): «Мне передают список элементов, которые можно сравнивать между собой».

Постусловие: «Я верну список той же длины, состоящий из тех же элементов, но в неубывающем порядке».

Заметьте: «в том же порядке, что и раньше» — это уже про стабильность сортировки. Это не всегда нужно, но если важно, это должно быть явной частью постусловия.

Пример контракта: поиск

Функция find(userId, users).

Предусловие: «users — коллекция пользователей, у каждого есть уникальный идентификатор».

Постусловие: «Если пользователь с таким userId существует, верну его; иначе верну признак отсутствия (например, null/None)».

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

Пример контракта: преобразование данных

Функция normalizePhone(input).

Проверяемые условия: «вход — строка», «на выходе только цифры и ведущий +», «пустой ввод даёт пустой результат/ошибку (выбрать одно)».

Уточняемые условия: «какие страны поддерживаем», «как трактуем добавочные номера», «нормализуем ли “8” в “+7”». Их тоже можно записать, но иногда сначала как бизнес‑правила, а уже потом формализовать.

Как записывать и зачем это нужно команде

Начинайте человеческим языком: 2–3 предложения про вход, выход и ошибки. Затем постепенно делайте условия точнее: перечисляйте варианты, добавляйте примеры, фиксируйте формат результата.

Контракты особенно полезны в спорах о коде: вместо «мне кажется так красивее» обсуждают конкретное утверждение — выполняется ли предусловие и обеспечивается ли постусловие. Это снижает вкусовщину и помогает быстро найти, кто и где нарушил договор.

Инварианты: опора для доказательства и понимания

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

Что такое инвариант простыми словами

Если предусловие отвечает на вопрос «с чего мы начинаем?», а постусловие — «что должно быть в конце?», то инвариант фиксирует «что должно оставаться истинным по дороге». Он соединяет три состояния: до шага, во время повторений и после завершения.

Почему инварианты особенно важны в циклах и рекурсии

В линейном коде легче держать в голове причинно‑следственные связи. Циклы и рекурсия создают повторяющиеся переходы состояния, где ошибка часто не видна на первых итерациях.

Инвариант позволяет рассуждать о корректности по схеме:

1. Инициализация: инвариант верен перед первой итерацией/входом в рекурсию.
2. Сохранение: один шаг цикла (или один рекурсивный вызов) не нарушает инвариант.
3. Завершение: когда условие выхода срабатывает, инвариант вместе с условием выхода даёт нужное постусловие.

Признаки хорошего инварианта

Хороший инвариант не должен быть «умным ради умности»:

• Простота: формулируется одной‑двумя ясными фразами.
• Проверяемость: можно представить, как его проверить на конкретном состоянии (хотя бы мысленно или через assert).
• Полезность: из него действительно выводится постусловие, а не просто «всё хорошо».

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

Quicksort как история про корректность, а не только про скорость

Quicksort часто вспоминают как «быструю сортировку», но его настоящая ценность в обучении — он отлично показывает разницу между идеей алгоритма и корректной реализацией. Описание на уровне «выбрать опорный элемент, разбить массив, рекурсивно отсортировать части» выглядит коротким и ясным. А вот в реализации легко допустить мелкую ошибку, которая проявится только на отдельных входах — поэтому Quicksort и стал классическим учебным примером.

Почему на Quicksort так удобно учиться корректности

У алгоритма есть сильная интуиция и при этом много острых углов:

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

Partition — место, где рождается большинство ошибок

Самый рискованный участок — разбиение (partition). Здесь обычно путают границы диапазона, неверно двигают два указателя навстречу друг другу, неправильно обрабатывают элементы, равные опорному, или делают swap не в тот момент.

Корректность partition удобно держать на «договоре» в виде инварианта: в процессе разбиения всегда сохраняется утверждение, что все элементы слева удовлетворяют условию относительно опорного, а все элементы справа — противоположному (например, слева ≤ pivot, справа ≥ pivot). Если инвариант где‑то нарушился — дальнейшая рекурсия уже не спасёт.

Корректность рекурсии: уменьшаем задачу и не забываем базовый случай

Даже идеальный partition бесполезен, если рекурсия не гарантирует прогресс. Для корректности важны два пункта:

1. уменьшение задачи: каждый рекурсивный вызов должен работать с диапазоном строго меньшего размера;

2. базовый случай: диапазон длины 0 или 1 уже отсортирован.

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

Где Quicksort ломается: типовые ошибки и их причины

Quicksort часто воспринимают как «просто сортировку», но на практике он ломается не из‑за идеи, а из‑за деталей реализации. Эти детали коварны: алгоритм может «почти всегда» работать, а затем выдавать редкие и трудноуловимые сбои.

Типичные дефекты: границы, рекурсия, разбиение

Самые частые ошибки — в границах и условиях остановки.

• Неверные границы подмассива: перепутали включительность/исключительность индексов (например, сортируем [l, r] в одном месте и [l, r) в другом). Итог — пропущенный элемент, выход за пределы массива или «странные» перестановки.
• Бесконечная рекурсия: после разбиения один из подмассивов не уменьшается. Это происходит, если partition возвращает те же границы, что и вход.
• Неправильное разбиение (partition): элементы, равные опорному, обрабатываются неверно. Например, все «равные» уходят в одну сторону, и на массивах с большим количеством одинаковых значений рекурсия перестаёт сокращаться.

Почему опасны «почти правильные» сортировки

Quicksort может давать верный результат на «обычных» данных и проваливаться на редких:

• много одинаковых элементов;
• уже отсортированный или почти отсортированный массив;
• массивы длины 0, 1, 2 (краевые случаи);
• повторяющиеся паттерны, где разбиение систематически не делит массив.

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

Постусловие сортировки: что именно должно быть истинно

Чтобы говорить о корректности, полезно формулировать постусловие явно. Для сортировки оно состоит из двух частей:

1. Порядок: результат упорядочен (например, для всех i < j выполняется a[i] ≤ a[j]).

2. Сохранение элементов: результат — это перестановка исходного массива (ничего не потеряли и не «создали»). На практике именно эта часть чаще всего ломается из‑за неверных обменов или выхода за границы.

Как контракты и инварианты подсвечивают место поломки

Контракты (пред- и постусловия) и инварианты помогают не «гадать», а локализовать проблему.

Например, для шага разбиения удобно держать инвариант вида: «все элементы слева от указателя ≤ pivot, все справа ≥ pivot». Если при очередном обмене инвариант перестал быть истинным — вы нашли точку, где разбиение реализовано неверно. А если после разбиения не выполняется предикат «подмассивы строго меньше исходного», это сразу объясняет риск бесконечной рекурсии.

Тесты vs доказательства: что дают оба подхода

Тестирование и доказательства корректности отвечают на разные вопросы. Тесты помогают найти ошибки, а доказательства объясняют, почему ошибок быть не может (при заданных предположениях). На практике эти подходы не конкурируют, а усиливают друг друга.

«Есть ли контрпример?» против «почему всегда верно?»

Тестирование по сути спрашивает: «Могу ли я подобрать входные данные, на которых программа ведёт себя неправильно?» Если контрпример найден — отлично, баг воспроизводим.

Доказательство корректности спрашивает другое: «Почему для любого допустимого входа результат будет правильным?» Оно строится на предусловиях, постусловиях и, для циклов, на инвариантах.

Важно помнить: доказательство всегда опирается на модель. Если предусловия выбраны слишком слабо или забыты ограничения (например, про диапазон индексов), «доказанная» программа всё равно может падать.

Когда достаточно тестов, а когда нужен более строгий подход

Тестов часто хватает, если:

• цена ошибки невысока (условная «не та кнопка в отчёте»);
• область входов ограничена и хорошо обозрима;
• есть быстрый обратный отклик (ошибку легко поймать и исправить).

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

Комбинация, которая работает

Практичная связка выглядит так:

1. Контракты: явно формулируем предусловия/постусловия.
2. Тесты по границам: генерируем кейсы вокруг нулей, максимумов, пустых коллекций, повторов.
3. Инварианты: проверяем, что ключевые утверждения сохраняются на каждом шаге.

Простой критерий выбора

Спросите себя: «Сколько стоит ошибка?» и «Насколько вероятно, что мы пропустим редкий крайний случай?» Чем выше оба ответа, тем больше смысла инвестировать в доказательность: контракты, анализ инвариантов и более формальную верификацию.

Безопасное мышление: как «корректность» снижает риск

Корректность — это не только про «доказать, что сортировка сортирует». Это про привычку проектировать так, чтобы целые классы ошибок не появлялись вообще. Такой подход особенно ценен там, где цена сбоя высока: деньги, персональные данные, здоровье, производство.

Хоар и систематическое предотвращение ошибок

Идея Хоара полезна как дисциплина мышления: мы заранее фиксируем, какие состояния программы допустимы, а какие — нет. Когда это сделано, многие баги перестают быть «неожиданными» и превращаются в нарушения договора, которые легче обнаружить на ревью, статическим анализом или проверками в коде.

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

Принцип «сначала спецификация»

Безопасность начинается с вопроса: что должно быть истинным до вызова (предусловие) и после (постусловие)? Спецификация также должна описывать запреты:

• какие аргументы считаются ошибочными;
• какие побочные эффекты недопустимы;
• какие ресурсы нельзя трогать.

Так вы сокращаете пространство неопределённости — а именно в нём чаще всего и прячутся уязвимости и аварии.

Отказоустойчивость и предсказуемые ошибки

Безопасное проектирование не требует «никогда не падать». Оно требует падать предсказуемо: с понятной ошибкой, без повреждения данных и без частично выполненных действий. Это ведёт к решениям вроде явных кодов ошибок/исключений, атомарных операций, проверок границ и валидации входов на ранней стадии.

Как меняется дизайн: меньше допущений, больше гарантий

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

Как применять идеи Хоара в обычной разработке

Логика Хоара часто ассоциируется с формальными доказательствами, но её главный подарок практикам — привычка формулировать «что должно быть верно» до и после работы кода. Это легко встроить в повседневную разработку без математики на доске.

Комментарии и ADR как «мягкая» спецификация

Начните с кратких утверждений рядом с кодом: что функция ожидает (предусловия) и что гарантирует (постусловия). Важно писать не «как сделано», а «что должно быть верно».

Для более крупных решений используйте ADR (Architecture Decision Record): одна страница о контексте, решении и последствиях. Такой текст легче поддерживать, чем объёмную документацию, и он реже «отстаёт» от кода, если обновлять его в тех же PR.

assert и проверки предусловий: где уместны

Проверки предусловий — это способ сделать договор явным. Хорошие места: границы модулей, публичные API, обработка внешнего ввода.

• Внутри горячих циклов и низкоуровневых участков — аккуратно: лучше один раз проверить «на входе», чем тормозить на каждой итерации.
• В продакшене — отличайте «ошибка разработчика» (assert) от «ошибка пользователя» (понятная валидация и сообщение).

Типы, линтеры и статический анализ как автоматизация гарантий

Типы, линтеры и статический анализ частично выполняют роль «машинной проверки» договоров: не дают передать null там, где его быть не должно, ловят недостижимые ветки, подозрительные сравнения, забытые обработки ошибок. Это не заменяет корректность целиком, но срезает целый класс багов ещё до тестов.

Документация API: что обещаем и что требуем

Описывайте API в терминах договоров:

• что считается корректным входом;
• какие гарантии даёт функция (включая ошибки/исключения);
• что происходит с состоянием (изменяемость, побочные эффекты);
• границы ответственности: «мы нормализуем данные» или «вы передаёте уже нормализованные».

Так идеи Хоара превращаются в понятные правила игры для команды и пользователей вашего кода.

Где здесь помогает TakProsto.AI

Даже если вы собираете продукт через чат‑подход (vibe‑coding), «договоры» остаются ключом к предсказуемому результату. В TakProsto.AI удобно начинать именно со спецификации: вы формулируете предусловия/постусловия и сценарии, а затем просите платформу построить реализацию веб/серверной/мобильной части так, чтобы эти условия выполнялись.

Практически это выглядит так:

• фиксируете контракт в «planning mode» перед тем, как генерировать изменения;
• проверяете крайние случаи и инварианты как часть критериев готовности;
• при спорных правках используете снимки (snapshots) и откат (rollback), чтобы безопасно сравнить варианты;
• при необходимости выгружаете исходники и продолжаете ревью/аудит в привычном пайплайне.

Плюс для команд на российском рынке — данные и окружение остаются в РФ, а стек (React на фронтенде, Go + PostgreSQL на бэкенде, Flutter для мобильных приложений) позволяет формулировать и проверять контракты на всех слоях.

Частые ошибки при внедрении «корректности» в команде

Пытаться «внедрить корректность» можно по‑разному: через предусловия/постусловия, инварианты, контракты в коде, чек‑листы к ревью. Но первые попытки часто дают обратный эффект — люди устают от формальностей, а реальных дефектов меньше не становится. Ниже — типовые промахи и как их распознать.

Слишком сильные предусловия

Иногда разработчики делают предусловие настолько жёстким, что функция становится удобной только «в идеальном мире». Например: «входной массив всегда отсортирован», «значение всегда непустое», «индекс всегда в диапазоне». Так проще рассуждать о корректности, но API теряет практическую ценность: реальный код вынужден раздуваться проверками и костылями.

Правило простое: если предусловие постоянно нарушается в местах вызова, значит оно не отражает реальность — либо перенесите проверку внутрь, либо измените контракт и поведение (например, возвращайте ошибку).

Слишком слабые постусловия

Постусловие вроде «возвращает результат» или «что‑то делает с коллекцией» выглядит как формальность: его невозможно проверить, и оно не помогает в ревью.

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

Инварианты «ради галочки»

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

Полезный инвариант обычно:

• короткий и локальный (про текущие переменные/структуры);
• проверяемый тестом или assert хотя бы в debug;
• объясняет, почему шаг алгоритма безопасен.

Риск формализма

Самая частая ловушка — «делаем корректность, потому что так надо». Держите фокус на целях: ясность, меньше дефектов, предсказуемое поведение. Если контракт не помогает принимать решения (в дизайне API, ревью, тестах), значит его стоит переписать проще или убрать.

Практический план внедрения и что делать дальше

Пытаться «доказать всё» сразу — почти гарантированный путь к разочарованию. Лучше относиться к идеям Хоара как к навыку командной гигиены: формулируем ожидания, проверяем границы, постепенно укрепляем самые рискованные места.

Мини‑чеклист на каждый важный кусок кода

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

2. Найдите инварианты: что обязано оставаться истинным на каждом шаге цикла/итерации/обработки. Это особенно помогает в «скользких» местах вроде индексов, указателей и границ массивов.

3. Проверьте границы: пустой ввод, один элемент, дубликаты, максимальные размеры, неожиданные значения, переполнения. Если есть сравнения ≤/< /≥/>, проверьте, что выбран именно тот знак.

С чего начать в реальном проекте

Выберите 1–2 критичных модуля, где ошибка дороже всего:

• платежи/биллинг, права доступа, обработка персональных данных;
• конвертация форматов, миграции, расчёты, которые сложно проверять глазами;
• участки, где уже были инциденты или много «горячих» фиксов.

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

Что читать и смотреть дальше

Ищите материалы по темам: логика Хоара, инварианты циклов, спецификации и контракты (Design by Contract), базовые идеи формальной верификации.

Если нужны примеры, шаблоны и инструменты/поддержка, загляните в /blog. Для обсуждения внедрения в команде и подбора тарифа (free/pro/business/enterprise) — /pricing.