alloy - 合金4中函数和谓词的区别？

Question

我很难理解 Alloy 4 中谓词和函数之间的区别。我已经阅读了软件抽象中的第 4.5.2 节，但我仍然不清楚。有人可以帮我理解吗？

Answer 1

一个函数只是表示一个参数化的表达式，它在每​​个调用站点都被内联。

谓词表示一个公式，即一个布尔表达式，所以从这个意义上说，它有点像一个返回布尔表达式的函数。另一个区别是，在 Alloy 中，您可以使用 Alloy“运行”和“检查”命令“运行”和“检查”谓词。运行谓词会指示 Alloy 找到该谓词适用的模型，而检查谓词会指示 Alloy 检查是否存在该谓词不适用的模型。