The AS-Domain-Mapping Package

The figure 27 shows the associations between the abstract syntax concepts and the domain concepts defined in this chapter. Each domain concept has a counterpart called model in the abstract syntax. Each model has one or more instances in the semantic domain. Note that in particular every OCL expression can have more than one evaluation. Still every evaluation has only one value. For example, the "asSequence" applied to a Set may have n! evaluations, which each give a different permutation of the elements in the set, but each evaluation has exactly one result value.






Well-formedness rules for the AS-Domain-Mapping.type-value Package

CollectionValue

[1] All elements in a collection value must have a type that conforms to the elementType of its corresponding CollectionType.

context CollectionValue inv:
    elements->forAll( e: Element | e.value.model.conformsTo( model.elementType ) )

DomainElement

No additional well-formedness rules.

Element

No additional well-formedness rules.

EnumValue

No additional well-formedness rules.

ObjectValue

[1] All bindings in an object value must correspond to attributes or associations defined in the object's Classifier.

context ObjectValue inv:
    history->forAll( snapshot | snapshot.bindings->forAll( b |
        self.model.allAttributes()->exists (attr | b.name = attr.name)
    or
        self.model.allAssociationEnds()->exists ( role | b.name = role.name) ) )

OclMessageValue

No additional well-formedness rules.

PrimitiveValue

No additional well-formedness rules.

SequenceTypeValue

No additional well-formedness rules.

SetTypeValue

No additional well-formedness rules.

StaticValue

No additional well-formedness rules.

TupleValue

[1] The elements in a tuple value must have a type that conforms to the type of the corresponding tuple parts.

    context TupleValue inv:
        elements->forAll( elem |    
                let   correspondingPart: Attribute =
                        self.model.allAttributes()->select( part | part.name = elem.name ) in
                elem.value.model.conformsTo( correspondingPart.type ) )

UndefinedValue

No additional well-formedness rules.

Value

No additional well-formedness rules.

Additional operations for the AS-Domain-Mapping.type-value Package

Value

[1] The additional operation isInstanceOf returns true if this value is an instance of the parameter classifier.

    context Value::isInstanceOf( c: Classifier ): Boolean
    pre: -- none
    post: result = self.model.conformsTo( c )

Well-formedness rules for the AS-Domain-Mapping.exp-eval Package


AssociationClassCallExpEval

[1] The string that represents the referredAssociationClass in the evaluation must be equal to the name of the referredAssociationClass in the corresponding expression.

    context AssociationClassCallExpEval inv:
        referredAssociationClass = model.referredAssociationClass.name

[2] The result value of an association class call expression evaluation that has qualifiers, is determined according to the following rule. The `normal' determination of result value is already given in section 10.3.7 ("Well-formedness Rules of theEvaluations package").

    let
    -- the attributes that are the formal qualifiers. Because and association class has two or
    -- more association ends, we must select the qualifiers from the other end(s), not from
    -- the source of this expression. We allow only 2-ary associations.
        formalQualifiers : Sequence(Attribute) =
                self.model.referredAssociationClass.connection->any( c |
                            c <> self.navigationSource).qualifier.asSequence() ,

    -- the attributes of the class at the qualified end. Here we already assume that an   
    -- AssociationEnd will be owned by a Classifier, as will most likely be the case in the
    -- UML 2.0 Infrastructure.
        objectAttributes: Sequence(Attribute) =
                self.model.referredAssociationClass.connection->any( c |
                            c <> self.navigationSource).owner.feature->select( f |
                                    f.isOclType( Attribute ).asSequence() ,

    -- the rolename of the qualified association end
        qualifiedEnd: String = self.model.referredAssociationClass.connection->any( c |
                c <> self.navigationSource).name ,

    -- the values for the qualifiers given in the ocl expression
        qualifierValues : Sequence( Value ) = self.qualifiers.asSequence()

    -- the objects from which a subset must be selected through the qualifiers
        normalResult =
                source.resultValue.getCurrentValueOf(referredAssociationClass.name)
        in
            -- if name of attribute of object at qualified end equals name of formal qualifier then
            -- if value of attribute of object at qualified end equals the value given in the exp
            -- then select this object and put it in the resultValue of this expression.
            qualifiers->size <> 0 implies
                normalResult->select( obj |
                    Sequence{1..formalQualifiers->size()}->forAll( i |
                        objectAttributes->at(i).name = formalQualifiers->at(i).name and
                        obj.qualifiedEnd.getCurrentValueOf( objectAttributes->at(i).name ) =
                                qualifiersValues->at(i) ))



AssociationEndCallExpEval

[1] The string that represents the referredAssociationEnd in the evaluation must be equal to the name of the referredAssociationEnd in the corresponding expression.

    context AssociationEndCallExpEval inv:
  referredAssociationEnd = model.referredAssociationEnd.name

[2] The result value of an association end call expression evaluation that has qualifiers, is determined according to the following rule. The `normal' determination of result value is already given in section 10.3.7 ("Well-formedness Rules of theEvaluations package").

    let
    -- the attributes that are the formal qualifiers
        formalQualifiers : Sequence(Attribute) = self.model.referredAssociationEnd.qualifier ,

    -- the attributes of the class at the qualified end
        objectAttributes: Sequence(Attribute) =
                (if self.resultValue.model.isOclKind( Collection ) implies
                then self.resultValue.model.oclAsType( Collection ).elementType->
                        collect( feature->asOclType( Attribute ) )
                else self.resultValue.model->collect( feature->asOclType( Attribute ) )
                endif).asSequence() ,

  -- the values for the qualifiers given in the ocl expression
      qualifierValues : Sequence( Value ) = self.qualifiers.asSequence()

  -- the objects from which a subset must be selected through the qualifiers
      normalResult =
                source.resultValue.getCurrentValueOf(referredAssociationEnd.name)

       in
    -- if name of attribute of object at qualified end equals name of formal qualifier then
    -- if value of attribute of object at qualified end equals the value given in the exp
    -- then select this object and put it in the resultValue of this expression.

    qualifiers->size <> 0 implies
           normalResult->select( obj |
                Sequence{1..formalQualifiers->size()}->forAll( i |
                        objectAttributes->at(i).name = formalQualifiers->at(i).name and
                        obj.getCurrentValueOf( objectAttributes->at(i).name ) =
                                    qualifiersValues->at(i) ))


