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.