Справочник Ada 2012

6.1.1 Предварительные и заключительные условия

Для подпрограммы без экземпляра, подпрограммы-генератора или входа могут быть указаны следующие определяемые языком аспекты с помощью aspect_specification (см. 13.1.1):

Pre

Этот аспект задаёт конкретное предварительное условие для вызываемого сущности; он должен быть указан с помощью выражения, называемого конкретным выражением предварительного условия. Если для сущности он не указан, то конкретным выражением предварительного условия для этой сущности является перечислительная константа True.

Pre'Class

Этот аспект задаёт предварительное условие для всего класса для операции помеченного типа и его потомков; он должен быть указан с помощью выражения, называемого выражением предварительного условия для всего класса. Если он не указан для сущности, и ни одно другое предварительное условие для всего класса не применяется, то выражение предварительного условия для всего класса для данной сущности — перечислительная константа True.

Post

Этот аспект задаёт конкретное заключительное условие для вызываемой сущности; он должен быть указан с помощью выражения, называемого конкретным выражением заключительного условия. Если он не указан для сущности, то конкретным выражением заключительного условия для этой сущности является перечислительная константа True.

Post'Class

Этот аспект задаёт заключительное условие для всего класса для операции помеченного типа и его потомков; он должен быть указан с помощью выражения, называемого выражением заключительного условия для всего класса. Если он не указан для сущности, то выражение заключительного условия для всего класса для данной сущности — перечислительная константа True.

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

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

В выражении аспекта Pre'Class или Post'Class для примитивной подпрограммы S помеченного типа T имя, обозначающее формальный параметр (или S'Result) типа T, интерпретируется как имеющее (условный) тип NT, который является формальным производным типом, предком которого является T, с непосредственно видимыми примитивными операциями. Аналогично, имя, обозначающее формальный параметр доступа (или S'Result) типа access-to-T, интерпретируется как имеющий тип access-to-NT. Это означает, что к таким именам можно применять только операции, определённые для такого формального производного типа.

Для attribute_reference с attribute_designator Old, если ожидаемый тип или требуется разрешение на определённый тип, то это же относится к prefix; в противном случае prefix разрешается независимо от контекста.

Правила законности

Аспект Pre или Post не должен быть указан для абстрактной подпрограммы или процедуры null. Для такой подпрограммы могут быть указаны только аспекты Pre'Class и Post'Class.

Если тип T имеет неявную подпрограмму P, унаследованную от родительского типа T1, и омограф (см. 8.3) P из родительского типа T2, и

соответствующая примитивная подпрограмма P1 типа T1 не является ни null, ни абстрактной; и

выражение предварительного условия True не применяется к P1 (неявно или явно); и

существует выражение предварительного условия для всего класса, которое применяется к соответствующей примитивной подпрограмме P2 типа T2, которое не полностью соответствует никакому выражению предварительного условия, применимому к P1,

то:

Если тип T является абстрактным, то неявная подпрограмма P является абстрактной.

В противном случае, подпрограмма P требует переопределения и должна быть переопределена неабстрактной подпрограммой.

Если переименование подпрограммы или входа S1 переопределяет унаследованную подпрограмму S2, то переопределение является незаконным, если каждое выражение предварительного условия, применяемое к S1, полностью соответствует некоторому выражению предварительного условия, применимому к S2, и каждое выражение предварительного условия, применяемое к S2, полностью соответствует некоторому выражению предварительного условия, применимому к S1.

Pre'Class не должен быть указан для переопределяющей примитивной подпрограммы помеченного типа T, если аспект Pre'Class не указан для соответствующей примитивной подпрограммы какого-либо предка T.

Помимо мест, где обычно применяются правила законности (см. 12.3), эти правила также применяются в закрытой части экземпляра генерируемого блока.

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

Если для примитивной подпрограммы S помеченного типа T указан аспект Pre'Class или Post'Class, или такой аспект по умолчанию равен True, то соответствующее выражение также применяется к соответствующей примитивной подпрограмме S каждого потомка T. Соответствующее выражение строится из связанного выражения следующим образом:

Ссылки на формальные параметры S (или на S само по себе) заменяются ссылками на соответствующие формальные параметры соответствующей унаследованной или переопределённой подпрограммы S (или на соответствующую подпрограмму S само по себе).

Примитивная подпрограмма S является незаконной, если она не является абстрактной, и соответствующее выражение для аспекта Pre'Class или Post'Class было бы незаконным.

Если выполнение проверок требуется политиками утверждений Pre, Pre'Class, Post или Post'Class (см. 11.4.2), действующими в момент указания соответствующего аспекта, применимого к данной подпрограмме или входу, то соответствующие выражения предварительного или заключительного условия считаются активированными.

Выражение является потенциально невычисляемым, если оно находится в:

любой части выражения if_expression, кроме первого условия;

выражении зависимого dependent_expression выражения case_expression;

предикате predicate выражения quantified_expression;

правом операнде краткого условного оператора; или

выборе membership_choice, кроме первого в операции членства.

Для префикса X, обозначающего объект неограниченного типа, определён следующий атрибут:

X'Old

Каждый X'Old в выражении заключительного условия, которое активировано, обозначает константу, неявно объявленную в начале тела подпрограммы, тела входа или оператора accept.

Неявно объявленная сущность, обозначаемая каждой записью X'Old, объявляется следующим образом:

Если X относится к анонимному типу доступа, определённому с помощью access_definition A, тогда

