examples/org.eclipse.ocl.examples.pivot/model/Pivot.ocl

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