import 'Pivot.ecore' | |
include 'Types.ocl' | |
package ocl | |
context Constraint | |
inv UniqueName: _'context'.ownedRule->excluding(self)->forAll(name <> self.name or stereotype <> self.stereotype) | |
context Element | |
def: allOwnedElements() : Set(Element) = | |
--self->closure(oclContents()) | |
oclContents() | |
--FIXME oclContainer() suspect on DomainElements | |
--def: owner : Element = oclContainer() | |
/** | |
* Elements that must be owned must have an owner. | |
*/ | |
-- inv has_owner: | |
-- mustBeOwned() implies owner->notEmpty() | |
/** | |
* An element may not directly or indirectly own itself. | |
*/ | |
inv not_own_self: | |
not allOwnedElements()->includes(self) | |
-- def: allOwnedElements() : Set(Element) = | |
-- ownedElement->union(ownedElement->collect(e | e.allOwnedElements()))->asSet() | |
-- def: mustBeOwned() : Boolean = true | |
context ParameterableElement | |
def: isCompatibleWith(p : ParameterableElement) : Boolean = | |
p.oclIsKindOf(self.oclType()) | |
context Property | |
def: isAttribute(p : Property) : Boolean = | |
--Type.allInstances()->exists(c| c.ownedAttribute->includes(p)) | |
let container : ocl::OclElement = oclContainer() in container.oclIsKindOf(Type) and container.oclAsType(Type).ownedAttribute->includes(self) | |
--inv DerivedIsInitialised: isDerived implies ownedRule->one(stereotype = 'derivation') or ownedRule->one(stereotype = 'initial') | |
inv CompatibleInitialiser: isDerived implies | |
let derivedConstraint : Constraint = ownedRule->any(stereotype = 'derivation') in | |
let initialConstraint : Constraint = ownedRule->any(stereotype = 'initial') in | |
let derivedSpecification : ValueSpecification = if derivedConstraint <> null then derivedConstraint.specification else null endif in | |
let initialSpecification : ValueSpecification = if initialConstraint <> null then initialConstraint.specification else null endif in | |
let initialiser: ValueSpecification = if derivedSpecification <> null then derivedSpecification else initialSpecification endif in | |
initialiser <> null and initialiser.oclIsKindOf(ExpressionInOcl) implies CompatibleBody(initialiser) | |
context Operation | |
inv CompatibleReturn: | |
let bodyConstraint : Constraint = ownedRule->any(stereotype = 'body') in | |
bodyConstraint <> null implies | |
let bodySpecification : ValueSpecification = bodyConstraint.specification in | |
bodySpecification <> null and bodySpecification.oclIsKindOf(ExpressionInOcl) implies CompatibleBody(bodySpecification) | |
context TypedMultiplicityElement | |
def: CompatibleBody(bodySpecification : ValueSpecification) : Boolean = | |
let bodyType : Type = bodySpecification.type in | |
if bodyType.oclIsKindOf(CollectionType) then | |
let bodyCollectionType : CollectionType = bodyType.oclAsType(CollectionType) in | |
let bodyElementType : Type = bodyCollectionType.elementType in | |
bodyElementType.conformsTo(self.type) | |
and self.isOrdered = (bodyCollectionType.conformsTo(OrderedSet(OclAny)) or bodyCollectionType.conformsTo(Sequence(OclAny))) | |
and self.isUnique = (bodyCollectionType.conformsTo(OrderedSet(OclAny)) or bodyCollectionType.conformsTo(Set(OclAny))) | |
else | |
bodyType.conformsTo(self.type) | |
endif | |
def: makeParameter() : Parameter = Parameter{name='name'} | |
---ExpressionWFRs.ocl----- | |
--context PropertyCallExp | |
/** The type of the call expression is the type of the referred property. */ | |
--inv TypeIsReferredPropertyType: type = referredProperty.type | |
context BooleanLiteralExp | |
/** The type of a boolean Literal expression is the type Boolean. */ | |
inv TypeIsBoolean: self.type = Boolean | |
context CollectionLiteralExp | |
/** 'Collection' is an abstract class on the M1 level and has no M0 instances. */ | |
inv CollectionKindIsConcrete: kind <> CollectionKind::Collection | |
context CollectionLiteralExp | |
/** The type of a collection literal expression is determined by the collection kind selection and the common | |
supertype of all elements. Note that the definition below defines only an upper bound on the elementType. The usage of | |
the CollectionLiteralExp defines a lower bound. If the elementType is not explicitly specified, the elementType must be | |
chosen to ensure the well-formedness of the elements of the CollectionLiteralExp and the usage of the | |
CollectionLiteralExp. | |
For instance in | |
acc : Set(Real) = Set{1}->excluding(-1) | |
Set{1} is well formed for any type Set(T) where T ≤ UnlimitedNatural. Well-formedness of the excluding operation call | |
requires T ≤ Integer, and well-formedness of the initializer requires Real ≤ T. The overall expression is therefore only | |
well-formed if Real ≤ T ≤ Integer. Either Set(Real) or Set(Integer) are well-formed. The most general type, Set(Real), is | |
recommended since it minimizes type conversions and can often be easily deduced by considering the result type. | |
*/ | |
inv SetKindIsSet: kind = CollectionKind::Set implies type.oclIsKindOf (SetType) | |
inv OrderedSetKindIsOrderedSet: kind = CollectionKind::OrderedSet implies type.oclIsKindOf (OrderedSetType) | |
inv SequenceKindIsSequence: kind = CollectionKind::Sequence implies type.oclIsKindOf (SequenceType) | |
inv BagKindIsBag: kind = CollectionKind::Bag implies type.oclIsKindOf (BagType) | |
--inv ElementTypeIsCommonElementType: let elementType : Type = part->iterate (p; c : Classifier = OclVoid | c.commonSuperType (p.type)) | |
--in elementType.conformsTo(type.oclAsType (CollectionType).elementType) | |
/* CollectionLiteralPart | |
No additional well-formedness rules. */ | |
context CollectionItem | |
/** The type of a CollectionItem is the type of the item expression. */ | |
inv TypeIsItemType: type = item.type | |
--context CollectionRange | |
/** The type of a CollectionRange is the common supertype of the expressions taking part in the range. */ | |
--inv TypeIsCommonType: type = first.type.commonSuperType (last.type) | |
context EnumLiteralExp | |
/** The type of an enum Literal expression is the type of the referred literal. */ | |
inv TypeIsEnumerationType: self.type = referredEnumLiteral.enumeration | |
context IfExp | |
/** The type of the condition of an if expression must be Boolean. */ | |
inv ConditionTypeIsBoolean: self.condition.type = Boolean | |
/* The type of the if expression is the most common supertype of the else and then expressions. */ | |
--context IfExp | |
--inv TypeIsCommonType: self.type = thenExpression.type.commonSuperType(elseExpression.type) | |
context IntegerLiteralExp | |
/** The type of an integer Literal expression is the type Integer. */ | |
inv TypeIsInteger: self.type = Integer | |
context IteratorExp | |
/** There is exactly one iterator. */ | |
inv AnyHasOneIterator: name = 'any' implies iterator->size() = 1 | |
context IteratorExp | |
/** The type is the same as the source element type */ | |
inv AnyTypeIsSourceElementType: name = 'any' implies type = source.type.oclAsType(CollectionType).elementType | |
context IteratorExp | |
/** The type of the body must be Boolean. */ | |
inv AnyBodyTypeIsBoolean: name = 'any' implies _'body'.type = 'Boolean' | |
context IteratorExp | |
/** There is exactly one iterator. */ | |
inv ClosureHasOneIterator: name = 'closure' implies iterator->size() = 1 | |
context IteratorExp | |
/** The collection type for an OrderedSet or a Sequence source type is OrderedSet. | |
* For any other source the collection type is Set. */ | |
inv ClosureTypeIsUniqueCollection: name = 'closure' implies | |
if source.type.oclIsKindOf(SequenceType) or source.type.oclIsKindOf(OrderedSetType) then | |
type.oclIsKindOf(OrderedSetType) | |
else | |
type.oclIsKindOf(SetType) | |
endif | |
context IteratorExp | |
/** The source element type is the same as type of the body elements or element. */ | |
inv ClosureSourceElementTypeIsBodyElementType: name = 'closure' implies | |
source.type.oclAsType(CollectionType).elementType = | |
if _'body'.type.oclIsKindOf(CollectionType) | |
then _'body'.type.oclAsType(CollectionType).elementType | |
else _'body'.type | |
endif | |
context IteratorExp | |
/** The element type is the same as the source element type. */ | |
inv ClosureElementTypeIsSourceElementType: name = 'closure' implies | |
type.oclAsType(CollectionType).elementType | |
= source.type.oclAsType(CollectionType).elementType | |
context IteratorExp | |
/** There is exactly one iterator. */ | |
inv CollectHasOneIterator: name = 'collect' implies iterator->size() = 1 | |
context IteratorExp | |
/* The collection type for an OrderedSet or a Sequence type is a Sequence, | |
* the result type for any other collection type is a Bag. | |
*/ | |
inv CollectTypeIsUnordered: name = 'collect' implies | |
if source.type.oclIsKindOf(SequenceType) or source.type.oclIsKindOf(OrderedSetType) then | |
type.oclIsKindOf(SequenceType) | |
else | |
type.oclIsKindOf(BagType) | |
endif | |
context IteratorExp | |
/** The element type is the type of the body elements. */ | |
inv CollectElementTypeIsSourceElementType: name = 'collect' implies | |
type.oclAsType(CollectionType).elementType = | |
_'body'.type.oclAsType(CollectionType).elementType | |
context IteratorExp | |
/** There is exactly one iterator. */ | |
inv CollectNestedHasOneIterator: name = 'collectNested' implies iterator->size() = 1 | |
context IteratorExp | |
/** The type is a Bag. */ | |
inv CollectNestedTypeIsBag: name = 'collectNested' implies type.oclIsKindOf(BagType) | |
context IteratorExp | |
/** The type is the type of source. */ | |
inv CollectNestedTypeIsBodyType: name = 'collectNested' implies type = _'body'.type | |
context IteratorExp | |
/** The type must be Boolean. */ | |
inv ExistsTypeIsBoolean: name = 'exists' implies type = Boolean | |
context IteratorExp | |
/** The type of the body must be Boolean. */ | |
inv ExistsBodyTypeIsBoolean: name = 'exists' implies _'body'.type = Boolean | |
context IteratorExp | |
/** The type must be Boolean. */ | |
inv ForAllTypeIsBoolean: name = 'forAll' implies type = Boolean | |
context IteratorExp | |
/** The type of the body must be Boolean. */ | |
inv ForAllBodyTypeIsBoolean: name = 'forAll' implies _'body'.type = Boolean | |
context IteratorExp | |
/** There is exactly one iterator. */ | |
inv IsUniqueHasOneIterator: name = 'isUnique' implies iterator->size() = 1 | |
context IteratorExp | |
/** The type must be Boolean. */ | |
inv IsUniqueTypeIsBoolean: name = 'isUnique' implies type = Boolean | |
context IteratorExp | |
/** There is exactly one iterator. */ | |
inv OneHasOneIterator: name = 'one' implies iterator->size() = 1 | |
context IteratorExp | |
/** The type is Boolean */ | |
inv OneTypeIsBoolean: name = 'one' implies type = Boolean | |
context IteratorExp | |
/** The type of the body must be Boolean. */ | |
inv OneBodyTypeIsBoolean: name = 'one' implies _'body'.type = Boolean | |
context IteratorExp | |
/** There is exactly one iterator. */ | |
inv RejectOrSelectHasOneIterator: name = 'reject' or name = 'select' implies iterator->size() = 1 | |
context IteratorExp | |
/** The type is the same as the source. */ | |
inv RejectOrSelectTypeIsSourceType: name = 'reject' or name = 'select' implies type = source.type | |
context IteratorExp | |
/** The type of the body must be Boolean. */ | |
inv RejectOrSelectTypeIsBoolean: name = 'reject' or name = 'select' implies type = Boolean | |
context IteratorExp | |
/** There is exactly one iterator. */ | |
inv SortedByHasOneIterator: name = 'sortedBy' implies iterator->size() = 1 | |
context IteratorExp | |
/** The collection type for an OrderedSet or a Sequence type is a Sequence, the result type for any other collection type is Bag. */ | |
inv SortedByIsOrderedIfSourceIsOrdered: name = 'sortedBy' implies | |
if source.type.oclIsKindOf(SequenceType) or source.type.oclIsKindOf(BagType) then | |
type.oclIsKindOf(SequenceType) | |
else | |
type.oclIsKindOf(OrderedSetType) | |
endif | |
context IteratorExp | |
/** The element type is the type of the body elements. */ | |
inv SortedByElementTypeIsSourceElementType: name = 'sortedBy' implies | |
type.oclAsType(CollectionType).elementType = | |
_'body'.type.oclAsType(CollectionType).elementType | |
context IterateExp | |
/** The type of the iterate is the type of the result variable. */ | |
inv TypeIsResultType: type = result.type | |
context IterateExp | |
/** The type of the body expression must conform to the declared type of the result variable. */ | |
inv BodyTypeConformsToResultType: _'body'.type.conformsTo(result.type) | |
context IterateExp | |
/** A result variable must have an init expression. */ | |
inv OneInitializer: self.result.initExpression->size() = 1 | |
/*------------- unescaped in */ | |
context LetExp | |
/** The type of a Let expression is the type of the in expression. */ | |
inv TypeIsInType: type = _'in'.type | |
/** LiteralExp | |
No additional well-formedness rules. */ | |
context LoopExp | |
/** The type of the source expression must be a collection. */ | |
inv SourceIsCollection: source.type.oclIsKindOf (CollectionType) | |
context LoopExp | |
/** The loop variable of an iterator expression has no init expression. */ | |
inv NoInitializers: self.iterator->forAll(initExpression->isEmpty()) | |
context IteratorExp | |
/** The type of each iterator variable must be the type of the elements of the source collection. */ | |
inv IteratorTypeIsSourceElementType: self.iterator->forAll(type = source.type.oclAsType (CollectionType).elementType) | |
/** FeatureCallExp | |
No additional well-formedness rules. */ | |
/** NumericLiteralExp | |
No additional well-formedness rules. */ | |
/** OclExpression | |
No additional well-formedness rules. */ | |
--context MessageExp | |
/** If the message is an operation call action, the arguments must conform to the parameters of the operation. */ | |
--inv: calledOperation->notEmpty() implies | |
--argument->forAll (a | a.type.conformsTo | |
--(self.calledOperation.operation.ownedParameter-> | |
--select( kind = ParameterDirectionKind::_'in' ) | |
--->at (argument->indexOf (a)).type)) | |
--context MessageExp | |
/** If the message is a send signal action, the arguments must conform to the attributes of the signal. */ | |
--inv: sentSignal->notEmpty() implies | |
--argument->forAll (a | a.type.conformsTo | |
--(self.sentSignal.signal.ownedAttribute | |
--->at (argument->indexOf (a)).type)) | |
--context MessageExp | |
/** If the message is a call operation action, the operation must be an operation of the type of the target expression. */ | |
--inv: calledOperation->notEmpty() implies | |
--target.type.allOperations()->includes(calledOperation.operation) | |
context MessageExp | |
/** An OCL message has either a called operation or a sent signal. */ | |
inv OneCallOrOneSend: calledOperation->size() + sentSignal->size() = 1 | |
context MessageExp | |
/** The target of an OCL message cannot be a collection. */ | |
inv TargetIsNotACollection: not target.type.oclIsKindOf (CollectionType) | |
/*------------- spelling: arguments */ | |
--context OperationCallExp | |
/** All the arguments must conform to the parameters of the referred operation. */ | |
/*inv ArgumentType: | |
let operation : Operation = self.referredOperation in | |
let parameters : OrderedSet(Parameter) = operation.ownedParameter in | |
let selfType : Type = operation.owningType in | |
Sequence{1..argument->size()}->forAll (i | | |
let argument : OclExpression = argument->at(i) in | |
let parameter : Parameter = parameters->at(i) in | |
let parameterType : Type = parameter.type in | |
argument.type.conformsTo(parameterType.resolveSelfType(selfType))) */ | |
/*------------- spelling: arguments */ | |
context OperationCallExp | |
/** There must be exactly as many arguments as the referred operation has parameters. */ | |
inv ArgumentCount: argument->size() = referredOperation.ownedParameter->size() | |
--context OperationCallExp | |
/** An additional attribute refParams lists all parameters of the referred operation except the return and out parameter(s). */ | |
--def: refParams: Sequence(Parameter) = referredOperation.ownedParameter->select (p | | |
--p.kind <> ParameterDirectionKind::return or | |
--p.kind <> ParameterDirectionKind::out) | |
endpackage |