JavaTESK Translation Scheme, Specification Class Translation

Трансляция элементов декларации спецификационного класса

SE_SpecificationClassBodyDeclaration может иметь один из следующих видов

FieldDeclaration
Остается как есть.
MethodDeclaration
Остается как есть.
ClassDeclaration
Остается как есть.
EnumDeclaration
Остается как есть.
InterfaceDeclaration
Остается как есть.
AnnnotationTypeDeclaration
Остается как есть.
;
Пропадает.
InstanceInitializer
Остается как есть.
StaticInitializer
static { ( BlockStatement )* }

Остается как есть.

Замечание: благодаря возможности нескольких статических инициализаторов. можно вставить инициализационный код в генерируемый, самый первый из них, а остальные оставить как есть. Иначе, если инициализатор был бы один, надо было бы вставлять код в начало инициализатора.
ConstructorDeclaration
Остается как есть.

Все дальнейшее оставлено на всякий случай - чтобы не удалять, а потом не писать то же самое.

( $modifiers ) ( TypePrameters )? $class_name ( TypeArguments )? FormalParameters ( throws NameList )?
{ ( ExplicitConstructorInvocation )? ( BlockStatement )* }

транслируется в

( $modifiers ) ( TypePrameters )? #derived ( $class_name ) ( TypeArguments )? FormalParameters ( throws NameList )?
{
( ExplicitConstructorInvocation )?
( BlockStatement )*
}
SE_InvariantDeclaration

( static )(10)?
( strictfp )(11)?
( $annotations )(12)?
( prime )(13)?
invariant $invariant_name ( ( $comment )(14)? )
Block

транслируется в

