OCL 发布条件是否可以位于 if then 语句中

Question

我是OCL的新手，我对前置和后置条件的工作原理有些怀疑。

是否可以将后置条件放在 if then 语句中？

例如，以下代码段是否有效，或者我只是混合了概念？

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

非常感谢您的帮助

Answer 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

Answer 2

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

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

Answer 3

简单的答案。不。完整的OCL帖子：申报是对行动的独立补充。

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

由于您的内部后置条件可以具体化为帮助程序操作的外部后置条件，因此 OCL 语法增强显然有机会允许与您建议的内容类似的东西。

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

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

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

但是，没有符号分析可以容纳所有可能的控制流，因此需要一个 oclAssert（expr，不变）包装器来帮助符号分析，断言返回的 expr 的局部不变性为真。类似的包装器可以支持您的使用，但您希望引发运行时故障，而不是承诺不可能发生危险。

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