Контракты Ada 2012: Pre, Post, инварианты

Контракты Ada 2012 — предусловия, постусловия, инварианты и предикаты — делают обещания подпрограмм и типов частью самого языка, а не комментариев.

Контракт (aspect-контракт Ada 2012) — формальное, проверяемое утверждение о подпрограмме или типе: что обязан обеспечить вызывающий (предусловие Pre), что гарантирует реализация (постусловие Post), какое свойство всегда истинно для значений типа (Type_Invariant, Predicate).

До Ada 2012 контракты жили в комментариях: «требуется: x > 0; гарантируется: результат отсортирован». Комментарии не проверяются, устаревают и лгут. Ada 2012 совершила тихую революцию: перенесла Design by Contract — методологию, выросшую из языка Eiffel, — прямо в синтаксис. Теперь обещания подпрограммы записываются аспектами (aspect) и проверяются автоматически: либо во время выполнения как исключение Assertion_Error, либо — что мощнее — статически инструментом SPARK ещё до запуска.

Предусловия и постусловия

Предусловие (Pre) — обязательство вызывающего: при каких условиях звать подпрограмму вообще допустимо. Постусловие (Post) — обещание реализации: что будет истинно после возврата, если предусловие соблюдено. Между ними проходит чёткая граница ответственности: нарушил Pre — виноват клиент; соблюдён Pre, но нарушен Post — виновата реализация. Это превращает отладку из спора в протокол.

function Sqrt (X : Float) return Float
   with Pre  => X >= 0.0,                       -- клиент не должен звать с X < 0
        Post => abs (Sqrt'Result * Sqrt'Result - X) <= 0.001;
   --  гарантия: квадрат результата близок к X

procedure Sort (A : in out Int_Array)
   with Post => (for all I in A'First .. A'Last - 1 => A (I) <= A (I + 1));
   --  гарантия: после сортировки массив неубывающий

В постусловии используются мощные конструкции: атрибут 'Result (значение, которое вернула функция), квантор for all («для всех») и for some («существует»), а также атрибут 'Old — значение выражения до вызова. 'Old особенно ценен: он позволяет связать «было» и «стало».

procedure Increment (Counter : in out Natural)
   with Pre  => Counter < Natural'Last,
        Post => Counter = Counter'Old + 1;
   --  читается буквально: после вызова Counter на единицу больше прежнего

Инварианты типов и предикаты подтипов

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

package Dates is
   type Date is private
      with Type_Invariant => Is_Valid (Date);   -- любая видимая дата корректна

   function Is_Valid (D : Date) return Boolean;
   function Make (Y, M, D : Integer) return Date
      with Pre => M in 1 .. 12 and D in 1 .. 31;
private
   type Date is record
      Year  : Integer;
      Month : Integer range 1 .. 12;
      Day   : Integer range 1 .. 31;
   end record;
   function Is_Valid (D : Date) return Boolean is
      (D.Day <= Days_In_Month (D.Year, D.Month));
end Dates;

Предикат подтипа (Dynamic_Predicate, Static_Predicate) — ограничение, более выразительное, чем простой диапазон range. Диапазоном не выразить «чётное число» или «множество разрешённых кодов» — предикатом можно.

subtype Even is Integer
   with Dynamic_Predicate => Even mod 2 = 0;     -- только чётные

type Weekday is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
subtype Working_Day is Weekday
   with Static_Predicate => Working_Day in Mon .. Fri;  -- пн..пт
--  Присваивание значения, не удовлетворяющего предикату,
--  нарушает проверку так же, как выход за range.

Design by Contract и мост к SPARK

Контракты — это не просто «продвинутые assert». Это спецификация поведения на языке, понятном и человеку, и инструменту. В обычной Ada контракты проверяются динамически (если включены прагмой pragma Assertion_Policy (Check)): нарушение даёт исключение Assertion_Error точно в момент и в месте, где обещание не выполнилось. Но настоящая сила раскрывается в связке со SPARK — формально верифицируемым подмножеством Ada. Инструмент GNATprove читает те же самые Pre/Post/инварианты и математически доказывает, что код им соответствует при всех возможных входах, без единого запуска. Тестирование показывает наличие ошибок на конкретных примерах; доказательство показывает их отсутствие в принципе. Об этом — отдельный урок-обзор далее в разделе.

Практическая ценность колоссальна. Один и тот же контракт служит трижды: как документация (читаемое обещание), как динамическая проверка при тестировании и отладке, и как цель формального доказательства в SPARK. Написав контракт однажды, вы получаете все три применения бесплатно — редкий случай, когда строгость не противоречит экономии усилий.

Как работает под капотом

Аспект Pre компилятор превращает в проверку, логически выполняемую в точке вызова перед входом в тело; Post — в проверку после вычисления результата, но до возврата управления. Выражения 'Old заставляют среду сохранить копию соответствующего значения на входе, чтобы было с чем сравнить на выходе. Все эти проверки управляются политикой утверждений: в отладочной сборке их включают (Check), в финальной — могут отключить (Ignore) ради скорости, как обычные assert. Принципиально иной режим — SPARK: там контракты не выполняются, а доказываются на этапе анализа, и в рантайме от них не остаётся ничего, потому что доказано отсутствие нарушений.

