Список используемых терминов

1. Спецификационный класс
   Класс, декларируемый с помощью SE_SpecificationClassDeclaration
   
2. Медиаторный класс
   Соответствует SE_MediatorClassDeclaration
   
3. Сценарный класс
   Соответствует SE_ScenarioClassDeclaration
   
4. Инвариант
   Соответствует SE_InvariantDeclaration
   
5. Аксиома
   Соответствует SE_AxiomDeclaration
   
6. Эквивалентность
   Соответствует SE_EquivalenceDeclaration
   
7. Спецификационная операция
   Соответсвует SE_OperationSpecification
   
8. Спецификационный метод
   Соответствует SE_MethodSpecification
   
9. Спецификационная реакция
   Соответствует SE_ReactionSpecification
   
10. Предусловие
    Соответствует SE_PreCondition
    
11. Постусловие
    Соответствует SE_PostCondition
    
12. Точка привязки превыражения
    Это место разделения ветвей, содержащих операторы branch, после схождения которых используется данное превыражение.
    Более точно
    1. Если в постусловии, в котором используется превыражение, нет операторов branch, то эта точка - начало постусловия.
    2. Если операторы branch есть, и превыражение достижимо только после одного из них, эта точка непосредственно предшествует этому единственному оператору branch.
    3. Если операторы branch есть, и превыражение достижимо после нескольких из них, находим наименьший блок или инструкцию, включающий/ую все операторы branch, после которых оно достижимо. Эта точка непосредственно предшествует этому блоку или этой инструкции.
       
13. Будем говорить, что к выражению в рамках операции, аксиомы, эквивалентности или функциональной ветви
    определен доступ на только запись, если
    1. Это выражение имеет вид ( PrimaryExpression | QualifiedIdentifier | super | this ) . Identifier и присутствует в таком же виде в ограничениях доступа для операции, аксиомы, эквивалентности или функциональной ветви с модификатором writes.
    2. Это выражение имеет вид ( PrimaryExpression | QualifiedIdentifier | super | this ) . Identifier, и соответствующая конструкция ( PrimaryExpression | QualifiedIdentifier | base ) . ? или ( PrimaryExpression | QualifiedIdentifier | base ) . * присутствует в ограничениях доступа для операции, аксиомы, эквивалентности или функциональной ветви с модификатором writes.
       
14. Медиаторный метод
    Соответствует декларации Se_MediatorMethodDeclaration
    
15. Спецификационные предки медиаторного класса
    Это набор спецификационных классов, который получается транзитивным замыканием по отношениям "реализует" между медиаторными и спецификационными классами, "расширяет" между спецификационными классами и "расширяет" между медиаторными классами.
    Т.е., сначала строится множество медиаторных и спецификационных классов при помощи транзитивного замыкания по этим отношениям, затем из этого множества выбрасываются медиаторные классы. Оставшиеся спецификационные и называются спецификационными предками.
    
16. Реализационное поле
    Соответствует SE_ImplementationFieldDeclaration
    
17. Набор реализационных полей класса
    Является объединением наборов реализационных полей, декларированных в самом классе и всех его предках.
    
18. Реализационный инициализатор
    Соответствует SE_ImplementationInitializer
    
19. Синхронизационный блок
    Соответствует SE_UpdateBlockDeclaration
    
20. Сценарный метод
    Соответствует SE_ScenarioMethodDeclaration
    
21. Блок вычисления обобщенного состояния
    Соответствует SE_ScenarioStateBlock
    
22. Элемент класса - его поле, метод, конструктор, вложенный именованный тип, спецификационный метод, реакция, обратный метод, инвариант, аксиома, эквивалентность, реализационная ссылка, медиаторный метод, сценарный метод.
    
23. Сценарный контекст
    Положение в рамках одной из следующих конструкций
    1. В SE_ScenarioMethodDeclaration
       
24. Переменная обобщенного состояния
    Переменная, декларированная в SE_StateVariableDeclaration.
    
25. Итерационная переменная
    Переменная, декларированная в декларационной части SE_Iterate или SE_CollectionIterate.
    
26. Итерационный блок
    Инструкция вида SE_Iterate, SE_CollectionIterate, SE_CoverageIterate или SE_CoverageCollectionIterate
    
27. Групповая итерация
    Инструкция вида SE_CoverageIterate или SE_CoverageCollectionIterate
    
28. Инструкция фильтрации
    Инструкция вида SE_ExpressionFilterStatement или SE_MethodInvocationFilterStatement
    
29. Жесткая групповая итерация
    Групповая итерация без модификатора casual
    
30. Итерационный блок, входящий в групповую итерацию
    Всякий итерационный блок, который вложен в блок групповой итерации, (включая его самого) и содержит инструкцию фильтрации
    
31. Несущественная инструкция или несущественный блок в SE_PostCondition или SE_PreCondition
    Инструкция одного из следующих видов
    
    1. WhileStatement
    2. DoStatement
    3. ForStatement
    4. TryStatement
    5. SE_IrrelevantStatement
       
32. Обработанная инструкция ThrowStatement
    Инструкция ThrowStatement ::= throw Expression ; называется обработанной, если она находится внутри блока, следующего сразу за оператором try в рамках TryStatement, имеющего CatchClause, подходящую для исключения Expression по правилам Java.
    
33. Мы говорим, что элемент декларирован в $type_name, если текст его декларации находится внутри декларации типа $type_name.
    
34. Если элемент декларирован в классе $class_name или в одном из его предков, мы говорим, что он декларирован в предках $class_name.
    
35. Если элемент декларирован в предках $class_name, но не в самом $class_name, говорим, что он декларирован только в предках $class_name.