| import 'Pivot.ecore' |
| |
| include 'Types.ocl' |
| |
| package ocl |
| |
| context Constraint |
| inv UniqueName: true -- _'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 defaultExpression <> null |
| |
| inv CompatibleDefaultExpression: defaultExpression <> null and defaultExpression.oclIsKindOf(ExpressionInOCL) implies CompatibleBody(defaultExpression) |
| |
| context Operation |
| inv CompatibleReturn: bodyExpression <> null and bodyExpression.oclIsKindOf(ExpressionInOCL) implies CompatibleBody(bodyExpression) |
| inv LoadableImplementation: |
| true |
| inv UniquePreconditionName: precondition->isUnique(name) |
| inv UniquePostconditionName: postcondition->isUnique(name) |
| |
| context Type |
| inv UniqueInvariantName: ownedInvariant->isUnique(name) |
| |
| context Variable |
| inv CompatibleInitialiserType: initExpression <> null implies initExpression.type.conformsTo(type) |
| |
| context IteratorExp |
| inv ClosureBodyTypeIsConformanttoIteratorType: |
| true |
| inv SortedByIteratorTypeIsComparable: |
| true |
| |
| context TypedMultiplicityElement |
| def: CompatibleBody(bodySpecification : ValueSpecification) : Boolean = |
| bodySpecification.type.conformsTo(self.type) |
| |
| 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(source.type.oclAsType (CollectionType).elementType.conformsTo(type)) |
| |
| /** 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 ArgumentTypeIsConformant: |
| 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.specializeIn(self, 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() |
| |
| --inv StaticSourceIsNull: referredOperation.isStatic implies source = null |
| |
| --inv NonStaticSourceIsConformant: let operation : Operation = self.referredOperation in |
| -- not operation.isStatic implies source <> null --.type.conformsTo(operation.owningType.specializeIn(self, operation.owningType)) |
| |
| |
| --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) |
| |
| context PropertyCallExp |
| def: getSpecializedReferredPropertyOwningType() : Type = referredProperty.owningType -- extended in Java code |
| def: getSpecializedReferredPropertyType() : Type = referredProperty.type -- extended in Java code |
| /** The type of the source conforms to the owning type of the property. */ |
| inv NonStaticSourceTypeIsConformant: not referredProperty.isStatic implies source.type.conformsTo(getSpecializedReferredPropertyOwningType()) |
| /** The type of the call expression is the type of the referred property. */ |
| inv CompatibleResultType: type = getSpecializedReferredPropertyType() |
| |
| --inv StaticSourceIsNull: referredProperty.isStatic implies source.oclAsType(Type).conformsTo(getSpecializedReferredPropertyOwningType()) |
| |
| context Element |
| def: getValue(stereotype : Type, propertyName : String) : Element[?] = null |
| |
| endpackage |