Контракты в проектировании, а не только в коде

Ценность контрактов раскрывается шире, если смотреть на них как на инструмент проектирования, а не только как на исполняемые проверки. Записывая Pre и Post, инженер вынужден заранее, ещё до реализации, ответить на ключевые вопросы: при каких условиях эту операцию вообще законно вызывать? что именно она гарантирует на выходе? какие свойства данных она сохраняет? Эти вопросы — суть проектирования интерфейса, и контракт заставляет ответить на них явно, а не оставить «на интуицию». Нередко сам процесс написания контракта вскрывает недодуманные случаи: «а что, если массив пуст?», «а гарантируем ли мы порядок?» — вопросы, которые иначе всплыли бы дефектом в эксплуатации.

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

Стоимость и дисциплина контрактов

Важно трезво понимать и издержки. Динамические проверки контрактов имеют цену во время выполнения, поэтому их обычно включают в отладочных и тестовых сборках и могут выключать в финальной — точно так же, как обычные assert. Из этого следует дисциплинарное правило: контракт не должен иметь побочных эффектов и не должен быть единственным местом, где происходит важная логика, — иначе при отключении проверок поведение программы изменится. Выражения в Pre/Post обязаны быть чистыми: они только наблюдают состояние, но не меняют его. Соблюдая это, вы получаете идеальную ситуацию: в разработке контракты ловят нарушения немедленно и точно, в релизе не замедляют код, а при переходе на SPARK те же самые контракты доказываются статически и не нуждаются в рантайм-проверках вовсе. Один артефакт служит трём режимам, и в каждом он на своём месте.

Квантование и выразительность постусловий

Отдельного восхищения заслуживает выразительная сила, которую кванторы придают постусловиям. Конструкции for all I in Range => Условие («для всех») и for some I in Range => Условие («существует») позволяют описывать свойства целых структур данных, а не отдельных значений. Постусловие сортировки for all I => A (I) <= A (I + 1) точно выражает «массив упорядочен» одной строкой. Свойство поиска можно записать как «если результат не ноль, то элемент по найденному индексу равен искомому». Свойство вставки — «длина увеличилась на единицу и все прежние элементы сохранились». Это язык спецификации, встроенный прямо в язык программирования.

Особенно ценны кванторы в связке со SPARK. Для динамической проверки квантор по большому диапазону мог бы быть дорогим (он буквально перебирает все индексы), поэтому в рантайме такие постусловия включают обычно при отладке. Но в SPARK квантор не выполняется, а доказывается: GNATprove рассуждает о свойстве математически, для всех элементов сразу, без всякого перебора. Тогда выразительное постусловие с for all становится строгой спецификацией, которую инструмент проверяет логически. Так кванторы раскрывают двойную природу контрактов Ada: читаемое человеком описание намерения, которое одновременно служит формальной целью доказательства. Умение формулировать сильные, точные постусловия с кванторами — навык, который отличает по-настоящему надёжный код от просто работающего.

Закрепим место контрактов в арсенале надёжности Ada. Если исключения и runtime-проверки ловят нарушения по факту, во время выполнения, то контракты поднимают планку до спецификации поведения: они описывают, что подпрограмма обязана получить на входе и гарантировать на выходе, и что всегда истинно для значений типа. Записанные аспектами Ada 2012, эти обещания перестают быть комментариями, которые лгут и устаревают, и становятся проверяемыми утверждениями — динамически при тестировании или статически в SPARK. Один и тот же контракт служит документацией, проверкой и целью доказательства. Привычка формулировать предусловия, постусловия и инварианты ещё на этапе проектирования заставляет продумать краевые случаи заранее, а не ловить их дефектами потом. Именно поэтому контракты — не «продвинутые assert», а способ мышления о корректности, который Ada встроила в язык и который остаётся ценным ориентиром при работе на любом языке.

Частые ошибки

• Считать контракты исполняемыми всегда. Динамические проверки работают, только если включена политика Assertion_Policy (Check); в релизе их часто выключают. Не закладывайте в Pre побочные эффекты — выражение должно быть чистым.
• Путать Pre и Post по ответственности. Pre — обязанность вызывающего, Post — обязанность реализации. Нарушение Pre указывает на ошибку у клиента, а не в теле.
• Забыть 'Old при сравнении «было/стало». Без Counter'Old в постусловии вы сравните новое значение с самим собой. 'Old фиксирует входное состояние.
• Писать слишком слабые контракты. Post => True ничего не гарантирует. Полезное постусловие выражает существо результата (отсортированность, сохранение длины, диапазон).

Итоги

• Ada 2012 встроила Design by Contract в язык: Pre, Post, Type_Invariant, предикаты подтипов.
• Pre — обязанность вызывающего, Post — обещание реализации; 'Result, 'Old, for all/for some делают их выразительными.
• Инвариант типа держится на границах абстракции; предикат подтипа выражает то, что не выразить диапазоном (чётность, набор значений).
• Динамически нарушение даёт Assertion_Error; в SPARK те же контракты доказываются статически для всех входов.
• Один контракт = документация + проверка при тестах + цель формального доказательства.