Справочник по Ada (Ada 2022)
6.1.1 Предварительные и заключительные условия
Для подпрограммы, не являющейся экземпляром (включая формальную подпрограмму обобщения, подпрограмму обобщения, входной точку или тип доступа к подпрограмме), следующие определённые языком аспекты утверждения могут быть указаны с помощью спецификации_аспекта (см. 13.1.1):
Pre
Этот аспект задаёт конкретное предварительное условие для вызываемого объекта или типа доступа к подпрограмме; он должен быть задан с помощью выражения, называемого конкретным выражением предварительного условия. Если для объекта не указано, то выражение конкретного предварительного условия для объекта — это перечисление True.
Pre'Class
Этот аспект задаёт предварительное условие для всего класса для операцию с диспетчеризацией помеченного типа и его потомков; он должен быть задан с помощью выражения, называемого выражением предварительного условия для всего класса. Если для объекта не указано, то если для объекта не применяются другие предварительные условия для всего класса, то выражение предварительного условия для всего класса для объекта — это перечисление True.
Post
Этот аспект задаёт конкретное заключительное условие для вызываемого объекта или типа доступа к подпрограмме; он должен быть задан с помощью выражения, называемого конкретным выражением заключительного условия. Если для объекта не указано, то выражение конкретного заключительного условия для объекта — это перечисление True.
Post'Class
Этот аспект задаёт заключительное условие для всего класса для операцию с диспетчеризацией помеченного типа и его потомков; он должен быть задан с помощью выражения, называемого выражением заключительного условия для всего класса. Если для объекта не указано, то выражение заключительного условия для всего класса для объекта — это перечисление True.
Правила разрешения имён
Ожидаемый тип для выражения предварительного или заключительного условия — это любой тип boolean.
В выражении для аспектов Pre'Class или Post'Class для примитивной подпрограммы S помеченного типа T, имя, обозначающее формальный параметр (или S'Result) типа T, интерпретируется так, как будто у него есть (фиктивный) неабстрактный тип NT, который является формальным производным типом, предком которого является T, с непосредственно видимыми примитивными операциями. Аналогично, имя, обозначающее формальный параметр доступа (или S'Result для результирующего доступа) типа access-to-T, интерпретируется как имеющий тип access-to-NT. Результатом этой интерпретации является то, что единственные операции, которые могут быть применены к таким именам, — это те, которые определены для такого формального производного типа.
Для ссылки на атрибут с обозначением атрибута Old, если ссылка на атрибут имеет ожидаемый тип (или класс типов) или должна разрешиться в заданный тип, то же самое относится к префиксу; в противном случае префикс должен быть разрешён независимо от контекста.
Правила законности
Аспект 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 (включая T само по себе). Соответствующее выражение строится из связанного выражения следующим образом:
- Ссылок на формальные параметры S (или на само S) заменяются ссылками на соответствующие формальные параметры соответствующей унаследованной или переопределяющей подпрограммы S (или на соответствующую подпрограмму S само по себе).
Если примитивная подпрограмма S не абстрактна, но заданный потомок T абстрактный, то вызов S без диспетчеризации является незаконным, если какой-либо аспект Pre'Class или Post'Class, который применяется к S, не является статическим булевым выражением. Аналогично, примитивная подпрограмма абстрактного типа T, к которой применяется нестатический аспект Pre'Class или Post'Class, не должна быть префиксом ссылки на атрибут Access, и не должна быть фактической обобщённой подпрограммой для формальной подпрограммы, объявленной объявлением_формальной_конкретной_подпрограммы.
Если выполнение проверок требуется политиками утверждений Pre, Pre'Class, Post или Post'Class (см. 11.4.2), действующими в момент соответствующей спецификации аспекта, применимой к данной подпрограмме, входу или типу доступа к подпрограмме, то соответствующие выражения предварительного или заключительного условия считаются активированными.
Подвыражение выражения заключительного условия известно при входе, если это одно из:
- статическое подвыражение (см. 4.9);
- литерал, тип которого не имеет указанных аспектов Integer_Literal, Real_Literal или String_Literal, или функция, указанная таким атрибутом, имеет аспект Global, заданный как null;
- имя, статически обозначающее полное объявление константы, которое, как известно, не имеет переменных представлений (см. 3.3);
- имя, статически обозначающее неалиастный параметр in элементарного типа;
- ссылка на атрибут Old;
- вызов предопределённого оператора, где все операнды известны при входе;
- вызов функции, где функция имеет аспект Global => null, где все фактические параметры известны при входе;
- выбранный компонент известного при входе префикса;
- индексированный компонент известного при входе префикса, где все индексные выражения известны при входе;
- выражение в скобках, известное при входе;
- квалифицированное выражение или преобразование типа, операнд которого — выражение, известное при входе;
- условное выражение, где все условные выражения, выражения выбора и зависимые выражения известны при входе.
Подвыражение выражения заключительного условия считается безусловно вычисляемым, условно вычисляемым или повторяюще вычисляемым. Подвыражение считается безусловно вычисляемым, если оно не является условно или повторяюще вычисляемым.
Следующие подвыражения повторяюще вычисляются:
- Подвыражение предиката квантифицированного_выражения;
- Подвыражение выражения ассоциации_компонента_массива;
- Подвыражение выражения ассоциации_элемента_контейнера.
Для подвыражения, которое вычисляется условно, существует набор определяющих выражений, определяющих, вычисляется ли подвыражение на самом деле во время выполнения. Подвыражения, которые вычисляются условно, и их определяющие выражения приведены ниже:
- Для выражения if_expression, которое не вычисляется многократно, подвыражение любой части, кроме первого условия, вычисляется условно, а его определяющие выражения включают все условия выражения if_expression, которые предшествуют тексту подвыражения;
- Для выражения case_expression, которое не вычисляется многократно, подвыражение любого зависимоговыражения вычисляется условно, а его определяющие выражения включают выбирающеевыражение выражения case_expression;
- Для формы управления короткого замыкания, которая не вычисляется многократно, подвыражение правого операнда вычисляется условно, а его определяющие выражения включают левый операнд формы управления короткого замыкания;
- Для проверки принадлежности, которая не вычисляется многократно, подвыражение membership_choice, кроме первого, вычисляется условно, а его определяющие выражения включают проверяемоепростое выражение и предшествующие membership_choiceы проверки принадлежности.
Условно вычисляемое подвыражение считается невычисленным во время выполнения, если его набор определяющих выражений известен при входе, а при вычислении при входе их значения таковы, что данное подвыражение не вычисляется.
Для префикса X, обозначающего объект типа без ограничений, определено следующее атрибут:
X'Old
Каждый X'Old в выражении пост условия, которое разрешено, кроме тех, которые встречаются в подвыражениях, которые определены как невычисленные, обозначает константу, которая неявно объявлена в начале тела подпрограммы, тела входа или оператора accept.
Неявно объявленная сущность, обозначаемая каждой записью X'Old, объявляется следующим образом:
Если X имеет анонимный тип доступа, определённый access_definition A, то
X'Old : constant A := X;
Если X имеет конкретный помеченный тип T, то
anonymous : constant T'Class := T'Class(X);
X'Old : T renames T(anonymous);
X'Old : T renames T(anonymous);
где имя X'Old обозначает переименование объекта.
В противном случае
X'Old : constant S := X;
где S — номинальный подтип X. Это включает случай, когда тип S — анонимный тип массива или универсальный тип.
Тип и номинальный подтип X'Old подразумеваются вышеприведёнными определениями.
Ссылка на этот атрибут разрешена только внутри выражения пост условия. Префикс префикса атрибута Old attribute_reference не должен содержать атрибута Result attribute_reference, атрибута Old attribute_reference, ни использования сущности, объявленной внутри выражения пост условия, но не внутри префикса (например, параметра цикла вложенного quantified_expression).
Для префикса F, обозначающего объявление функции или тип доступа к функции, определён следующий атрибут:
F'Result
Внутри выражения пост условия для F обозначает возвращаемый объект вызова функции, для которого вычисляется выражение пост условия. Тип этого атрибута — тип подтипа результата функции или типа доступа к функции, за исключением выражения Post'Class пост условия для функции с управляемым результатом или с управляемым результатом доступа; в этих случаях тип атрибута описан выше как часть Правил разрешения имён для Post'Class.
Использование этого атрибута разрешено только в выражении пост условия для F.
Для префикса E, обозначающего объявление входа семейства входов (см. 9.5.2), определён следующий атрибут:
E'Index
Внутри выражения предусловия или пост условия для семейства входов E обозначает значение индекса входа для вызова E. Номинальный подтип этого атрибута — подтип индекса входа.
Использование этого атрибута разрешено только в выражении предусловия или пост условия для E.
Динамические семантика
При вызове подпрограммы или входа, после вычисления фактических параметров, проверки предусловия выполняются следующим образом:
- Конкретная проверка предусловия начинается с вычисления конкретного выражения предусловия, применимого к подпрограмме или входу, если оно разрешено; если выражение вычисляется в False, то поднимается Assertions.Assertion_Error; если выражение не разрешено, проверка проходит успешно.
- Проверка предусловия класса начинается с вычисления всех разрешённых выражений предусловия класса, применимых к подпрограмме или входу. Если и только если все выражения предусловия класса вычисляются в False, поднимается Assertions.Assertion_Error.
Проверки предусловия выполняются в произвольном порядке, и если любое из выражений предусловия класса вычисляется в True, то не определено, будут ли вычисляться другие выражения предусловия класса. Проверки предусловия и любая проверка разработки тела подпрограммы выполняются в произвольном порядке. При вызове защищённой операции проверки выполняются до начала защищённого действия. При вызове входа проверки выполняются до проверки открыт ли вход.
После успешного возврата из вызова подпрограммы или входа, перед копированием обратно параметров in out или out по копированию, выполняется проверка пост условия. Это состоит из вычисления всех разрешённых конкретных и повсеместных выражений пост условия, применимых к подпрограмме или входу. Если какое-либо из выражений пост условия вычисляется в False, то поднимается Assertions.Assertion_Error. Выражения пост условия вычисляются в произвольном порядке, и если какое-либо выражение пост условия вычисляется в False, то не определено, будут ли вычисляться другие выражения пост условия. Проверка пост условия и любые проверки ограничений или предикатов, связанные с параметрами in out или out, выполняются в произвольном порядке.
При вызове входа задачи проверка пост условия выполняется перед окончанием rendez-vous; при вызове защищённой операции проверка пост условия выполняется перед окончанием защищённого действия вызова. Проверка пост условия для любого вызова выполняется перед финализацией любых неявно объявленных констант, связанных (как описано выше) со ссылками атрибутов Old attribute_reference, но после финализации любых других сущностей, уровень доступности которых — уровень выполнения вызываемого конструкта.
Если проверка предусловия или пост условия терпит неудачу, исключение поднимается в момент вызова; исключение не может обрабатываться внутри вызываемой подпрограммы или входа. Аналогично, любое исключение, поднятое при вычислении выражения предусловия или пост условия, поднимается в момент вызова.
Для любого вызова подпрограммы или входа S (включая вызовы диспетчеризации), проверки, которые выполняются для проверки конкретных выражений предусловия и конкретных и повсеместных выражений пост условия, определяются теми, которые для подпрограммы или входа фактически вызваны. Обратите внимание, что выражения повсеместного пост условия, проверенные проверкой пост условия, которая является частью вызова примитивной подпрограммы типа T, включают все выражения повсеместного пост условия, исходящие от любого предка T, даже если вызываемая примитивная подпрограмма унаследована от типа T1 и некоторые выражения пост условия не применяются к соответствующей примитивной подпрограмме T1. Любые операции в выражении повсеместного пост условия, которые были разрешены как примитивные операции (номинального) формального производного типа NT, в вычислении пост условия связаны с соответствующими операциями типа, идентифицированного управляющим тегом вызова S. Это относится как к вызовам диспетчеризации, так и к вызовам без диспетчеризации S.
Проверка предословия, относящаяся ко всему классу для вызова подпрограммы или входа S, состоит только из проверки выражений предословия, относящихся к обозначенному вызываемому элементу (не обязательно к вызываемому). Любые операции в таком выражении, которые были разрешены как примитивные операции (предполагаемого) формального производного типа NT, при оценке предословия связаны с соответствующими операциями типа, определенного управляющим тегом вызова S. Это относится как к вызовам с диспетчеризацией, так и к вызовам без диспетчеризации на S.
В целях вышеуказанных правил вызов унаследованной подпрограммы рассматривается как вызов подпрограммы S', тело которой состоит только из вызова (с соответствующими преобразованиями) неунаследованной подпрограммы S, из которой была получена унаследованная подпрограмма. Не определено, выполняются ли выражения предословия или постусловия, относящиеся ко всему классу, которые эквивалентны (в отношении выполнения тел неунаследованных функций) для S и S' один или два раза. Если они выполняются только один раз, возвращаемое значение используется для обеих связанных проверок.
Для вызова через значение доступа к подпрограмме, проверки предословия и постусловия выполняются в соответствии с подпрограммой или входом, обозначенным префиксом ссылки на атрибут Access, который произвел значение. Кроме того, выполняется проверка предословия любого выражения предословия, связанного с типом доступа к подпрограмме. Аналогично, выполняется проверка постусловия любого выражения постусловия, связанного с типом доступа к подпрограмме.
Для вызова универсальной формальной подпрограммы проверки предословия и постусловия выполняются в соответствии с подпрограммой или входом, обозначенным фактической подпрограммой, а также с любым специфическим предословием и специфическим постусловием самой формальной подпрограммы.
Разрешения реализации
Реализация может оценить подвыражение, известное при входе, выражения постусловия сущности в месте создания констант X'Old для сущности, с обычной оценкой выражения постусловия или с обоих.
ПРИМЕЧАНИЕ 1 Предословие проверяется непосредственно перед вызовом. Если другая задача может изменить любое значение, от которого зависит выражение предословия, предословие может принять значение False внутри тела подпрограммы или входа.
ПРИМЕЧАНИЕ 2 Пример использования этих аспектов и атрибутов см. в определениях подсистемы потоков в 13.13.1.
