Определения функций

1. Преобразование трансляции
   #( ... )
   
2. Имя производного типа
   #derived( $typename )
   Совпадает с именем исходного типа
   [ $typename ]
   
3. Строковое представление сигнатуры метода или конструктора
   #string_representation ( $method_signature )
   Представляет собой строку, получаемую при отбрасывании возможной информации об исключениях и предшествующего ей throws в результате вызова метода toString() в соответствующем данному методу или конструктору reflection-объекте.
   Более точно - то, что получается из результата применения toString() к соответствующему объекту класса java.lang.reflect.Method или java.lang.reflect.Constructor, а затем выполнении над полученной строкой операции substring( 0, indexOf(" throws ") ), если indexOf(" throws ") != -1.
   
4. Полное имя типа
   #full_name( $typename )
   Для базовых типов boolean, char, byte, short, int, long, float, double - в точности имя типа. Для всех остальных - имя типа, дополеннное спереди именами всех содержащих его пакетов, в порядке вложенности, через точку.
   
   1. Короткое имя типа
      Последний идентификатор в полном имени типа.
      #short_name( $typename )
      
   2. Префикс имени типа
      Представляет собой имя типа, от которого отбросили последний идентификатор с точкой, если она есть.
      Т.е., пусто, если имя типа состоит из одного идентификатора, а иначе, квалифицированный идентификатор, из которого полное имя типа получается добавлением в конец точки и #short_name( $typename ).
      #prefix( $typename )
      
   3. Идентификатор, строящийся по полному имени типа (?????)
      #full_identifier ( $typename )
      Совпадает #full_name( $typename ), в котором точки заменены на '_' (?????).
      
      
5. Инициализационное выражение для типа
   #init_expression( $typename )
   [
   ( если $typename = boolean ) ( false )
   ( если $typename = char ) ( '\0' )
   ( если $typename = byte, short, int, long, float, double ) ( 0 )
   ( если $typename - ссылочный, в т.ч. перечислимый ) ( null )
   ]
   
6. Преобразование выражения в строку
   #slashing ( $expression )
   Состоит в замене всех символов " на \".
   
7. Производные спецификационных классов
   При отсутствии явно указанного имени интерфейса для метода вся вставка в скобках ()? опускается.
   
   1. Имя класса модели класса или класса медиатора класса
      #ClassModel
      [ ClassModel ]
      Поскольку этот класс и так вложен в класс, производный от спецификационного, его имя может не зависеть от имени исходного класса.
      
   2. Идентификатор предиката
      #PID( $predicate )
      Это может быть просто номер предиката для данной операции
      Или строковое представление предиката в виде логического выражения
      
   3. Идентификатор элементарной формулы
      #FID( $formula )
      Это может быть её номер для данной операции или её строковое представление в виде логического выражения
      
   4. Имя предусловия спецификационной операции
      #precondition ( $operation_signature )
      [ _ts_precondition_($operation_name) ]
      
   5. Имя анализатора тестовой ситуации для разбиений
      #getPartitionElement ( $operation_signature )
      [ _ts_getPartitionElement_($operation_name) ]
      
   6. Имя анализатора тестовой ситуации для покрытий
      #getCoverageElement ( $operation_signature )
      [ _ts_getCoverageElement_($operation_name) ]
      
   7. Имя вспомогательного метода реализации для спецификационной операции
      #implementation ( $operation_signature )
      [ _ts_implementation_($operation_name) ]
      
   8. Имя оракула спецификационной операции
      #oracle ( $operation_signature )
      [ _ts_oracle_($operation_name) ]
      
   9. Имя медиатора наследования
      #inheritance_mediator ( $operation_signature )
      [ _ts_inheritance_mediator_($operation_name) ]
      
   10. Имя класса события вызова
       #CallEvent ( $method_signature )
       [ _TS_Call_($operation_name)_(номер операции среди операций данного класса и предков, без учета перегрузки (можно - с таким же именем, но не обязательно)) ]
       
   11. Имя внутреннего поля
       #internal_field_name ( $field_identifier )
       [ _ts_field_($field_identifier) ]
       
   12. Имя метода инициализации данных об операции
       #initialize_operation ( $operation_signature )
       [ _ts_init_($operation_name)_(номер операции среди операций данного класса и предков, без учета перегрузки (можно - с таким же именем, но не обязательно)) ]
       
   13. Имя переключателя вызова спецификационной операции
       #switch ( $operation_signature )
       [ _ts_switch_($operation_name) ]
       
   14. Имя метода синхронизации для спецификационной операции
       #update ( $operation_signature )
       [ _ts_update_($operation_name) ]
       
   15. Имя метода, реализующего проверку инварианта
       #generated_invariant_name ( $class_name, $invariant_name )
       [ _ts_($class_name)_($invariant_name) ]
       
