可以将 UML 与 OCL 用于正式规范吗？答案

【问题标题】：Can UML with OCL be used for formal specifications?可以将 UML 与 OCL 用于正式规范吗？
【发布时间】：2023-04-02 02:53:02
【问题描述】：

我之所以这么问，是因为 UML 用于非正式规范，并且在语义上有一些歧义。然而，我认为 OCL 可以非常有效地用于指定前置/后置条件、不变量和其他约束。

我最近遇到了 Z 表示法和代数规范。我的问题是，UML 和 OCL 的组合足以满足正式规范吗？

【问题讨论】：

@Robert Harvey 单元测试很好，但它们不是正式规范，它们只能用于证明具体示例，而不是输入和输出的所有可能组合。

标签： uml modeling specifications ocl

【解决方案1】：

是的，对于您可以构建的大多数系统。

我的意思是，UML 和 OCL 只是半形式语言（它们的语法定义明确，但语义只是部分形式化，许多方面只是在标准文档规范中用自然语言描述）。因此，如果您正在构建一个关键系统并且您需要证明系统的正确性，那么 UML/OCL 可能会有所不足，但对于许多其他类型的系统，UML/OCL 可以提供的那种形式已经足够了

【讨论】：

谢谢，虽然您的回答以“是”开头，但结果似乎是“否”:) 您能否提供一些有用的语义变化示例？我的意思是，为什么不完全形式化 UML？
许多人尝试过将 UML 形式化，但都失败了（UML 太大太复杂）。他们最多只能通过用某种形式语言重新表达 UML 来形式化特定的子集。