Operation (as specialized)

An operation is a behavioral feature of a classfier that specifies the name, type, parameters, and constraints for invoking
an associated behavior.

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.
Associations
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

  1. If this operation has a single return result, isOrdered equals the value of isOrdered for that parameter. Otherwise isOrdered
    is false.

    isOrdered = if returnResult->size() = 1 then returnResult->any().isOrdered else false endif

  2. If this operation has a single return result, isUnique equals the value of isUnique for that parameter. Otherwise isUnique is
    true.

    isUnique = if returnResult->size() = 1 then returnResult->any().isUnique else true endif

  3. If this operation has a single return result, lower equals the value of lower for that parameter. Otherwise lower is not
    defined.

    lower = if returnResult->size() = 1 then returnResult->any().lower else Set{} endif

  4. If this operation has a single return result, upper equals the value of upper for that parameter. Otherwise upper is not
    defined.

    upper = if returnResult->size() = 1 then returnResult->any().upper else Set{} endif

  5. If this operation has a single return result, type equals the value of type for that parameter. Otherwise type is not defined.

    type = if returnResult->size() = 1 then returnResult->any().type else Set{} endif

  6. A bodyCondition can only be specified for a query operation.

    bodyCondition->notEmpty() implies isQuery

Additional Operations

  1. The query isConsistentWith() specifies, for any two Operations in a context in which redefinition is possible, whether
    redefinition would be logically consistent. A redefining operation is consistent with a redefined operation if it has the
    same number of formal parameters, the same number of return results, and the type of each formal parameter and return
    result conforms to the type of the corresponding redefined parameter or return result.
    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}