【发布时间】：2020-03-07 02:58:55
【问题描述】：
我正在尝试使用合金来表示条件（if-else）语句。我的理解是我需要使用 Hoare 三元组。但是，我对软件验证工具没有太多经验，也找不到任何演示它的在线教程。
【问题讨论】：
标签： conditional-statements software-design alloy formal-verification
【发布时间】：2020-03-07 02:58:55
【问题描述】：
条件语句的基本语法是implies：
cond => expr [ else expr ]
你也可以使用：
cond implies expr [ else expr ]
但是，请确保您了解蕴含/=> 的逻辑规则。
这听起来相当基础的程序；你读过Daniel Jackson's book吗？你看过简单的例子吗，例如in the model repo？
【讨论】：
-
感谢您的回答。是的，我发现了这本书，并且一直在浏览。再次感谢