我很难理解Alloy 4中谓词和函数之间的区别 . 我已经阅读了软件抽象中的4.5.2部分，但我仍然不清楚 . 有人可以帮我理解吗？
函数只是表示一个参数化表达式，它在每个调用站点都有内联 .
谓词表示一个公式，即一个布尔表达式，所以在这个意义上它有点像一个返回布尔表达式的函数 . 另一个区别是，在Alloy中，您可以使用Alloy“run”和“check”命令“运行”和“检查”谓词 . 运行谓词指示Alloy查找该谓词所包含的模型，而检查谓词则指示Alloy检查是否存在该谓词不存在的模型 .
1 回答
函数只是表示一个参数化表达式，它在每个调用站点都有内联 .
谓词表示一个公式，即一个布尔表达式，所以在这个意义上它有点像一个返回布尔表达式的函数 . 另一个区别是，在Alloy中，您可以使用Alloy“run”和“check”命令“运行”和“检查”谓词 . 运行谓词指示Alloy查找该谓词所包含的模型，而检查谓词则指示Alloy检查是否存在该谓词不存在的模型 .