合金中的真假答案

【问题标题】：True and False in Alloy合金中的真假
【发布时间】：2016-01-25 18:06:40
【问题描述】：

Alloy 有很多逻辑连接词，例如 and 和 or 和 implies。但我找不到true 和false。他们失踪了吗？目前，我一直在使用 1=1 和 1=0，但这相当 hacky（并给出编译器警告）。

顺便说一句，我想要true 和false 的原因是我正在写一些产生.als 文件的东西。我的顶级.als 文件期望我的自动生成的.als 文件定义一个wellformed 谓词和一个faulty 谓词。有时这些谓词很复杂，但有时我只想让wellformed[...] 返回true，而faulty[...] 返回false。这就是为什么我想要使用 Alloy 语言的 true 和 false。

【问题讨论】：

标签： alloy

【解决方案1】：

它们没有内置是有充分理由的：请参阅软件抽象第 137 页的常见问题解答（Daniel Jackson，麻省理工学院出版社，2012 年）。简而言之，如果它们是内置的，您必须能够在布尔值上声明一个关系，然后因为布尔表达式可以计算为 {} 和 {T,F}，连接词需要是对这些值进行定义，这似乎是一个非常糟糕的主意。

【讨论】：

我买了你的书来跟进这个评论！（好吧，我也出于其他原因想要它。）这是一个有趣的问题。我仍然不太相信可以使用 2 元合取和析取运算符，但是 not 可以使用 0 元合取和析取运算符（因为这基本上就是 true 和 @ 987654322@ 是）。我想当你开始需要布尔值变量时问题就来了。

【解决方案2】：

由于空谓词为真，我最喜欢的真假实现是：

pred true {}
pred false { not true }

【讨论】：

【解决方案3】：

pred true {no none}
pred false {some none}

似乎有效；但是如果有这些内置就好了。

【讨论】：