X'Old : const A := X;

Если X относится к конкретному помеченному типу T, тогда

анонимный : const T'Class := T'Class(X);
X'Old : T переименовывает T(анонимный);

где имя X'Old обозначает объект переименования.

В противном случае

X'Old : const S := X;

где S — номинальный подтип X. Это включает случай, когда тип S — это анонимный массивный тип или универсальный тип.

Номинальный подтип X'Old соответствует вышеуказанным определениям. Ожидаемый тип префикса атрибута Old — это тип атрибута. Аналогично, если атрибут Old должен быть разрешён на некоторый тип, то префикс атрибута должен быть разрешён на этот тип.

Ссылка на этот атрибут разрешена только в выражении заключительного условия. Префикс атрибута Old не должен содержать атрибут Result, ни атрибут Old, ни ссылку на сущность, объявленную в выражении заключительного условия, но не в самом префиксе (например, параметр цикла вложенного quantified_expression). Префикс атрибута Old, который потенциально не вычисляется, должен статически обозначать сущность.

END_OF_DOCUMENT_MARKER ```

Для префикса F, обозначающего объявление функции, определён следующий атрибут:

F'Result

Внутри выражения пост условия для функции F обозначает объект результата функции. Тип этого атрибута — тип результата функции, за исключением выражения пост условия Post'Class для функции с контролируемым результатом или с контролируемым результатом доступа. Для контролируемого результата тип атрибута — T'Class, где T — тип результата функции. Для контролируемого результата доступа тип атрибута — анонимный тип доступа, назначенный тип которого — T'Class, где T — назначенный тип типа результата функции.

Использование этого атрибута разрешено только внутри выражения пост условия для F.

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

При вызове подпрограммы или входа, после оценки фактических параметров, выполняются проверки предусловия следующим образом:

Конкретная проверка предусловия начинается с оценки конкретного выражения предусловия, применимого к подпрограмме или входу, если оно активировано; если выражение вычисляется как False, возникает Assertions.Assertion_Error; если выражение не активировано, проверка выполняется успешно.

Проверка предусловия класса начинается с оценки всех активированных выражений предусловия класса, применимых к подпрограмме или входу. Если и только если все выражения предусловия класса вычисляются как False, возникает Assertions.Assertion_Error.

Проверки предусловия выполняются в произвольном порядке, и если любое из выражений предусловия класса вычисляется как True, не определено, будут ли вычисляться другие выражения предусловия класса. Проверки предусловия и любая проверка разработки тела подпрограммы выполняются в произвольном порядке. Не определено, выполняются ли проверки в вызове защищённой операции до или после начала защищённого действия. Для вызова входа проверки выполняются до проверки, открыт ли вход.

При успешном возвращении из вызова подпрограммы или входа, до копирования обратно параметров in out и out по копированию, выполняется проверка пост условия. Это включает в себя оценку всех активированных выражений пост условия конкретного и класса, применимых к подпрограмме или входу. Если какое-либо из выражений пост условия вычисляется как False, то возникает Assertions.Assertion_Error. Выражения пост условия оцениваются в произвольном порядке, и если какое-либо выражение пост условия вычисляется как False, не определено, будут ли оцениваться другие выражения пост условия. Проверка пост условия и любые проверки ограничений или предикатов, связанные с параметрами in out или out, выполняются в произвольном порядке.

Для вызова входа задачи проверка пост условия выполняется до завершения rendez-vous; для вызова защищённой операции проверка пост условия выполняется до завершения защищённого действия вызова. Проверка пост условия для любого вызова выполняется до финализации любых неявно объявленных констант, связанных (как описано выше) со старыми ссылками_атрибута, но после финализации любых других сущностей, уровень доступа которых соответствует выполнению вызываемого конструкта.

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

Для любого вызова подпрограммы или входа S (включая вызовы диспетчеризации), проверки, выполняемые для проверки конкретных выражений предусловия и конкретных и выражений пост условия класса, определяются теми, которые выполняются для фактически вызываемой подпрограммы или входа. Обратите внимание, что выражения пост условия класса, проверенные проверкой пост условия, являющейся частью вызова примитивной подпрограммы типа T, включают все выражения пост условия класса, исходящие от любого предка T, даже если вызываемая примитивная подпрограмма унаследована от типа T1 и некоторые из выражений пост условия не применимы к соответствующей примитивной подпрограмме T1. Любые операции внутри выражения пост условия класса, которые были разрешены как примитивные операции (номинального) формального производного типа NT, при вычислении пост условия связаны с соответствующими операциями типа, идентифицированного контролирующей меткой вызова S. Это относится как к вызовам диспетчеризации, так и к вызовам без диспетчеризации S.

Проверка предусловия класса для вызова подпрограммы или входа S состоит только в проверке выражений предусловия класса, которые применимы к обозначаемому вызываемому элементу (не обязательно к тому, который вызывается). Любые операции внутри такого выражения, которые были разрешены как примитивные операции (номинального) формального производного типа NT, при вычислении предусловия привязаны к соответствующим операциям типа, определяемого контролирующей меткой вызова S. Это относится как к вызовам диспетчеризации, так и к вызовам без диспетчеризации S.

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

ПРИМЕЧАНИЯ

5 Предусловие проверяется непосредственно перед вызовом. Если другая задача может изменить любое значение, от которого зависит выражение предусловия, предусловие не обязательно должно выполняться внутри тела подпрограммы или входа.