private
(10)?( static )
(11)?( strictfp )
(12)?( $annotations )
void #generated_invariant_name ( $class_name, $invariant_name ) ( )
{
#TestManager #registrar = #TestManager . #getRegistrar ( ) ;
#registrar . #invariantEnter (
(10)?( #derived ( $class_name ) . class . getName ( ) )
(!10)?( this )
, "$invariant_name" , (14)?( $comment ) (!14)?( null ) ) ;

try
{

#( Block ),
где инструкции
return Expression ;
заменены на
if ( ! ( Expression ) ) throw new #InvariantException (
(10)?( #derived ( $class_name ) . class . getName ( ) )
(!10)?( this )
, "$invariant_name" ) ;

Выбрасывать необработанные исключения в теле инварианта запрещено.

}
catch ( #TestException #error )
{
throw #error ;
}
catch ( Throwable #error )
{
throw new #InvariantException (
(10)?( #derived ( $class_name ) . class . getName ( ) )
(!10)?( this )
, "$invariant_name" , #error ) ;
}
finally
{
#registrar . #invariantExit ( ) ;
}
}
SE_OperationSpecification
1. Это может быть SE_MethodSpecification (A) или SE_ReactionSpecification (B)
  
  Для deferred return и deferred throws $exception_type
  модификаторы, кроме unmixable и аннотаций, совпадают с модификаторами объемлющего метода (аннотации могут быть свои)
  типовые параметры - те же
  $method_name =
  = _a_return_($including_method_name)
  = _a_throws_($exception_type)_($including_method_name)
  $result_type = void
  $parameters
  = $including_method_result_type #result
  = $exception_type #exception
  
  ( static )(10)?
  ( strictfp )(11)?
  ( $annotations )(12)?
  ( final )(13)?
  ( synchronized )(14)?
  ( unmixable )(A 15)?
  ( specification )(A) ( reaction )(B)
  ( < $type_parameters > )(16)?
  $result_type $method_name ( $parameters ) ( $dimensions )(17)?
  ( throws $exceptions )(18)?
  ( refines super )(19)?
  ( refines $refined_class_or_blocks )(20)?
  ( reads $read_accesses )(21)? ( writes $write_accesses )? ( updates $update_accesses )?
  {
  ( $initial_block_statements )(22)?
  ( $initial_coverages )(23)?
  ( pre $pre_block )(24)?
  ( $intermediate_coverages )(25)?
  ( post $post_block )(26)?
  ( $last_coverages )(27)?
  ( $deferred_results )(28)?
  ( $inline_reactions )(A 29)?
  ( $last_block_statements )(30)?
  }
  
  Замечание: поскольку $dimensions при анализе исходного кода считаются частью типа возвращаемого значения, тип возвращаемого значения автоматически модифицируется и при трансляции будет доступен в полном виде. Далее везде под $result_type имеется в виду этот полный тип возвращаемого значения.
  
  Семантические ограничения
  - Действуют те же ограничения на допустимые сочетания модификаторов, что и для методов Java.
  - Наследование
    - Среди идентификаторов, указанных после refines может быть только один super. В этом случае данный спецификационный метод называется наследующим поведение.
    - Если нестатический метод наследует поведение, один из предков данного класса должен иметь спецификационный метод с такой же сигнатурой.
  - Перегрузка
    - Если два спецификационных метода, один из которых декларирован в некотором классе, а другой - в его предке (в том числе, в нем самом) имеют одну сигнатуру, то они оба должны быть статическими или нестатическими.
    - Спецификационный метод может перегружать только такие неспецификационные, которые декларированы в интерфейсах.
    - Если метод final, он должен содержать тело
  - Поток управления.
    Блок, помеченный ключевым словом pre, называется предусловием данного спецификационного метода, а блок, помеченный post - его постусловием. Набор инструкций StatementList, предшествующий предусловию, будем называть инициализационным блоком.
    - Внутри инициализационного блока нельзя использовать оператор return и оператор throw, не обрамленный в try-блок, обрабатывающий исключения того типа, который имеет выражение в операторе throw. Операторы throw, обрамленные в такой try-блок, будем называть обработанными.
    - Предусловие и постусловие должны возвращать значение типа boolean.
    - Внутри пред- и постусловия нельзя использовать необработанные операторы throw.
  Далее через $parameters обозначается строка, перечисляющая через запятую все формальные параметры метода вместе с их типами, через $parameter_values - строка, перечисляющая чере запятую только идентификаторы формальных параметров метода. Если у метода нет параметров, обе эти строки пусты.
  Число параметров - $parameters_number, идентификатор i-го параметра (нумерация идет с 0) - $parameter_i, полное имя его типа - $type_i.
  Говорим, что данный спецификационный метод перегружает другой, если в одном из предков данного класса есть спецификационный метод с такой же сигнатурой и совпадающим с данным методом контекстом (т.е., одновременно с ним статический или нестатический).
  
  Для этого элемента генерируется несколько элементов производного класса.
  Аннотации переносятся к интерфейсному методу (и к специальному интерфейсному методу для реакций тоже).
  1. Интерфейсный метод
    public
    (10)?( static )
    (11)?( strictfp )
    (12)?( $annotations )
    (13)? ( final )
    (14)?( synchronized )
    (16)?( < $type_parameters > )
    $result_type $method_name
    (
    (B)?
    (
    #SynchronizationObjectInterface #synch_object
    ( Если $parameters - не пустой )?( , )
    )
    $parameters
    )
    (18)?( throws $exceptions )
    {
    Object[] #args = new Object [ $parameters_number ] ;
    ( Для каждого из параметров метода )
    (
    ( Если параметр $parameter_i - ссылочного типа ) ( #args[ i ] = $parameter_i ; )
    ( Если параметр $parameter_i - примитивного типа ) ( #args [ i ] = #Utils . #toObject ( $parameter_i ) ; )
    )
    
    #ModelEvent #event = new (A)? ( #ModelCall ) (B)?( #ModelReaction ) (
    (10)? ( #class_model ) (!10)? ( this )
    , #specificationOperations . #get ( "#string_representation ( $method_signature )" )
    , #args ) ;
    
    ( B )?
    ( #event . #addSynchronizationObject ( #synch_object ) ; )
    
    #TestManager . #getRegistrar ( ) . #registerModelEvent ( #event ) ;
    
    Throwable #error = #event . #getException ( ) ;
    if ( #error != null )
    {
    ( Для каждого исключения, в порядке, обратном к наследованию )
    ( if ( #error instanceof $exception_i ) throw ( $exception_i ) #error ; )
    ( Если среди $exceptions нет RuntimeException или его предков )
    ( if ( #error instanceof RuntimeException ) throw ( RuntimeException ) #error ; )
    ( Если среди $exceptions нет Error или его предков )
    ( if ( #error instanceof Error ) throw ( Error ) #error ; )
    }
    
    ( Если $resul_type != void и ссылочный )( return ( $result_type ) #event . #getResult ( ) ; )
    ( Если $result_type != void и примитивный ) ( return #Utils . #to($resul_type) ( #event . #getResult ( ) ) ; )
    }
  2. Специальный интерфейсный метод для реакции.
    Генерируется, только если (B).
    Ниже список $parameter_names представляет собой список имён параметров исходного метода, разделённых запятой. Он нужен для передачи значений параметров из специального интерфейсного метода в обычный.
    public
    (10)?( static )
    (11)?( strictfp )
    (12)?( $annotations )
    (13)? ( final )
    (14)?( synchronized )
    (16)?( < $type_parameters > )
    $result_type $method_name
    (
    $parameters
    )
    (18)?( throws $exceptions )
    {
    ( Если $result_type != void )?( return ) $method_name ( null ( Если $parameters не пуст )?( , ) $parameter_names ) ;
    }
  3. ( Генерируется, если !19 или 24 )
    Предусловие спецификационного метода ()
    public
    (10)?( static )
    (11)?( strictfp )
    (16)?( < $type_parameters > )
    boolean #precondition ( $method_signature ) ( $parameters )
    {
    #TestManager #registrar = #TestManager . #getRegistrar( ) ;
    #registrar . #preconditionEnter ( ) ;
    
    try
    {
    ( 19 )?
    (
    boolean #base_pre_result = (10)?( #derived ( $base_name ) ) (!10)?( super ) . #precondition ( $method_signature ) ( $parameter_values ) ;
    if ( #base_pre_result ) return true ;
    )
    Далее в тело предусловия собираются
    - (22)?( $initial_block_statements )
    - (24)? (
      $pre_block , в котором
      - Трансляция SE_MethodInfoParameterized_Expression
        
        (Если данный метод перегружает другой)
        Все вхождения $base . pre заменяются на false
        
        (Если данный метод перегружает другой)
        Выражения $base . pre ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются
        в случае нестатического метода на base . #precondition ( $method_signature ) ( #( $arguments ) )
        в случае статического метода на $base_name . #precondition ( $method_signature ) ( #( $arguments ) )
        
        (Если данный метод перегружает другой)
        $base.branch
        
        (Если данный метод перегружает другой)
        Выражения $base . coverage . $coverage_id заменяются
        в случае нестатического метода на base . #GetPartitionElement ( $operation_signature ) ( "$coverage_id" , $parameter_values )
        в случае статического метода на $base_name . #GetPartitionElement ( $operation_signature ) ( "$coverage_id" , $parameter_values )
        
        (Если данный метод перегружает другой)
        Выражения $base . coverage . $coverage_id ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются
        в случае нестатического метода на base . #GetPartitionElement ( $operation_signature ) ( "$coverage_id", #( $arguments ) )
        в случае статического метода на $base_name . #GetPartitionElement ( $operation_signature ) ( "$coverage_id", #( $arguments ) )
        
        (Если данный метод перегружает другой)
        Выражения $base . coverage ( $argument ), где $argument - выражение, заменяются
        в случае нестатического метода на base . #GetPartitionElement ( $operation_signature ) ( #( $argument ) , $parameter_values )
        в случае статического метода на $base_name . #GetPartitionElement ( $operation_signature ) ( #( $argument ) , $parameter_values )
        
        Выражения $this . pre ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются на #precondition ( $method_signature ) ( #( $arguments ) )
        
        $this.branch
        
        Выражения $this . coverage . $coverage_id ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются на #GetPartitionElement ( $operation_signature ) ( "$coverage_id", #( $arguments ) )
      - Операторы mark, tautology заменяются на ;
      - В SE_IrrelevantStatement отбрасывается модификатор irrelevant
      - SE_AxiomStatement выбрасывается
    - )
    - (! 24)? ( return true ; )
    }
    catch ( #TestException #error ) { throw #error ; }
    catch ( Throwable #error )
    {
    throw new #RuntimeSpecificationMethodException (
    (10)?( #derived ( $class_name ) . class . getName ( ) )
    (!10)?( this )
    , "#string_representation ( $method_signature )"
    , "Exception in precondition"
    , #error ) ;
    }
    finally
    {
    #registrar . #preconditionExit ( ) ;
    }
    }
  4. ( Только если A, т.е. это не реакция )
    Анализатор тестовой ситуации для разбиений
    public
    (10)?( static )
    (11)?( strictfp )
    (16)?( < $type_parameters > )
    int #getPartitionElement ( $operation_signature ) ( String #coverage_id ( Если есть параметры )( , $parameters ) )
    {
    Далее используется нумерация элементов стандартных покрытий. Элементы каждого покрытия нумеруются, начиная с 0, по порядку строк в таблице соответствий. В приводимой выше таблице, например, 20 дизъюнктов, di соответствует номер (i-1), 12 последовательностей предикатов, (P2;P7;P8;P10) имеет номер 5, 10 последовательностей отметок, (1;3;B4) имеет номер 6, и 4 ветви, Bi соответствует номер (i-1).
    
    #TestManager #registrar = #TestManager . #getRegistrar( ) ;
    #registrar . #coverageAnalysisPreconditionEnter ( ) ;
    
    #DisjunctAnalyser #analyser = new #DisjunctAnalyser ( #specificationOperations . #get ( "#string_representation ( $method_signature )" ) ) ;
    
    ( 19 )?
    (
    boolean #base_pre_result = (10)?( #derived ( $base_name ) ) (!10)?( super ) . #precondition ( $method_signature ) ( $parameter_values ) ;
    )
    
    try
    {
    Далее в тело собираются
    - try
      {
    - (22)?( $initial_block_statements )
    - (24)? (
      $pre_block , в котором
      - Трансляция SE_MethodInfoParameterized_Expression
        
        (Если данный метод перегружает другой)
        Все вхождения $base . pre заменяются на #base_pre_result
        
        (Если данный метод перегружает другой)
        Выражения $base . pre ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются
        в случае нестатического метода на base . #precondition ( $method_signature ) ( #( $arguments ) )
        в случае статического метода на $base_name . #precondition ( $method_signature ) ( #( $arguments ) )
        
        (Если данный метод перегружает другой)
        $base.branch
        
        (Если данный метод перегружает другой)
        Выражения $base . coverage . $coverage_id заменяются
        в случае нестатического метода на base . #getPartitionElement ( $operation_signature ) ( "$coverage_id" , $parameter_values )
        в случае статического метода на $base_name . #getPartitionElement ( $operation_signature ) ( "$coverage_id" , $parameter_values )
        
        (Если данный метод перегружает другой)
        Выражения $base . coverage . $coverage_id ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются
        в случае нестатического метода на base . #getPartitionElement ( $operation_signature ) ( "$coverage_id", #( $arguments ) )
        в случае статического метода на $base_name . #getPartitionElement ( $operation_signature ) ( "$coverage_id", #( $arguments ) )
        
        (Если данный метод перегружает другой)
        Выражения $base . coverage ( $argument ), где $argument - выражение, заменяются
        в случае нестатического метода на base . #getPartitionElement ( $operation_signature ) ( #( $argument ) , $parameter_values )
        в случае статического метода на $base_name . #getPartitionElement ( $operation_signature ) ( #( $argument ) , $parameter_values )
        
        Выражения $this . pre заменяются на #precondition ( $method_signature ) ( $parameter_values )
        
        Выражения $this . pre ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются на #precondition ( $method_signature ) ( #( $arguments ) )
        
        $this.branch
        
        Выражения $this . coverage . $coverage_id ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются на #getPartitionElement ( $operation_signature ) ( "$coverage_id", #( $arguments ) )
      - Все элементарные формулы в условиях существенных ветвлений и операторах return преобразуются в канонический вид, после чего все вхождения элементарной формулы $formula с идентификатором #FID( $formula ) заменяются на #analyser . #recordFormulaValue ( #FID( $formula ) , $formula )
      - Существенные блоки switch ( Expression ) { ... } преобразуются следующим образом
        Если тип Expression $expression_type, перед блоком switch вставляем следующие инструкции
        $expression_type #tmp_var = #(Expression) ; ( имя #tmp_var уникально в рамках данного метода )
        для всех костант $value_i, используемых как часть меток ветвей, вставляем
        #analyser . #recordFormulaValue ( #FID( "Expression == $value_i" ) , ( #tmp_var ) == ( $value_i ) ) ;
        Выражение Expression в операторе switch заменяем на #tmp_var
      - Операторы mark, tautology заменяются на ;
      - В SE_IrrelevantStatement отбрасывается модификатор irrelevant (ветвления внутри этой инструкции не являются существенными, поэтому элементарные формулы в них не отслеживаются)
      - Операторы return Expression ; заменяются на
        if ( ! ( Expression ) ) return -1;
      }
      catch ( #TestException #error ) { throw #error ; }
      catch ( Throwable #error )
      {
      throw new #RuntimeSpecificationMethodException (
      (10)?( #derived ( $class_name ) . class . getName ( ) )
      (!10)?( this )
      , "#string_representation ( $method_signature )"
      , "Exception in precondition"
      , #error ) ;
      }
      finally
      {
      #registrar . #coverageAnalysisPreconditionExit ( ) ;
      }
    - (26 & В постусловии есть хотя бы один оператор branch )?
      (
      try
      {
      $post_block, в котором производятся те же преобразования, что и для предусловия, плюс
      - Оператор branch заменяется на следующий набор инструкций
        return #analyser . #getPartitionElementIndex ( #coverage_id ) ;
      - Все инструкции, которые не могут быть достигнуты без прохода через оператор branch, должны быть отброшены.
        Примерный алгоритм отбрасывания такой:
        Объявляем текущим самый внутренний блок, содержащий branch. Инструкцию branch в нем объявляем помеченной.
        Если помеченная инструкция не является IfStatement или SwitchStatement, отбрасываем все инструкции текущего блока, идущие после нее.
        Если помеченная инструкция является IfStatement или SwitchStatement, в котором все возможные ветви проходят через branch (т.е. IfStatement с else или SwitchStatement, у которых во всех SwitchBlockStatementGroup, с учетом возможного перехода из них в следующие, есть branch), отбрасываем все инструкции текущего блока, идущие после нее.
        Если помеченная инструкция является IfStatement или SwitchStatement, в rоторой хотя бы одна ветвь не содержит branch (например, это IfStatement без else), просто идем дальше.
        После этого, если текущим блоком является Block постусловия, прекращаем работу, иначе объявляем помеченной инструкцией текущий блок, а текущим - самый внутренний блок, содержащий её.
      }
      catch ( #TestException #error ) { throw #error ; }
      catch ( Throwable #error )
      {
      throw new #RuntimeSpecificationMethodException (
      (10)?( #derived ( $class_name ) . class . getName ( ) )
      (!10)?( this )
      , "#string_representation ( $method_signature )"
      , "Exception in postcondition"
      , #error ) ;
      }
      )
      (!26 | Ни одного оператора branch в постусловии нет )?
      ( return 0 ; )
    }
    finally
    {
    #registrar . #coverageAnalysisPostconditionExit ( ) ;
    }
    }
  5. Оракул спецификационного метода.
    Генерируется и для стимулов, и для реакций
    protected
    (10)?( static )
    (11)?( strictfp )
    (16)?( < $type_parameters > )
    boolean #oracle ( $method_signature ) ( int #level ( Если есть параметры )( , $parameters ) )
    {
    ( 19 )
    (
    if ( #level < #class_level )
    return (10)?( #derived ( $base_name ) ) (!10)?( super ) . #oracle ( $method_signature ) ( #level - 1, $parameters_values ) ;
    else if ( #level > #class_level ) #level = #class_level ;
    )
    
    #TestManager #registrar = #TestManager . #getRegistrar ( ) ;
    #registrar . #oraclePreconditionEnter ( "#full_name ( $class_name )" ) ;
    
    ( 19 )
    (
    boolean #base_pre_result = (10)?( #derived ( $base_name ) ) (!10)?( super ) . #precondition ( $method_signature ) ( $parameter_values ) ;
    boolean #base_verdict = true ;
    )
    boolean #pre_result = true ;
    boolean #verdict = true ;
    - try
      {
      - Ограничения доступа
        
        Для всякого ограничения доступа, указанного в методе, выделяется объект доступа, класс доступа и поле(я) доступа (поле доступа не обязательно является полем в каком-то объекте, объект доступа должен быть определён тогда и только тогда, когда не определён класс доступа).
        Смысл этих понятий следующий:
        (i). Если ограничение доступа указано на ( Primary | ( ClassName . )? super ) "." ( Identifier | ? | * ), то
        Объектом доступа является значение выражения, стоящего до точки, если это выражение имеет значение ссылки на какой-то объект, иначе объект доступа не определён;
        Классом доступа является имя класса, стоящее до точки, если это имя класса, иначе класс доступа не определён;
        Полем доступа являяется, соответственно, Identifier, если же указаны ? или *, поле доступа не определено.
        (ii). Если ограничение доступа указано на ( Identifier | ? | * ), то
        Если указан Identifier, являющийся именем параметра метода, то ни объект, ни класс доступа не определены (случай ((ii)-a));
        Если указан Identifier, являющийся именем не static поля, или указан ? | *, то объектом доступа является this;
        Если указан Identifier, являющийся именем static поля, или указан ? | *, то классом доступа является класс this;
        Полем доступа здесь является Identifier или, при указании ? или *, оно не определено.
        (iii). Если ограничение доступа указано на ArrayAccess (::= ( ExpressionName | PrimaryNoNewArray ) [ Expression_1 ]...[ Expression_t] ), то
        Объектом доступа является объект-массив, ссылка на который является значением выражения ( ExpressionName | PrimaryNoNewArray );
        Класс доступа не определён;
        Полями доступа здесь являются значения выражений Expression_i в квадратных скобках.
        Цель выделения этих элементов - при проверке ограничений "только чтение" мы должны сохранить ссылку на объект доступа и указание на поле доступа (если это действительно поле, в смысле Java, надо только запомнить его имя, если это целое значение, надо запомнить его, и т.д.), а также пре-значение этого поля, а затем, после вызова целевого метода, получить значение, укызываемого полем доступа по запомненной ссылке на объект доступа и сравнить его с пре-значением.
        
        Для всякого reads-доступа делается следующее
        (Если определён объект доступа)
        Объявляется локальная переменная #rco_tmp_object_i того же типа, что и объект доступа, далее обозначаемого как $access_object_class, или типа #derived ( $access_object_class ), если $access_object_class - спецификационный. Инициализируется ссылкой на объект доступа.
        (Если определён класс доступа $access_class_name и он спецификационный или наследует #ModelObject)
        Объявляется локальная переменная #rco_tmp_class_i, имеющая тип #ModelClass. Инициализируется null.
        (В случае (iii))
        Для каждого поля доступа объявляется локальная переменная #rco_tmp_index_i_j типа int, инициализируемая соответствующим выражением Expression_j.
        (Если указание доступа оканчивается не на ? или *)
        В случае ((ii)-a) ничего не делается.
        Объявляется локальная переменная #rco_tmp_i, имеющая тот же тип, что и значение, находящееся в поле доступа. В случае (iii) это тип элемента массива. Инициализируется null, в том случае, если тип значения - класс, true - если это boolean, 0 - если это byte, char, short, int, long, float, double.
        (Если указание доступа оканчивается на ? или * и определён объект доступа)
        Если тип объекта доступа - спецификационный (объявлен в спецификационном пакете) или наследует #ModelObject, объявляется локальная переменная #rco_tmp_object_value_i, имеющая тип #ModelObject. Инициализируется null.
        
        Далее, добавляется следущий блок.
        if(
        (Если метод нестатический) (#read_only_checking_flag )
        (Если метод статический) ( #class_read_only_checking_flag )
        )
        {
        (Случай (i) или (ii), указание доступа оканчивается не на ? или *, определён объект доступа)
        #rco_tmp_i = #rco_tmp_object_i.Identifier;
        (Случай (iii))
        #rco_tmp_i = #rco_tmp_object_i [ #rco_tmp_index_i_1 ] ... [ #rco_tmp_index_i_t];
        (Cлучай (i) или (ii), указание доступа оканчивается не на ? или *, определён класс доступа)
        #rco_tmp_i = $access_class_name.Identifier;
        (Случай (i) или (ii), указание доступа оканчивается на ? или *, определён объект доступа и он - спецификационного типа или наследующего #ModelObject)
        #rco_tmp_object_value_i = ( #ModelObject ) #rco_tmp_object_i.#shallowClone ( );
        (Cлучай (i) или (ii), указание доступа оканчивается на ? или *, определён класс доступа - спецификационный или наследник #ModelObject )
        #rco_tmp_class_i =
        (Если он спецификационный) #object_model_name($access_class_name). #get_jatva_class_copy ( );
        (Если он просто наследует #ModelObject ) $access_class_name. #get_jatva_class_copy ( );
        }
      - try
        {
        #pre_label :
        {
      - (22)?( $initial_block_statements )
      - (24)? (
        $pre_block , в котором
        
        Трансляция SE_MethodInfoParameterized_Expression
        
        (Если данный метод перегружает другой)
        Все вхождения $base . pre заменяются на #base_pre_result
        
        (Если данный метод перегружает другой)
        Выражения $base . pre ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются
        в случае нестатического метода на base . #precondition ( $method_signature ) ( #( $arguments ) )
        в случае статического метода на $base_name . #precondition ( $method_signature ) ( #( $arguments ) )
        
        (Если данный метод перегружает другой)
        $base.branch
        
        (Если данный метод перегружает другой)
        Выражения $base . coverage . $coverage_id заменяются
        в случае нестатического метода на base . #getPartitionElement ( $operation_signature ) ( "$coverage_id" , $parameter_values )
        в случае статического метода на $base_name . #getPartitionElement ( $operation_signature ) ( "$coverage_id" , $parameter_values )
        
        (Если данный метод перегружает другой)
        Выражения $base . coverage . $coverage_id ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются
        в случае нестатического метода на base . #getPartitionElement ( $operation_signature ) ( "$coverage_id", #( $arguments ) )
        в случае статического метода на $base_name . #getPartitionElement ( $operation_signature ) ( "$coverage_id", #( $arguments ) )
        
        (Если данный метод перегружает другой)
        Выражения $base . coverage ( $argument ), где $argument - выражение, заменяются
        в случае нестатического метода на base . #getPartitionElement ( $operation_signature ) ( #( $argument ) , $parameter_values )
        в случае статического метода на $base_name . #getPartitionElement ( $operation_signature ) ( #( $argument ) , $parameter_values )
        
        Выражения $this . pre заменяются на #precondition ( $method_signature ) ( $parameter_values )
        
        Выражения $this . pre ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются на #precondition ( $method_signature ) ( #( $arguments ) )
        
        $this.branch
        
        Выражения $this . coverage . $coverage_id заменяются на #getPartitionElement ( $operation_signature ) ( "$coverage_id" , $parameter_values )
        
        Выражения $this . coverage . $coverage_id ( $arguments ), где $arguments - список выражений, возможно пустой, заменяются на #getPartitionElement ( $operation_signature ) ( "$coverage_id", #( $arguments ) )
        
        Выражения $this . coverage ( $argument ), где $argument - выражение, заменяются на #getPartitionElement ( $operation_signature ) ( #( $argument ) , $parameter_values )
        
        Все элементарные формулы в условиях существенных ветвлений и операторах return преобразуются в канонический вид, после чего все вхождения элементарной формулы $formula с идентификатором #FID( $formula ) заменяются на #registrar . #formulaValue ( #FID( $formula ) , #( $formula ) )
        
        Существенные блоки switch ( Expression ) { ... } преобразуются следующим образом
        Если тип Expression $expression_type, перед блоком switch вставляем следующие инструкции
        $expression_type #tmp_var = #(Expression) ; ( имя #tmp_var уникально в рамках данного метода )
        для всех костант $value_i, используемых как часть меток ветвей, вставляем
        #registrar . #formulaValue ( #FID( $Expression == $value_i ) , ( #tmp_var ) == ( $value_i ) ) ;
        Выражение Expression в операторе switch заменяем на #tmp_var
        
        Операторы mark ( Identifier )(31)? <StringLiteral> ; заменяются на
        #registrar . #markExecution ( (31)?( "Identifier" )(!31)?( null ) , <StringLiteral> ) ;
        
        Следующие конструкции разрешены только в пост-блоках стимулов, поэтому при трансляции реакций они встречаться не должны
        
        Операторы tautology заменяются на ;
        
        В SE_IrrelevantStatement отбрасывается модификатор irrelevant
        Ветвления внутри этой инструкции не являются существенными, поэтому элементарные формулы в них не отслеживаются.
        
        Операторы return Expression ; заменяются на блок
        { #pre_result = #(Expression) ; break #pre_label ; }
        
        }
        
        if ( ! #pre_result )
        {
        #registrar . #registerOracleException ( new #PreconditionViolationException (
        (10)?( #derived ( $class_name ) . class . getName ( ) )
        (!10)?( this )
        , "#string_representation ( $method_signature )") ) ;
        
        ( !(19) )
        ( if ( ! (10)?( #class_model . ) #isAnyPreconditionHolds ( ) ) return false ; )
        }
        ( 19 )
        ( else (10)?( #class_model . ) #setAnyPreconditionHolds ( ) ; )
        
        }
        catch ( #TestException #error ) { throw #error ; }
        catch ( Throwable #error )
        {
        throw new #RuntimeSpecificationMethodException (
        (10)?( #derived ( $class_name ) . class . getName ( ) )
        (!10)?( this )
        , "#string_representation ( $method_signature )"
        , "Exception in precondition"
        , #error ) ;
        }
        finally
        {
        #registrar . #oraclePreconditionExit ( ) ;
        }
      - (!26, т.е. постусловия нет)
        (
        #registrar . #oraclePostconditionEnter ( "#full_name ( $class_name )" ) ;
        #registrar . #branchExecution ( "Single", null ) ;
        
        ( !19)
        (
        #switch ( $method_signature ) ( $parameter_values ) ;
        return #pre_result ;
        )
        ( 19 )
        (
        #base_verdict = (10)?( #derived ( $base_name ) ) (!10)?( super ) . #oracle ( $method_signature ) ( #level - 1, $parameters_values ) ;
        return #pre_result && #base_verdict ;
        )
        )
      - (26, т.е. если постусловие есть)
        Код постусловия
        (
        if ( #pre_result
        ( 19 )( && (10)?( #class_model . ) #isAnyPreconditionHolds ( ) )
        )
        {
        Throwable #thrown = null ;
        ( $result_type != void ) ($result_type #result = #init_expression( $result_type ) ;)
        
        try
        {
        
        #post_label :
        {
        #registrar . #oraclePostconditionEnter ( "#full_name ( $class_name )" ) ;
        
        (Если нет ни одного оператора branch)
        (
        ( Для каждого пре-выражения $pre_expression_i объявляется переменная #pre_variable_i того же типа $pre_expression_type_i, что и пре-выражение, и инициализируется текущим значением пре-выражения, если в $pre_expresson входят элементарные формулы, то они обрабатываются, как обычно )
        ( #pre_variable_i = #( $pre_expression_i ) ; )
        
        #registrar . #branchExecution ( "Single", null ) ;
        
        ( !(19) ) ( #switch ( $method_signature ) ( $parameter_values ) ; )
        ( 19)
        ( #base_verdict = (10)?( #derived ( $base_name ) ) (!10)?( super ) . #oracle ( $method_signature ) ( #level - 1, $parameters_values ) ; )
        
        ( $result_type != void & $result_type - примитивный)
        ( #result = #Utils . #to($result_type) ( #registrar . #getCurrentEvent ( ) . #getResult ( ) ) ; )
        ( $result_type != void & $result_type - ссылочный)
        ( #result = ( $result_type ) ( #registrar . #getCurrentEvent ( ) . #getResult ( ) ) ; )
        #thrown = #registrar . #getCurrentEvent ( ) . #getException ( ) ;
        )
        
        $post_block, в котором производятся те же преобразования, что и для предусловия, кроме преобразований операторов return, плюс следующие
        
        Для каждого пре-выражения $pre_expression_i непосредственно перед точкой, где разделяются ветви, после слияния которых оно используется (точка привязки превыражения), объявляется переменная #pre_variable_i того же типа $pre_expression_type_i, что и пре-выражение, и инициализируется значением типа по умолчанию.
        $pre_expression_type_i #pre_variable_i = #init_expression( $pre_expression_type_i ) ;
        
        Каждый оператор
        ( deferred )(31)? branch Identifier ( ( Expression ) )(32)? ( $accesses )(33)? ( $refines )(34)? ;
        заменяется на следующую группу
        
        Обработка ограничений доступа
        
        ( Для каждого пре-выражения $pre_expression_i, используемого после данного оператора branch, соответсвующая переменная инициализируется текущим значением пре-выражения, если в $pre_expresson входят элементарные формулы, то они трассируются, как обычно )
        ( #pre_variable_i = #( $pre_expression_i ) ; )
        
        #registrar . #branchExecution ( "Identifier", (31)?( #(Expression) ) (!31)?( null ) ) ;
        
        ( Если branch не deferred, но в постусловии есть другой deferred branch )
        ( #registrar . #markImmediateResult ( ) ; )
        
        ( !19) ( #switch ( $method_signature ) ( $parameter_values ) ; )
        
        ( 19)
        ( #base_verdict = (10)?( #derived ( $base_name ) ) (!10)?( super ) . #oracle ( $method_signature ) ( #level - 1, $parameters_values ) ; )
        
        ( $result_type != void & $result_type - примитивный)
        ( #result = #Utils . #to($result_type) ( #registrar . #getCurrentEvent ( ) . #getResult ( ) ) ; )
        ( $result_type != void & $result_type - ссылочный)
        ( #result = ( $result_type ) ( #registrar . #getCurrentEvent ( ) . #getResult ( ) ) ; )
        #thrown = #registrar . #getCurrentEvent ( ) . #getException ( ) ;
        
        Использование пре-выражения pre $pre_expression_i заменяется на использование соответствующей переменной #pre_variable_i
        
        Если ( $result_type != void ), то использование имени метода и @this . result заменяется на использование #result.
        Использование thrown и @this . exception заменяется на использование #thrown.
        В стальных случаях использование выражения @this заменяется на использование #registrar . #getCurrentEvent ( ).
        
        У update блоков (SE_UpdateStatement) убирается модификатор update
        
        Каждый оператор return Expression ; заменяется на
        #verdict = #(Expression) ; break #post_label ;
        
        }
        
        Далее вставляется блок проверки ограничений доступа
        
        (Случай (i) или (ii), указание доступа оканчивается не на ? или *, определён объект доступа)
        #verdict = #verdict && #TS_Tracer.#trace_prime_formula ( #rco_tmp_i == #rco_tmp_object_i.Identifier, #FID( reads ... ) );
        (Случай (iii))
        #verdict = #verdict && #TS_Tracer.#trace_prime_formula ( #rco_tmp_i == #rco_tmp_object_i [ #rco_tmp_index_i_1 ] ... [ #rco_tmp_index_i_t ], #FID( reads ... ) );
        (Cлучай (i) или (ii), указание доступа оканчивается не на ? или *, определён класс доступа)
        #verdict = #verdict && #TS_Tracer.#trace_prime_formula ( #rco_tmp_i == $access_class_name.Identifier, #FID( reads ... ) );
        (Случай (i) или (ii), указание доступа оканчивается на ? или *, определён объект доступа спецификационного типа или типа-наследника #TS_ModelObject)
        #verdict = #verdict && #TS_Tracer.#trace_prime_formula ( #rco_tmp_object_value_i.#technical_equals ( #rco_tmp_object_i ), #FID( reads... ) );
        (Cлучай (i) или (ii), указание доступа оканчивается на ? или *, определён класс доступа, спецификационный или наследник #TS_ModelObject)
        #verdict = #verdict && #TS_Tracer.#trace_prime_formula ( #rco_tmp_class_i.#technical_equals (
        (Если он спецификационный) #object_model_name($access_class_name). #get_jatva_class_copy ( )
        (Если он просто наследует #TS_ModelObject ) $access_class_name. #get_jatva_class_copy ( )
        ), #FID( reads ... ) );
        
        if( !#verdict )
        {
        #registrar . #registerOracleException ( new #PostconditionViolationException (
        (10)?( #derived ( $class_name ) . class . getName ( ) )
        (!10)?( this )
        , "#string_representation ( $method_signature )") ) ;
        
        ( 19 )
        ( return #base_verdict ; )
        ( !19 )
        ( return false ; )
        }
        return true ;
        
        }
        catch( #TestException #error )
        {
        throw #error ;
        }
        catch( Throwable #error )
        {
        throw new #RuntimeSpecificationMethodException (
        (10)?( #derived ( $class_name ) . class . getName ( ) )
        (!10)?( this )
        , "#string_representation ( $method_signature )"
        , "Exception in postcondition"
        , #error ) ;
        }
        
        }
        else
        {
        ( !19 )
        (
        #switch ( $method_signature ) ( $parameter_values ) ;
        return false ;
        )
        ( 19 )
        (
        return (10)?( #derived ( $base_name ) ) (!10)?( super ) . #oracle ( $method_signature ) ( #level - 1, $parameters_values ) ;
        )
        }
    - Общее окаймление оракула
      }
      finally
      {
      #registrar . #oraclePostconditionExit ( ) ;
      }
    }
  6. ( Генерируется, только если метод не перегружает другой )
    Переключатель вызова спецификационного метода
    protected
    (10)?( static )
    (16)?( < $type_parameters > )
    void #switch ( $method_signature ) ( $parameters )
    {
    #TestManager #registrar = #TestManager . #getRegistrar ( ) ;
    
    if ( #registrar . #isExecuting ( ) )
    {
    try
    {
    #registrar . #implementationStart ( ) ;
    
    ( $result_type != void & $result_type - примитивный )
    ( #registrar . #storeResult ( #Utils . #toObject ( )
    ( $result_type != void & $result_type - ссылочный )
    ( #registrar . #storeResult ( )
    (10)?( #class_model . ) #implementation ( $method_signature ) ( $parameters_values )
    ( $result_type != void ) ( ) ) ;
    
    #registrar . #implementationExit ( ) ;
    }
    catch( #TestException #error )
    {
    if ( ! #error . #isCritical ( ) )
    {
    #registrar . #implementationExit ( ) ;
    }
    throw #error ;
    }
    catch( Throwable #error )
    {
    #registrar . #storeException ( #error ) ;
    #registrar . #implementationExit ( ) ;
    }
    }
    else
    {
    #registrar . #implementationStart ( ) ;
    #registrar . #implementationExit ( ) ;
    }
    }
  7. Реализация спецификационного метода
    protected
    (10)?( static )
    (11)?( strictfp )
    (14)?( synchronized )
    (16)?( < $type_parameters > )
    $result_type #implementation ( $method_signature ) ( $parameters )
    (18)?( throws $exceptions )
    {
    - Если !(30) и A, то тело этого метода содержит только одну инструкцию
      
      throw new #ImplicitMethodCallException (
      (10)?( #derived ( $class_name ) . class . getName ( ) )
      (!10)?( this ) $full_name($class_name)
      , "#string_representation ( $method_signature )" ) ) ;
    - Иначе, в тело этого метода собираются
      - ( Если метод - не статический )
        ( #Tracer . #TracerObject . #TraceImplementationObject ( this ) ; )
        ( Если метод - статический )
        ( #Tracer . #TracerObject . #TraceImplementationClass ( "$full_name ( $class_name )" ) ; )
        
        #Tracer . #TracerObject . #TraceImplementationOperationStart ( "#string_representation ( $method_signature )" ) ;
      - ( Для всех параметров в порядке их следования в сигнатуре )
        (
        ( Если тип $type_i параметра $parameter_i является ссылочным и параметр - не out и не params )
        ( #Tracer . #TracerObject . #TraceImplementationValue ("argument( Если $parameter_i_modifier - ref )( ref)", ( $parameter_i == null )? "$full_name($type_i)":$parameter_i.GetType().FullName, "$parameter_i", "" + $parameter_i ) ; )
        ( Если тип $type_i параметра $parameter_i является типом значения и параметр - не out и не params )
        ( #Tracer . #TracerObject . #TraceImplementationValue ("argument( Если $parameter_i_modifier - ref )( ref)", "$full_name($type_i)", "$parameter_i", "" + $parameter_i ) ; )
        ( Если параметр - out )
        ( #Tracer . #TracerObject . #TraceImplementationValue ( "argument out", "$full_name( $type_i )", "$parameter_i", "" ) ; )
        ( Если параметр - params )
        (
        if ( $parameter_i . Length == 0 )
        #Tracer . #TracerObject . #TraceImplementationValue ( "argument params", "$full_name( $type_i )", "$parameter_i", "" ) ;
        else
        for ( int #j = 0 ; #j < $parameter_i . Length ; #j ++ )
        ( Если тип элементов массива $base_type_i является ссылочным )
        ( #Tracer . #TracerObject . #TraceImplementationValue ( "argument params",
        ( $parameter_i[#j] == null )? "$full_name($base_type_i)":$parameter_i[#j].GetType().FullName, "$parameter_i[" + #j + "]", "" + $parameter_i[#j] ) ; )
        ( Если тип элементов массива $base_type_i является типом значения )
        ( #Tracer . #TracerObject . #TraceImplementationValue ( "argument params", "$full_name( $base_type_i )", "$parameter_i_name[" + #j + "]", "" + $parameter_i_name[#j] ) ; )
        )
        )
        
        (Для каждого out-параметра $par_i типа $type_i)
        ( $par_i = #init_expression( $type_i ) ; )
      - long #startTime = -1, #endTime = -1 ;
        ( $result_type != void ) ( $result_type #result = #init_expression( $result_type ) ; )
      - try
        {
        #startTime = System.DateTime.Now.Ticks ;
      - (9)? (
        StatementList,
        из которых выброшены операторы tautology
        )
      - (12)? (
        StatementList,
        преобразованный следующим образом
      - операторы tautology и coverage заменяются на ;
      - ( $result_type != void )
        (
        оператор return Expression ; заменяется на
        #result = Expression ;
        
        ( $result_type - ссылочный тип )
        ( #Tracer . #TracerObject . #TraceImplementationValue ( "result", ( #result == null )? "$full_name($result_type)":#tmp_res.GetType().FullName, "", "" + #result ) ; )
        ( $result_type - тип значения )
        ( #Tracer . #TracerObject . #TraceImplementationValue ( "result", "$full_name($result_type)", "", "" + #result ) ; )
        
        return #result ;
        )
        )
      - }
        catch ( System.Exception #error )
        {
        #Tracer . #TracerObject . #TraceImplementationValue ( "exception", #error.GetType().FullName, "", "" + #error ) ;
        throw #error ;
        }
        finally
        {
        #endTime = System.DateTime.Now.Ticks ;
        
        ( Для всех ref и out параметров в порядке их следования в сигнатуре )
        (
        ( Если тип $parameter_i_type является ссылочным )
        ( #Tracer . #TracerObject . #TraceImplementationValue ( "argument( Если $parameter_i_modifier - ref )( ref)( Иначе) ( out)", ( $parameter_i_name == null )? "$full_name($type_i)":$parameter_i_name.GetType().FullName, "$parameter_i_name", "" + $parameter_i_name ) ; )
        ( Если тип $parameter_i_type является типом значения )
        ( #Tracer . #TracerObject . #TraceImplementationValue ("argument( Если $parameter_i_modifier - ref )( ref)( Иначе) ( out)","$full_name($type_i)", "$parameter_i_name", "" + #tmp_par_i ) ; )
        )
        
        #Tracer . #TracerObject . #TraceImplementationTimeInterval ( #startTime, #endTime ) ;
        #Tracer . #TracerObject . #TraceImplementationOperationEnd ( ) ;
        #SynchronizationManager . #Update ( ) ;
        }
    - Если B
    }
  8. Метод инициализации данных об операции
    Алгоритм вычисления структуры предопределенных покрытий, а также определения используемых при работе с покрытиями понятий, описаны здесь.
    
    private static void #initialize_operation ( $operation_signature ) ( )
    {
    #OperationInfo #current = new #OperationInfo ( #derived ( $class_name ) . class
    , "#string_representation ( $method_signature )"
    , new String[] {
    ( Для каждого параметра метода )
    (
    ( i != 0) ( , )
    "parameter_i"
    )
    }
    ) ;
    
    #specificationOperations . #put ( "#string_representation ( $method_signature )" , #current ) ;
    
    ( Для каждой вычисленной элементарной формулы, строковое представление которой $formula , и которой был присвоен числовой идентификатор #FID( $formula ) )
    ( #current . #addFormula ( #FID( $formula ) , "#slashing( $formula )" ) ; )
    
    ( Если A & 26 & в постуловии есть операторы branch )
    (
    ( Для каждой ветви функциональности, соответствующей оператору
    branch $branch_identifier ( ( "$branch_description" ) )? ( SE_AccessDescriptions )? ;
    и которой в ходе обсчета структуры покрытий был присвоен числовой идентификатор $id )
    ( #current . #addBranch ( $id , "$branch_identifier" ) ; )
    
    ( Если трансляции идет без опции -nodisjuncts, для каждой вычисленной последовательности марок, строковые литералы которых равны $mark_1, ... , $mark_k, $branch_identifier, и которой в ходе обсчета структуры покрытий был присвоен числовой идентификатор $id )
    ( #current . #addMarkedPath ( $id , "$mark_1; " + ... + "$mark_k; " + "$branch_identifier" ) ; )
    
    ( Если трансляции идет без опции -nodisjuncts, для каждого вычисленного полного предиката, строковое представление которого $full_predicate, и которому в ходе обсчета структуры покрытий был присвоен числовой идентификатор $id )
    ( #current . #addPredicate ( $id , "$full_predicate" ) ; )
    
    ( Если трансляции идет без опции -nodisjuncts, для каждого вычисленного дизъюнкта, которому в ходе обсчета структуры покрытий был присвоен числовой идентификатор $id, и который соответсвует ветви $branch_id, маркированному пути $marked_path_id и полному предикату $full_predicate_id. Далее, создается строка $values из символов '+', '-' и '*' на местах, соответствующих используемым формулам, имеющим значение true, false и несущественным
    Для дизъюнкта true, соответсвующего едиснтвенному возможному ходу вычислений, в качестве $values используется пустая строка)
    ( #current . #addDisjunct ( $id , new #DisjunctInfo ( $branch_id , $marked_path_id , $full_predicate_id , $values ) ) ; )
    )
    
    ( Если A & !26 или A & 26 & в постусловии нет операторов branch )
    ( #current . #addBranch ( 0 , "Single" ) ; )
    
    }