Справочник по Ada (Ada 2022)

7.3.2 Инварианты типов

Для частного типа, частного расширения или интерфейса могут быть указаны следующие определяемые языком аспекты утверждений с помощью aspect_specification (см. 13.1.1):

Type_Invariant

Этот аспект должен быть указан с помощью выражения, называемого выражением инварианта. Type_Invariant может быть указан в объявлении частного типа, в объявлении частного расширения или в полном объявлении типа, которое объявляет завершение частного типа или частного расширения.

Type_Invariant'Class

Этот аспект должен быть указан с помощью выражения, называемого выражением инварианта. Type_Invariant'Class может быть указан в объявлении частного типа, объявлении частного расширения или полном объявлении типа для типа интерфейса. Type_Invariant'Class определяет инвариант типа класса для помеченного типа. Аспект Type_Invariant'Class не наследуется, но его эффекты аддитивны, как определено ниже.

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

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

В выражении инварианта идентификатор первого подтипа связанного типа обозначает текущий экземпляр типа. В выражении инварианта для аспекта Type_Invariant типа T тип этого текущего экземпляра — T. В выражении инварианта для аспекта Type_Invariant'Class типа T тип этого текущего экземпляра интерпретируется так, как будто у него есть (гипотетический) неабстрактный тип NT, который является видимым формальным производным типом, предком которого является тип T. Влияние этой интерпретации заключается в том, что к этому текущему экземпляру могут быть применены только те операции, которые определены для такого формального производного типа.

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

Аспект Type_Invariant'Class не должен быть указан для неупомянутого типа. Аспект Type_Invariant не должен быть указан для абстрактного типа.

Если расширение типа происходит непосредственно внутри видимой части спецификации пакета, в точке, где видима и наследуется частная операция какого-либо предка, и выражение Type_Invariant'Class относится к этому предку, то унаследованная операция должна быть абстрактной или переопределённой.

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

Если аспект Type_Invariant указан для типа T, то выражение инварианта относится к T.

Если аспект Type_Invariant'Class указан для помеченного типа T, то соответствующее выражение также относится к каждому неабстрактному потомку T1 типа T (включая сам T, если он не является абстрактным). Соответствующее выражение строится из связанного выражения следующим образом:

Ссылки на компоненты без дискриминантов T (или на сам T) заменяются ссылками на соответствующие компоненты T1 (или на сам T1).

Ссылки на дискриминанты T заменяются ссылками на соответствующий дискриминант T1 или на указанное значение для дискриминанта, если дискриминант задан в derived_type_definition для какого-либо типа, являющегося предком T1 и потомком T (см. 3.7).

Для неабстрактного типа T вызываемый элемент называется граничным элементом для T, если он объявлен в непосредственной области видимости T (или экземпляром генерируемого блока, а генерик объявлен в непосредственной области видимости типа T), или является потоком чтения или ввода, ориентированным на атрибут типа T, и либо:

T — это частный тип или частное расширение, и вызываемый элемент виден вне непосредственной области видимости типа T или переопределяет унаследованную операцию, которая видна вне непосредственной области видимости T; или

T — это расширение записи, а вызываемый элемент — примитивная операция, видимая вне непосредственной области видимости типа T, или переопределяет унаследованную операцию, которая видна вне непосредственной области видимости T.

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

Если один или несколько выражений инварианта применяются к неабстрактному типу T, то проверка инварианта выполняется в следующих местах, для указанных объекта(ов):

После успешной инициализации объекта типа T по умолчанию (см. 3.3.1), проверка выполняется на новом объекте, если частичный вид T не имеет неизвестных дискриминантов;

После успешной явной инициализации завершения отложенной константы, чьим номинальным типом является часть типа T, если завершение находится внутри непосредственной области видимости полного вида T, а отложенная константа видна вне непосредственной области видимости T, проверка выполняется на части(ях) типа T;

После успешного преобразования в тип T проверка выполняется на результате преобразования;

Для преобразования вида, вне непосредственной области видимости T, которое преобразует потомка T (включая сам T) в предка типа T (кроме самого T), проверка выполняется на части объекта, которая является типа T:

после присваивания преобразованию вида; и

после успешного возвращения из вызова, который передаёт преобразование вида как параметр in out или out.

По успешном возвращении из вызова любого вызываемого элемента, являющегося граничным элементом для T, проверка инварианта выполняется для каждого объекта, который подлежит проверке инварианта для T. В случае вызова защищённой операции проверка выполняется до окончания защищённого действия. В случае вызова входа задачи проверка выполняется до окончания взаимодействия. Следующие объекты вызываемого элемента подлежат проверке инварианта для T:

Абзац 16 был объединён выше.

результат с номинальным типом, содержащим часть типа T;

параметр out или in out, чьим номинальным типом является часть типа T;

параметр или результат доступа к объекту, чьим номинальным типом является часть типа T; или

для процедуры или входа, параметр in, чьим номинальным типом является часть типа T.

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

Для преобразования вида к классовому типу, происходящего внутри непосредственной области видимости T, от конкретного типа, являющегося потомком T (включая сам T), выполняется проверка на части объекта, являющейся типа T.

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

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

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

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

ПРИМЕЧАНИЕ Для вызова примитивной подпрограммы типа NT, унаследованной от типа T, выполняются указанные проверки конкретных инвариантов как типов NT, так и T. Для вызова примитивной подпрограммы типа NT, которая переопределена для типа NT, выполняются указанные проверки только конкретных инвариантов типа NT.

Примеры

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

package Work_Orders is

-- См. 3.5.1 для объявлений типов Level, Day и Weekday

END_OF_DOCUMENT_MARKER

тип Work_Order является приватным с
Type_Invariant => Day_Scheduled (Work_Order) в Будний_день
или же Priority (Work_Order) = Срочно;

функция Schedule_Work (Urgency : в Уровень;
To_Occur : в День) возвращает Work_Order
с Pre => Urgency = Срочно или же To_Occur в Будний_день;

функция Day_Scheduled (Order : в Work_Order) возвращает День;

функция Priority (Order : в Work_Order) возвращает Уровень;

процедура Change_Priority (Order : вход/выход Work_Order;
New_Priority : вход Уровень;
Changed : выход Булево)
с Post => Changed = (Day_Scheduled(Order) в Будний_день
или же Priority(Order) = Срочно);

приватный

тип Work_Order является записываемым
Scheduled : День;
Urgency : Уровень;
конец записи;

конец Work_Orders;

основной тело Work_Orders есть

функция Schedule_Work (Urgency : вход Уровень;
To_Occur : вход День) возвращает Work_Order есть
(Scheduled => To_Occur, Urgency => Urgency);

функция Day_Scheduled (Order : вход Work_Order) возвращает День есть
(Order.Scheduled);

функция Priority (Order : вход Work_Order) возвращает Уровень есть
(Order.Urgency);

процедура Change_Priority (Order : вход/выход Work_Order;
New_Priority : вход Уровень;
Changed : выход Булево) есть
начало
-- Убедитесь, что инвариант типа не нарушен
если Order.Urgency = Срочно или же (Order.Scheduled в Будний_день) тогда
Changed := True;
Order.Urgency := New_Priority;
иначе
Changed := False;
конец если;
конец Change_Priority;

конец Work_Orders;