8. Производные медиаторных классов
   1. Имя метода создания медиаторов
      #create_mediator ( $type )
      [ _ts_create_( $type_short_name ) ]
      
   2. Имя класса медиатора класса
      См. имя класса модели класса в производных спецификационных классов
      
      Поскольку этот класс и так вложен в класс, производный от медиаторного, его имя может не зависеть от имени исходного класса.
      Кроме того, для того, чтобы удобнее было обрабатывать медиаторные классы, это имя сделано совпадающим с именем класса модели класса.
      
   3. Имя класса-синхронизатора статических полей
      #static_synchronization_manager_name ( $class_name )
      Это "#full_name ( $class_name )", если в нем определен статический метод #mapClassStateDown ( ) или есть static update блок..
      Если в $class_name ни блока, ни метода нет, и есть медиаторный класс-предок $base_name, то #static_synchronization_manager_name ( $class_name ) = #static_synchronization_manager_name ( $base_name ).
      Если в $class_name ни блока, ни метода нет, и есть спецификационный класс-предок $base_name (упомянутый в интерфейсах для медиатора $class_name), то #static_synchronization_manager_name ( $class_name ) = #static_synchronization_manager_name ( $base_name ).
      Если в $class_name ни блока, ни метода нет, и $class_name является спецификационным классом без спецификационных предков, то #static_synchronization_manager_name ( $class_name ) = null.
      
   4. Имя вспомогательного метода вызова предположительно реализационной операции
      #auxiliary_call_method ( $type, $method_signature, ($called_method_exceptions)? )
      Генерировать можно любым, обеспечивающим уникальность имени в пределах данного класса, способом. Напрмер, использовать номера пар (тип, сигнатура) для статических методов, троек (тип, сигнатура, множество типов исключений) для нестатических и номера сигнатур конструкторов для конструкторов.
      
      
9. Производные сценарных классов
   1. Номер сценарного метода $method
      #number ( $method )
      
   2. Число сценарных методов в классе $class_name
      #number ( $class_name )
      
   3. Имя сценарного метода с данным номером $number
      #scenario_method ( $number )
      
   4. Имя класса обощенного воздействия для сценарного метода $method
      #AbstractAction ( $method )
      [ AbstractAction_($method) ]
      
   5. Имя метода вычисления очередного воздействия для сценарного метода $method
      #PartialNext ( $method )
      [ _ts_partialNext_($method) ]
      
   6. Имя метода выполнения очередного воздействия для сценарного метода $method
      #PartialExecute ( $method )
      [ _ts_partialExecute_($method) ]
      
   7. Результирующий идентификатор итерационной переменной или переменной обощенного состояния $variable
      #identifier ( $variable )
      
   8. Идентификатор слеующего значения итерационной переменной
      #next_value ( $variable )
      
   9. Номер итерационной переменной $iteration_variable в рамках сценарного метода
      #number ( $iteration_variable )
      
   10. Номер переменной обобщенного состояния $state_variable в рамках сценарного метода
       #number ( $state_variable )