OCL Post 条件可以在 if then 语句中吗？答案

【问题标题】：Can an OCL Post condition be inside an if then statement?OCL Post 条件可以在 if then 语句中吗？
【发布时间】：2013-10-20 13:18:29
【问题描述】：

我是 OCL 的新手，我对前置条件和后置条件的工作方式有些疑问。

后置条件可以放在 if then 语句中吗？

例如，下面这段代码是有效的还是我只是在混合概念？

Context [some context here]
if ( 
... some conditions...
) then ( 
result = 1
post: self.isComplete() -- for example
)
endif

非常感谢您的帮助

【问题讨论】：

标签： ocl post-conditions

【解决方案1】：

我会改写为：

Context MyContext :: Integer
    post :
        if <some condition>
        then
            result = 1
        endif

如果您需要更多条件，您可以这样做：

Context MyContext :: Integer
    post :
        if <some condition>
        then
            -- Another condition
            if self.isComplete()
            then
                result = 1
            else
               result = 0
            endif
        else
            result = 0
        endif

【讨论】：

谢谢你的回答莫斯，这就是我在我的任务中遵循的方法；）

【解决方案2】：

您可以使用如下所示的隐含运算符：

context k 
inv
(k.count=0)implies(k.status='nothing')

【讨论】：

【解决方案3】：

简单的答案。不。完整的 OCL 帖子：声明是对操作的独立补充。

如果实际模型数据与 OCL 程序员的期望不兼容，则后置条件可能会失败。因此，如果您想要失败，那么您将进入 OCL 如何可靠且有效地失败的困难领域。见[1]。或者，如果您只是想要一个更复杂的控制流，请按照前面的答案中的说明进行重写。

由于您的内部后置条件可以被具体化为辅助操作的外部后置条件，显然有机会通过 OCL 语法增强来实现您所建议的内容。

当前工具对前置条件和后置条件的支持很差。 USE 有执行它们的选项，Eclipse OCL 没有；它们仅被解析为语法有效性。在运行时执行后置条件可能会非常昂贵和困难，因为@pre 最病态的使用可能需要整个系统状态的副本。

对于几次测试运行来说，昂贵的运行时执行可能是可以接受的，但您是否希望将其强加给您的最终用户？如果后置条件失败，这些用户该怎么办？

[1] 中描述的工作使用符号分析将评估迁移到编译时，确保遵守条件并且在使用额外时间时不会在运行时失败。

然而，没有符号分析可以容纳所有可能的控制流，因此需要一个 oclAssert(expr, invariant) 包装器来帮助符号分析，方法是断言返回的 expr 的局部不变量为真。一个类似的包装器可以支持您的使用，只是您想引发运行时故障而不是承诺不可能发生危险。

[1]http://www.eclipse.org/modeling/mdt/ocl/docs/publications/OCL2021Validity/OCLValidity.pdf

【讨论】：