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

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

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

Type_Invariant

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

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, то выражение инвариантности применяется ко всем потомкам T.

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

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

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

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

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

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

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

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

После успешного вызова атрибута потокового типа T Read или Input, проверка выполняется на объекте, инициализированном атрибутом;

Инвариант проверяется после успешного возврата из вызова любого подпрограммы или входа, который:

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

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

и либо:

имеет результат с частью типа T, или

имеет один или несколько параметров out или in out с частью типа T, или

имеет параметр или результат доступа к объекту, тип которого имеет часть типа T, или

является процедурой или входом, имеющим параметр in с частью типа T,

и либо:

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

T является расширением записи, и подпрограмма или вход — это примитивная операция, видимая за пределами непосредственной области видимости типа T, или переопределяет унаследованную операцию, которая видна за пределами непосредственной области видимости 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.

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

ПРИМЕЧАНИЯ

13 При вызове примитивной подпрограммы типа NT, унаследованной от типа T, выполняются указанные проверки конкретных инвариантов как типов NT, так и T. При вызове примитивной подпрограммы типа NT, переопределённой для типа NT, выполняются указанные проверки только конкретных инвариантов типа NT.