Alloy 中的真假

Question

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

_{顺便说一句，我想要 true 和 false 的原因是我正在编写生成 .als 文件的东西。我的顶级 .als 文件期望我自动生成的 .als 文件定义一个 wellformed 谓词和一个 faulty 谓词。有时这些谓词很复杂，但有时我只想wellformed[...]到returntrue，faulty[...]到returnfalse。这就是为什么我想要 Alloy 语言中的 true 和 false。}

Answer 1

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

似乎有效；但最好内置这些。

Answer 2

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

pred true {}
pred false { not true }

Answer 3

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