Руководство по Ada (Ada 2022)
11.4.2 Директивы Assert и Assertion_Policy
Директива Assert используется для проверки истинности булевого выражения в определенной точке последовательности объявлений или операторов.
Директивы Assert, предикаты подтипов (см. 3.2.4), предусловия и постусловия (см. 6.1.1), инварианты типов (см. 7.3.2) и значения начального состояния по умолчанию (см. 7.3.3) коллективно называются утверждениями; их булевы выражения называются выражениями утверждений.
Директива Assertion_Policy используется для управления тем, будут ли утверждения игнорироваться реализацией, проверяться во время выполнения или обрабатываться каким-либо определённым реализацией способом.
Синтаксис
Форма директивы pragma Assert следующая:
Форма директивы pragma Assertion_Policy следующая:
pragma Assertion_Policy(policy_идентификатор);
pragma Assertion_Policy(
assertion_аспект_метка => policy_идентификатор
{, 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, Default_Initial_Condition или какой-либо определённый реализацией (утверждение) аспект_метка. policy_идентификатор должен быть либо Check, Ignore, либо какой-либо определённый реализацией идентификатор.
Статическая семантика
Директива pragma Assertion_Policy определяет для каждого аспекта утверждения, указанного в pragma_argument_associations, следует ли выполнять проверки утверждений данного аспекта во время выполнения. policy_идентификатор Check требует, чтобы выражения утверждений данного аспекта проверялись на истинность (равно True) в указанных точках; policy_идентификатор Ignore требует, чтобы выражение утверждения не оценивалось в этих точках, и проверки во время выполнения не выполнялись. Обратите внимание, что для аспектов предикатов подтипов (см. 3.2.4), даже если соответствующая Assertion_Policy — Ignore, предикат всё равно будет оцениваться в рамках проверок на членство и Valid attribute_references, и если статический, то всё равно будет влиять на итерацию цикла по подтипу, и выбор case_statement_alternatives и variants.
Если assertion_аспект_метка не указаны в директиве, указанная политика применяется ко всем аспектам утверждений.
Директива 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
with Pure is
with Pure is
Assertion_Error : exception;
procedure Assert(Check : in Boolean);
procedure Assert(Check : in Boolean; Message : in String);
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;
raise Ada.Assertions.Assertion_Error;
end if;
Вызов процедуры Assertions.Assert с параметром Message эквивалентен:
if Check = False then
raise Ada.Assertions.Assertion_Error with Message;
end if;
raise Ada.Assertions.Assertion_Error with Message;
end if;
Процедуры Assertions.Assert имеют эти эффекты независимо от действующей политики утверждений.
Ограниченные (временно́й) ошибки
Вызов потенциально блокирующей операции (см. 9.5.1) во время вычисления выражения утверждения, связанного с вызовом или возвратом из защищенной операции, является ограниченной ошибкой. Если ограниченная ошибка обнаружена, возбуждается Program_Error. Если она не обнаружена, выполнение продолжается нормально, но если она вызвана внутри защищенного действия, это может привести к тупику или (вложенному) защищенному действию.
Требования к реализации
Любое выражение постусловия, инварианта типа или значения начального состояния по умолчанию, встречающееся в спецификации модуля языка, включено (см. 6.1.1, 7.3.2 и 7.3.3).
Вычисление любого такого выражения постусловия, инварианта типа или значения начального состояния по умолчанию должно либо вернуть True, либо распространить исключение из raise_expression, который появляется в выражении утверждения.
END_OF_DOCUMENT_MARKER Любое условие предварительной проверки, встречающееся в спецификации языка-определённого блока, включено (см. 6.1.1), если не отключено (см. 11.5). Аналогично, любые проверки предиката для подтипа, встречающиеся в спецификации языка-определённого блока, включены (см. 3.2.4), если не отключены.
Разрешения для реализации
Assertion_Error может быть объявлен путём переименования исключения, определённого реализацией в другом пакете.
Реализации могут определять собственные политики проверки утверждений.
Если результат вызова функции в утверждении не используется для определения значения выражения утверждения, реализация имеет право опустить вызов функции. Это разрешение действует даже в случае, если функция имеет побочные эффекты.
Реализация может запретить указание выражения утверждения, если вычисление выражения имеет побочный эффект, такой, что непосредственное повторное вычисление выражения может привести к другому значению. Аналогично, реализация может запретить указание выражения утверждения, которое проверяется как часть вызова или возврата из вызываемого объекта C, если вычисление выражения имеет побочный эффект, такой, что вычисление другого выражения утверждения, связанного с тем же вызовом (или возвратом) C, может привести к другому значению, чем в случае, когда первое выражение не было вычислено.
ПРИМЕЧАНИЕ Обычно булево выражение в директиве Assert не должно вызывать функции, имеющие значительные побочные эффекты, когда результат выражения True, чтобы конкретная политика проверки утверждений не влияла на нормальную работу программы.
