Postcondition

Like a precondition, a postcondition is a constraint that may be linked to an Operation of a Classifier. The purpose of a postcondition is to specify the conditions that must hold after the operation executes. A postcondition consists of an OCL xpression of type Boolean. The expression must evaluate to true at the moment that the operation stops executing, but only for the instance that has just executed the operation. Within an OCL expression used in a postcondition, the "@pre" mark can be used to refer to values at precondition time. The variable result refers to the return value of the operation if there is any.

The placement of a postcondition in the UML metamodel is equal to the placement of a precondition, which is shown in Figure 31. The following well-formedness rule must hold. This rule also defines the value of the contextual Classifier.
 

Well-formedness rules


[1] The Constraint has the stereotype <<postcondition>> (A), and it is attached to only one model element (B), that is an BehavioralFeature (C), which has an owner (D). The contextual classifier is the owner of the operation to which the constraint is attached, and the type of the OCL expression must be Boolean

context Expression
inv: self.constraint.stereotype.name = 'postcondition' -- A
    and
    self.constraint.constrainedElement->size() = 1 -- B
    and
    self.constraint.constrainedElement->any(true).oclIsKindOf(BehavioralFeature) -- C
    and
    self.constraint.constrainedElement->any(true) -- D
                            .oclAsType(BehavioralFeature).owner->size() = 1
    implies
            contextualClassifier =
                    self.constraint.constrainedElement->any().oclAsType(BehavioralFeature).owner
    and
    self.bodyExpression.type.name = 'Boolean'