AttributeCallExpEval

[1] The string that represents the referredAttribute in the evaluation must be equal to the name of the referredAttribute in the corresponding expression.

    context AttributeCallExpEval inv:
    referredAttribute = model.referredAttribute.name

BooleanLiteralExpEval

[1] The result value of a boolean literal expression is equal to the literal expression itself (`true' or `false'). Because the booleanSymbol attribute in the abstract syntax is of type Boolean as defined in the MOF, and resultValue is of type Primitive as defined in this chapter, a conversion is neccessary. For the moment, we assume the additional operation MOF-booleanToOCLboolean() exists. This will need to be re-examined when the MOF and/or UML Infrastructure submissions are finalised.

    context BooleanLiteralExpEval inv:
    resultValue = model.booleanSymbol.MOFbooleanToOCLboolean()

CollectionItemEval

No extra well-formedness rules.

CollectionLiteralExpEval

No extra well-formedness rules.

CollectionLiteralPartEval

No extra well-formedness rules.

CollectionRangeEval

No extra well-formedness rules.

EvalEnvironment

Because there is no mapping of name space to an abstract syntax concept, there are no extra well-formedness rules.

LiteralExpEval

No extra well-formedness rules.

LoopExpEval

No extra well-formedness rules.

EnumLiteralExpEval

[1] The result value of an EnumLiteralExpEval must be equal to one of the literals defined in its type.

context EnumLiteralExpEval inv:
model.type->includes( self.resultValue )

IfExpEval

[1] The condition evaluation corresponds with the condition of the expression, and likewise for the thenExpression and the else Expression.

context IfExpEval inv:
    condition.model = model.condition
    thenExpression.model = model.thenExpression
    elseExpression.model = model.elseExpression

IntegerLiteralExpEval

    context IntegerLiteralExpEval inv:
  resultValue = model.integerSymbol

IterateExpEval

[1] The model of the result of an iterate expression evaluation is equal to the model of the result of the associated IterateExp.

    context IterateExpEval
  inv: result.model = model.result


IteratorExpEval

No extra well-formedness rules.

LetExpEval

[1] All parts of a let expression evaluation correspond to the parts of its associated LetExp.

    context LetExpEval inv:
        in.model = model.in and
        initExpression.model = model.initExpression and
        variable = model.variable.varName

LoopExpEval

[1] All sub evaluations have the same model, which is the body of the associated LoopExp.

    context LoopExpEval
  inv: bodyEvals->forAll( model = self.model )

ModelPropertyCallExpEval

No extra well-formedness rules.

NumericLiteralExpEval

No extra well-formedness rules.

NavigationCallExpEval

[1] The string that represents the navigation source in the evaluation must be equal to the name of the navigationSource in the corresponding expression.

    context NavigationCallExpEval inv:
    navigationSource = model.navigationSource.name

[2] The qualifiers of a navigation call expression evaluation must correspond with the qualifiers of the associated expression.

    context NavigationCallExpEval inv:
        Sequence{1..qualifiers->size()}->forAll( i |
                qualifiers->at(i).model = model.qualifiers->at(i).type )

OclExpEval

[1] The result value of the evaluation of an ocl expression must be an instance of the type of that expression.

    context OclExpEval
   inv: resultValue.isInstanceOf( model.type )


OclMessageExpEval

[1] An ocl message expression evaluation must correspond with its message expression.

    context OclMessageExpEval
    inv: target.model = model.target
    inv: Set{1..arguments->size()}->forall (i | arguments->at(i) = model.arguments->at(i) )

[2] The name of the resulting ocl message value must be equal to the name of the operation or signal indicated in the message expression.

    context OclMessageExpEval inv:
           if model.operation->size() = 1
           then resultValue.name = model.operation.name
           else resultValue.name = model.signal.name
           endif

[3] The isSignal, isSyncOperation, and isAsyncOperation attributes of the result value of an ocl message expression evaluation must correspond to the operation indicated in the ocl message expression.

    context OclMessageExpEval
    inv:
        if model.calledOperation->size() = 1
        then model.calledOperation.isAsynchronous = true implies
            resultValue.isAsyncOperation = true
        else -- message represents sending a signal
            resultValue.isSignal = true
        endif

[4] The arguments of an ocl message expression evaluation must correspond to the formal input parameters of the operation, or the attributes of the signal indicated in the ocl message expression.

    context OclMessageExpEval
    inv: model.calledOperation->size() = 1 implies
        Sequence{1.. arguments->size()} ->forAll( i |
            arguments->at(i).variable->size() = 1 implies
                model.calledOperation.operation.parameter->
                    select( kind = ParameterDirectionKind::in )->at(i).name =
                            arguments->at(i).variable
        and
             arguments->at(i).expression->size() = 1 implies
                model.calledOperation.operation.parameter->
                    select( kind = ParameterDirectionKind::in )at(i).type =
                        arguments->at(i).expression.model
   inv: model.sentSignal->size() = 1 implies
       Sequence{1.. arguments->size()} ->forAll( i |
            arguments->at(i).variable->size() = 1 implies
                model.sentSignal.signal.feature->select(
                    arguments->at(i).variable )->notEmpty()
        and
            arguments->at(i).expression->size() = 1 implies
                model.sentSignal.signal.feature.oclAsType(StructuralFeature).type =
                    arguments->at(i).expression.model


[5] The arguments of the return message of an ocl message expression evaluation must correspond to the names given by the formal output parameters, and the result type of the operation indicated in the ocl message expression. Note that the Parameter type is defined in the UML 1.4 foundation package.

    context OclMessageExpEval
    inv: let returnArguments: Sequence{ NameValueBindings ) =
                        resultValue.returnMessage.arguments ,
          formalParameters: Sequence{ Parameter } =
                model.calledOperation.operation.parameter
    in
         resultValue.returnMessage->size() = 1 and model.calledOperation->size() = 1 implies
        -- 'result' must be present and have correct type
                returnArguments->any( name = 'result' ).value.model =
                            formalParameters->select( kind = ParameterDirectionKind::return ).type
        and
        -- all 'out' parameters must be present and have correct type
        Sequence{1.. returnArguments->size()} ->forAll( i |
                returnArguments->at(i).name =
                            formalParameters->select( kind = ParameterDirectionKind::out )->at(i).name
        and
                returnArguments->at(i).value.model =
                            formalParameters->select( kind = ParameterDirectionKind::out )->at(i).type )


OclMessageArgEval

[1] An ocl message argument evaluation must correspond with its argument expression.

    context OclMessageArgEval
  inv: model.variable->size() = 1
           implies variable->size() = 1 and variable.symbol = model.variable.name
  inv: model.expression->size() = 1
           implies expression and expression.model = model.expression


OperationCallExpEval

[1] The result value of an operation call expression will have the type given by the Operation being called, if the operation has no out or in/out parmeters, else the type will be a tuple containing all out, in/out parameters and the result value.

    context OperationCallEval inv:
    let outparameters : Set( Parameter ) = referedOperation.parameter->select( p |
            p.kind = ParameterDirectionKind::in/out or
            p.kind = ParameterDirectionKind::out)
    in
            if outparameters->isEmpty()
            then resultValue.model = model.referredOperation.parameter
                    ->select( kind = ParameterDirectionKind::result ).type
            else resultValue.model.oclIsType( TupleType ) and
                    outparameters->forAll( p |
                            resultValue.model.attribute->exist( a | a.name = p.name and a.type = p.type ))
            endif


[2] The string that represents the referred operation in the evaluation must be equal to the name of the referredOperation in the corresponding expression.

    context OperationCallExpEval inv:
       referredOperation = model.referredOperation.name


[3] The arguments of an operation call expression evaluation must correspond with the arguments of its associated expression.

    context OperationCallExpEval inv:
        Sequence{1..arguments->size}->forAll( i |
                arguments->at(i).model = model.arguments->at(i) )

PropertyCallExpEval

[1] The source of the evaluation of a property call corresponds to the source of its associated expression.

    context PropertyCallExpEval inv:
    source.model = model.source

PrimitiveLiteralExpEval

No extra well-formedness rules.

RealLiteralExpEval

    context RealLiteralExpEval inv:
    resultValue = model.realSymbol

StringLiteralExpEval

    context StringLiteralExpEval inv:
    resultValue = model.stringSymbol  

TupleLiteralExpEval

    context TupleLiteralExpEval inv:
    model.tuplePart = tuplePart.model

UnspecifiedValueExpEval

[1] The result of an unspecified value expression is a randomly picked instance of the type of the expression.

    context UnspecifiedValueExpEval
    inv: resultValue = model.type.allInstances()->any( true )
    inv: resultValue.model = model.type

VariableDeclEval

    context VariableDeclEval inv:
    model.initExpression = initExpression.model

VariableExpEval

No extra well-formedness rules.