Description
Constructs::Operation reuses the definition of Operation from Basic. It adds a specialization to
Constructs::BehavioralFeature.
The specification of an operation defines what service it provides, not how this is done, and can include a list of pre- and
postconditions.
Attributes
/isOrdered : Boolean |
Redefines the corresponding property from Basic to derive this information from the return result for this Operation. |
isQuery : Boolean |
Specifies whether an execution of the BehavioralFeature leaves the state of the system unchanged (isQuery=true) or whether side effects may occur (isQuery=false). The default value is false. |
/isUnique : Boolean |
Redefines the corresponding property from Basic to derive this information from the return result for this Operation. |
/lower : Integer[0..1] |
Redefines the corresponding property from Basic to derive this information from the return result for this Operation. |
/upper : UnlimitedNatural[0..1] | Redefines the corresponding property from Basic to derive this information from the return result for this Operation. |
bodyCondition: Constraint[0..1] | An optional Constraint on the result values of an invocation of this Operation. Subsets Namespace.ownedMember. |
formalParameter: Parameter[*] | Specifies the formal parameters for this Operation. Redefines Basic::Operation.ownedPa- rameter and BehavioralFeature.formalParameter. |
postcondition: Constraint[*] |
An optional set of Constraints specifying the state of the system when the Operation is completed. Subsets Namespace.ownedMember. |
precondition: Constraint[*] |
An optional set of Constraints on the state of the system when the Operation is invoked. Subsets Namespace.ownedMember. |
raisedException: Type[*] |
References the Types representing exceptions that may be raised during an invocation of this operation. Redefines Basic::Operation.raisedException and BehavioralFea- ture.raisedException. |
redefinedOperation: Operation[*] | References the Operations that are redefined by this Operation. Subsets RedefinableEle- ment.redefinedElement. |
/type: Type[0..1] |
Redefines the corresponding property from Basic to derive this information from the return result for this Operation. |
Constraints
isOrdered = if returnResult->size() = 1 then returnResult->any().isOrdered else false endif
isUnique = if returnResult->size() = 1 then returnResult->any().isUnique else true endif
lower = if returnResult->size() = 1 then returnResult->any().lower else Set{} endif
upper = if returnResult->size() = 1 then returnResult->any().upper else Set{} endif
type = if returnResult->size() = 1 then returnResult->any().type else Set{} endif
bodyCondition->notEmpty() implies isQuery
Additional Operations
Operation::isConsistentWith(redefinee: RedefinableElement): Boolean;
pre: redefinee.isRedefinitionContextValid(self)
isConsistentWith = (redefinee.oclIsKindOf(Operation) and
let op: Operation = redefinee.oclAsType(Operation) in
self.formalParameter.size() = op.formalParameter.size() and
self.returnResult.size() = op.returnResult.size() and
forAll(i | op.formalParameter[i].type.conformsTo(self.formalParameter[i].type)) and
forAll(i | op.returnResult[i].type.conformsTo(self.returnResult[i].type))
)
Semantics
An operation is invoked on an instance of the classifier for which the operation is a feature. A static operation is invoked
on the classifier owning the operation, hence it can be invoked without an instance.
The preconditions for an operation define conditions that must be true when the operation is invoked. These preconditions
may be assumed by an implementation of this operation.
The postconditions for an operation define conditions that will be true when the invocation of the operation is completes
successfully, assuming the preconditions were satisfied. These postconditions must be satisfied by any implementation of
the operation.
The bodyCondition for an operation constrains the return result. The bodyCondition differs from postconditions in that
the bodyCondition may be overridden when an operation is redefined, whereas postconditions can only be added during
redefinition.
An operation may raise an exception during its invocation. When an exception is raised, it should not be assumed that the
postconditions or bodyCondition of the operation are satisfied.
An operation may be redefined in a specialization of the featured classifier. This redefinition may specialize the types of
the formal parameters or return results, add new preconditions or postconditions, add new raised exceptions, or otherwise
refine the specification of the operation.
Each operation states whether or not its application will modify the state of the instance or any other element in the model
(isQuery).
Semantic Variation Points
The behavior of an invocation of an operation when a precondition is not satisfied is a semantic variation point.
Notation
An operation is shown as a text string of the form:
visibility name ( parameter-list ) : property-string
Presentation Options
The parameter list can be suppressed.
Style Guidelines
An operation name typically begins with a lowercase letter.
Examples
display ()
-hide ()
+createWindow (location: Coordinates, container: Container [0..1]): Window
+toString (): String {query}