Трансляция выражений

В этом разделе представлены правила трансляции выражений JavaTESK для каждой их разновидности.

  1. Выражения Java
    По правилу [*] эти выражения преобразуются без изменений, за исключением преобразования кода деклараций JavaTESK.
  2. Выражения JavaTESK
    Специфическими выражениями JavaTESK являются
    1. SE_MediatorCreationExpression
      Это выражение предназначено для создания медиаторных объектов по набору их реализационных ссылок. Необходимость в особом выражении возникает, поскольку при этом может быть создан новый объект, а может быть найден уже имеющийся в системе объект данного класса, имеющий указанный набор ссылок.
      Может быть использовано в любом месте.
      Type должен быть медиаторным классом.
      Множество идентификаторов не должно содержать повторяющихся идентификаторов и должно совпадать с множеством идентификаторов реализационных полей, декларированных в классе Type и его предках.
      Каждый Expression должен иметь тот же тип, который имеет реализационная ссылка с соответствующим идентификатором.
      Тип результирующего выражения - Type.

      SE_MediatorCreationExpression ::= mediator Type (
      ( Identifier = Expression )? ( , Identifier = Expression )* )

      mediator $type ( $id_1 = $expr_1 , ... , $id_n = $expr_n )

      транслируется в вызов

      $type . #CreateMediator ( $type ) ( $expr_i_1 , ... , $expr_i_n )

      где $expr_i_k - исходные выражения, упорядоченные в порядке декларации соответствующих им реализационных ссылок (т.е. имеющих тот же идентификатор, который используется перед этим выражением).
      Порядок декларации реализационных ссылок следующий: ссылка, декларированная в предке считается идущей раньше ссылки, декларированной в потомке,
    2. SE_ImplicationExpression
      Это выражение обозначает логическую импликацию.
      Импликация правоассоциативна, т.е. A => B => C должно толковаться как A => (B => C).
      Может быть использовано в любом месте.
      Оба вложенных выражения должны иметь тип boolean.
      Тип результируюющего выражения - boolean.

      SE_ImplicationExpression ::= ConditionalOrExpression ( => ConditionalOrExpression )*

      $expr_1 => $expr_2 => ... => $expr_i => ... => $expr_(n-1) => $expr_n

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

      !( #( $expr_1 ) ) || !( #( $expr_2 ) ) || ... || !( #( $expr_i ) ) || ... || !( #( $expr_(n-1) ) ) || ( #( $expr_n ) )
    3. SE_PreExpression
      Это выражение имеет то значение, которое вложенное выражение имело в пре-состоянии данного события.
      Такое выражение называется далее пре-выражением.
      Может быть использовано только после одного из операторов branсh в рамках SE_Postcondition.
      Имеет тот же тип, что и вложенное выражение.

      Правила трансляции его см. в правилах трансляции постусловия.
    4. Выражения для получения описателей операций и связанных с ними данных
      1. Описатели операций

        SE_OperationExpression

        Это выражение обозначает объект-описатель операции (спецификационного метода, обратного метода, реакции).
        Используется для получения информации о структуре покрытий, определенных в них.
        Может быть использовано в любом месте.

        SE_OperationExpression ::= ( "#" )+ "super" | ( "#" )+ "this" | ( PrimaryExpression | ClassOrInterfaceType )? "#" Identifier "(" ( ParameterType )? ( "," ParameterType )* ")"

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

        ( PrimaryExpression )? $ MemberName ( ( TypeName ( , TypeName )* )? )
        Первая альтернатива этого выражения допустима в любом месте в рамках декларации типа Ch@se.
        При этом PrimaryExpression должно обозначать имя спецификационного типа, или иметь спецификационный тип, а MemberName - имя спецификационой операции (спецификационного метода, спецификационного оператора, спецификационного индексера, спецификационного поля-делегата или имя метода доступа к спецификационному свойству), имеющей указанные типы параметров.
        Может оказаться, что достаточно иметь возможность указывать таким образом только обратные операции. Но для гибкости и поддержки возможности сослаться на операцию в связи с разными поводами, а не только из трассы обратных вызовов, сделано как сейчас.
        Действительно нужно указывать все спецификационные операции: таким образом можно осуществлять доступ к информации о покрытиях.
         ( $expression )(1)? $ $operation ( $typename_1, ... , $typename_n )
        транслируется в

        если $expression обозначает спецификационный тип с именем $typename, то
        #derived ( $typename ) . #getClassOperationInfo ( "#string_representation ( $operation ( $typename_1, ... , $typename_n ) )" )

        иначе, если это выражение спецификационного типа или оно отсутсвует, то
        (1)?( #( $expression ) . ) #getOperationInfo ( "#string_representation ( $operation ( $typename_1, ... , $typename_n ) )" )

        Здесь #string_representation ( $operation ( $typename_1, ... , $typename_n ) ) - строковое представление сигнатуры операции, строящееся как конкатенация имени операции (это имя метода или определяемое правилами C# имя оператора, метода доступа к свойству или метода доступа по индексу), открывающейся скобки, списка полных имен типов параметров, перечисляемых через запятую, и закрывающей скобки.

        $this
        Вторая альтернатива может встречаться в рамках SE_PostBlock, после оператора branch по потоку управления.

        Выражение $this . Result имеет особые свойства. В рамках SE_PostBlock или MethodBody оно имеет тип, совпадающий с типом результата соответсвующей операции. Если тип результата данной операции - void, то использовать это выражение нельзя.
      2. Выражения для получения покрытий и их элементов

        SE_StaticOperationCoverageAccessExpression
        SE_StaticOperationCoverageItemAccessExpression
        SE_StaticClassCoverageAccessExpression
        SE_StaticClassCoverageItemAccessExpression

        ( PrimaryExpression )? $ MemberName ....
        Альтернатива этого выражения, начинающаяся с ( PrimaryExpression )? $ MemberName, допустима в любом месте.
        При этом PrimaryExpression должно обозначать имя спецификационного типа или иметь спецификационный тип, а MemberName - имя спецификационной операции, декларированной в данном типе. Соответствующую операцию будем называть референс операцией.

        ( PrimaryExpression )? $ MemberName . ( pre | branch | coverage.(...) ) ( ( ArgumentList )? )
        Скобки, окружающие ArgumentList, при этом обязательны, а сам список аргументов должен быть списком выражений, подходящих по правилам C# в качестве параметров референс операции.
        1. ... . pre ( ( ArgumentList )? )

          ( $expression )(1)? $ $operation . pre ( $argument_1, ... , $argument_n )
          транслируется в
        2. ... . branch ( ( ArgumentList )? )

          ( $expression )(1)? $ $operation . branch ( $argument_1, ... , $argument_n )
          транслируется в
          • Если $expression имеет спецификационный тип
            (1)?( #derived ( $typename ) . ) #getBranch($operation) ( #($argument_1), ... , #(argument_n) )
          • Иначе, т.е. если $expression обозначает имя спецификационного типа
            #derived ( $expression ) . #getBranch($operation) ( #( $argument_1 ), ... , #( argument_n ) )
        3. ... . coverage .(...) ) ( ( ArgumentList )? )

          ( $expression )(1)? $ $operation . coverage . $identifier ( $argument_1, ... , $argument_n )
          транслируется в
        4. ( PrimaryExpression )? $ MemberName .coverage ( ArgumentList )
          Скобки, окружающие ArgumentList, при этом обязательны, а сам список аргументов должен быть списком выражений, в котором первое имеет тип string, а список остальных подходит по правилам C# в качестве параметров референс операции.

          ( $expression )(1)? $ $operation . coverage ( $argument_1, ... , $argument_n, $argument_(n+1) )
          транслируется в

          Если $expression имеет спецификационный тип
          (1)?( #( $expression ) . ) #GetPartitionElement ( $operation_signature ) ( #($argument_1), ..., #($argument_n), #(argument_(n+1)) )

          Иначе, т.е. если $expression обозначает имя спецификационного типа
          #derived ( $expression ) . #GetPartitionElement ( $operation_signature ) ( #($argument_1), ..., #($argument_n), #(argument_(n+1)) )
        5. $this ....
          Вторая альтернатива может встречаться в рамках SE_MethodBody или MethodBody операции, переопределяющей спецификационную операцию в медиаторном классе. При этом референс операцией называется соответствующая спецификационная операция.
          Правила трансляции в рамках SE_MethodBody.
          Правила трансляции в рамках MethodBody операции медиаторного класса, переопределяющей спецификационную операцию.
        6. $base ....
          Третья альтернатива может встречаться только в рамках SE_MethodBody или MethodBody операции, переопределяющей спецификационную операцию в медиаторном классе. В первом случае операция должна совпадать по сигнатуре со спецификационной операцией в классе-предке данного, являющемся спецификационным классом или обратным спецификационным классом. При этом референс операцией называется соответсвующая спецификационная операция в классе-предке. Во втором случае референс-операцией является перегружаемая спецификационная операция.
          1. Правила трансляции в рамках SE_MethodBody.
          2. Правила трансляции в рамках MethodBody операции медиаторного класса, переопределяющей спецификационную операцию.
    5. Выражения для получения описателей событий и связанных с ними данных
      1. Описатели событий

        SE_EventInfoExpression

        Доделать
      2. Выражения для получения значений предусловия и элементов покрытий, связанных с событиями

        SE_EventPreExpression
        SE_DynamicOperationCoverageAccessExpression
        SE_DynamicOperationCoverageItemAccessExpression
        SE_DynamicClassCoverageAccessExpression
        SE_DynamicClassCoverageItemAccessExpression

        Доделать

      3. Событийные предикаты

        SE_ExpectEventConstraintExpression
        SE_OccuredEventConstraintExpression

        Прагматика.
        Такие предикаты должны отражать непосредственные причинно-следственные связи между событиями и не должны использоваться для описания случайно или опосредованно возникающих зависимостей.
        Это требование возникает из того соображения, что непосредственные причинно-следственные связи реже придется изменять при вносимых модификациях. Связь же опосредованная может значительно поменяться при изменении одного из ее элементов.

        Примеры:

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

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

        В то же время, если, например, мы можем снимать деньги со счета, находящегося в активированном состоянии, а активация может быть сделана вызовом одной из двух операций - внос количества денег, превышающего долг на определенную сумму, или переведение счета в привелигированный режим, лучше оформить активированное состояние как состояние и не опеределять его по тому, случались ли события, соответствующие вызовам описанных операций. Здесь связь между состоянием и возможностью снимать деньги - непосредственная, а между вызовами, переводящими счет в это состояние и той же возможностью - опосредованная. Например, условия перехода в активированное состояние могут поменяться.

        Доделать
        Использование @@this, @@@this и пр. в рамках событийных предикатов.
    6. thrown
      Это выражение обозначает ссылку на созданное в ходе работы метода исключение. Используется в постусловии для проверки ограничений на возникающие исключения.
      Может быть использовано только в постусловии после точки обращения к целевому методу.
    7. Ссылки на уточняемый и уточняющие объекты

      SE_RefinementReference

      Это выражение обозначает единственную реализационную ссылку в обощающем или уточняющем медиаторах при уточнении спецификаций.
      Может быть использовано только в рамках SE_Refined. Есть дополнительные ограничения на использование этого выражения в разных контекстах.
    8. SE_RelevantExpression

      Используется для выделение в пред- и постусловиях вызовов методов, код которых надо анализировать при анализе структуры предопределенных покрытий.

      Доделать