Справочное руководство Ada 2012

11.4.2 Директивы Assert и Assertion_Policy

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

Директивы Assert, предикаты подтипов (см. 3.2.4), предусловия и постусловия (см. 6.1.1), и инварианты типов (см. 7.3.2) в совокупности называются утверждениями; их булевые выражения называются выражениями утверждений.

Директива Assertion_Policy используется для управления тем, игнорировать ли утверждения реализации, проверять их во время выполнения или обрабатывать каким-либо образом, определённым реализацией.

Синтаксис

Форма директивы pragma Assert следующая:

pragma Assert([Check =>] boolean_выражение[, [Message =>] string_выражение]);

Директива pragma Assert допускается в месте, где допускается declarative_item или statement.

Форма директивы pragma Assertion_Policy следующая:

pragma Assertion_Policy(policy_идентификатор);

pragma Assertion_Policy(
assertion_метка_аспекта => policy_идентификатор
{, assertion_метка_аспекта => policy_идентификатор});

Директива pragma Assertion_Policy разрешена только непосредственно внутри declarative_part, непосредственно внутри package_specification или как конфигурационная директива.

Правила разрешения имён

Ожидаемый тип для boolean_выражения директивы pragma Assert — любой булев тип. Ожидаемый тип для string_выражения директивы pragma Assert — тип String.

Правила легальности

assertion_метка_аспекта директивы pragma Assertion_Policy должна быть одной из Assert, Static_Predicate, Dynamic_Predicate, Pre, Pre'Class, Post, Post'Class, Type_Invariant, Type_Invariant'Class или какой-либо реализацией определенной метка_аспекта. policy_идентификатор должен быть Check, Ignore или каким-либо реализацией определенным идентификатором.

Статические семантика

Директива pragma Assertion_Policy определяет для каждого аспекта утверждения, указанного в pragma_argument_associations, следует ли проверять во время выполнения утверждения данного аспекта. идентификатор Check требует, чтобы выражения утверждений данного аспекта проверялись на то, что они вычисляются как True в указанные моменты для данного аспекта; идентификатор Ignore требует, чтобы выражение утверждения не вычислялось в эти моменты, и проверки во время выполнения не производились. Обратите внимание, что для аспектов предиката подтипа (см. 3.2.4), даже когда соответствующая Assertion_Policy — Ignore, предикат по-прежнему будет вычисляться в рамках тестов принадлежности и Valid attribute_references, и, если статический, по-прежнему будет влиять на итерацию цикла по подтипу и выбор case_statement_alternatives и variants.

Если в директиве не указаны assertion_метка_аспектаs, указанная политика применяется ко всем аспектам утверждений.

Директива pragma Assertion_Policy применяется к указанным аспектам утверждений в определенной области и применяется ко всем выражениям утверждений, указанным в этой области. Директива pragma Assertion_Policy, заданная в declarative_part или непосредственно внутри package_specification, применяется от места директивы до конца самого внутреннего содержащего декларативного региона. Область действия директивы pragma Assertion_Policy, заданной как конфигурационная директива, — это декларативный регион для всего модуля компиляции (или модулей), на который она распространяется.

Если директива pragma Assertion_Policy применяется к generic_instantiation, то директива pragma Assertion_Policy применяется ко всему экземпляру.

Если несколько директив Assertion_Policy применяются к заданному конструкту для данного аспекта утверждения, политика утверждения определяется той, которая находится в самом внутреннем содержащем регионе pragma Assertion_Policy, определяющем политику для аспекта утверждения. Если такая директива Assertion_Policy отсутствует, политика определяется реализацией.

Существует следующий определённый языком библиотечный пакет:

package Ada.Assertions is
pragma Pure(Assertions);

Assertion_Error : exception;

procedure Assert(Check : in Boolean);
procedure Assert(Check : in Boolean; Message : in String);

end Ada.Assertions;

Модуль компиляции, содержащий проверку утверждения (включая pragma Assert), имеет семантическую зависимость от модуля библиотеки Assertions.

Этот абзац был удалён.

Динамическая семантика

Если политика утверждения Assert, действующая в месте директивы pragma Assert, требует выполнения проверок, выработка директивы заключается в вычислении булева выражения, и если результат — False, вычислении аргумента Message, если он есть, и возбуждении исключения Assertions.Assertion_Error, с сообщением, если аргумент Message указан.

Вызов процедуры Assertions.Assert без параметра Message эквивалентен:

if Check = False then
raise Ada.Assertions.Assertion_Error;
end if;

Вызов процедуры Assertions.Assert с параметром Message эквивалентен:

if Check = False then
raise Ada.Assertions.Assertion_Error with Message;
end if;

Процедуры Assertions.Assert имеют эти эффекты независимо от действующей политики утверждения.

Ограниченные (времени выполнения) ошибки

Ошибка является ограниченной, если вызов потенциально блокирующей операции (см. 9.5.1) происходит во время вычисления выражения утверждения, связанного с вызовом или возвратом из защищённой операции. Если ограниченная ошибка обнаружена, возбуждается Program_Error. Если не обнаружена, выполнение продолжается нормально, но если вызов произошёл внутри защищённого действия, он может привести к тупику или к (вложенному) защищённому действию.

Разрешения реализации

Assertion_Error может быть объявлен переименованием реализацией определённого исключения из другого пакета.

Реализации могут определять свои собственные политики утверждений.

Если результат вызова функции в утверждении не нужен для определения значения выражения утверждения, реализация может опустить вызов функции. Это разрешение применимо даже если функция имеет побочные эффекты.

END_OF_DOCUMENT_MARKER

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

ПРИМЕЧАНИЯ

3 Обычно булево выражение в директиве Assert не должно вызывать функции с существенными побочными эффектами, когда результат выражения True, чтобы конкретная политика утверждений не влияла на нормальную работу программы.