12.7 前置条件

前置条件是一个可以链接到分类符的一个操作的约束。前置条件的目的是规定操作执行前必须满足的条件。前置条件包含一个类型为布尔的OCL表达式。在操作开始执行时该表达式必须计算为真，但它只约束于将要执行该操作的实例。

UML元模型中前置条件的位置如图12.3所示（译者注：原文是图12.4，是错误的）。如下的良构规则必须要满足。该规则还定义了上下文分类符的值。

图12.3 An OCL ExpressionInOcl used as a pre- or postcondition

12.7.1 良构规则

[1] 该约束具有泛型«precondition» (A)，并且只附加到一个模型元素(B)，且该模型元素是一个行为特征(C)，该行为特征有一个属主(D)。上下文分类符是该约束所附加到的操作的属主，且OCL表达式的类型必须是布尔。

context Expression
inv: self.constraint.stereotype.name = ‘precondition’                         -- 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(true)
                    .oclAsType(BehavioralFeature).owner
            and
            self.bodyExpression.type.name = ‘Boolean’

[2] @pre不允许用在前置条件约束中。

context ExpressionInOcl
inv: --

12.7.2 后置条件

与前置条件类似，后置条件是一个可以链接到分类符的一个操作的约束。后置条件的目的是规定操作执行后必须满足的条件。后置条件包含一个类型为布尔的OCL表达式。在操作开始执行后该表达式必须计算为真，但它只约束于刚好执行完该操作的实例。在一个使用了后置条件的OCL表达式中，“@pre”可以用来标识前置条件时刻的值。如果该操作有返回值的话，变量result指示操作的返回值。

UML元模型中后置条件的位置等同与前置条件，如图12.3所示（译者注：原文是图12.4，是错误的）。如下的良构规则必须要满足。该规则还定义了上下文分类符的值。

12.7.3 良构规则

[1] 该约束具有泛型«postcondition» (A)，并且只附加到一个模型元素(B)，且该模型元素是一个行为特征(C)，该行为特征有一个属主(D)。上下文分类符是该约束所附加到的操作的属主，且OCL表达式的类型必须是布尔。

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(true)
                    .oclAsType(BehavioralFeature).owner
            and
            self.bodyExpression.type.name = ‘Boolean’

12.7 前置条件