2

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

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

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

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

非常感谢您的帮助

4

3 回答 3

3

我会将其重写为：

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
于 2013-10-27T13:33:16.470 回答
1

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

context k 
inv
(k.count=0)implies(k.status='nothing')
于 2015-07-07T14:50:11.863 回答
0

简单的回答。不，完整的 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

于 2022-02-20T21:09:53.197 回答