代表合金分析仪中的条件语句

Question

我正在尝试使用Alloy表示条件（if-else）语句。我的理解是我需要使用Hoare三元组。但是，我在软件验证工具方面经验不足，也找不到任何在线软件演示工具来演示它。

Answer 1

条件语句的基本语法是implies：

 cond => expr [ else expr ]

您也可以使用：

 cond implies expr [ else expr ]

但是，请确保您了解隐含/ =>的逻辑规则。

这听起来很基础，您读过Daniel Jackson's book吗？您是否看过简单的示例，例如in the model repo？