主要观点：

• 在 Alloy 中，事实（fact）常用于缩小问题范围、排除无意义情况、优化慢模型、定义 Alloy 无法原生表达的必要关系等，但初学者易将其用于建模系统而导致问题。
• 应使用谓词（predicate）来明确约束，而非事实，谓词具有局部作用域等优点。
• 约束有风险，需要错误状态来检查程序是否避免错误状态。

关键信息：

• 在 Alloy 中通过不同方式建模依赖树等，如 sig Package { depends_on: set Package } 等。
• 事实如 fact no_self_deps { all p: Package { p not in p.depends_on } } 可防止包自身依赖等情况，但可能使某些非法状态不可表示。
• 可通过细化（refinement）技术使无效状态在世界中可表示但在机器中不可表示。
• 事实的使用场景包括缩小问题范围（如仅指定包安装器时使用“无自依赖”事实）、排除无意义情况（如在链表建模中排除多余列表）、优化慢模型（通过对称破缺）、定义必要关系等。

重要细节：

• Alloy 有内置枚举但与语言其他部分不兼容。
• 模型检查器评估纯关系表达式比量化表达式快得多。
• 事实不会生成违反它的模型，也不会寻找不变量违反。
• 谓词可测试其为真或检查其对获取其他属性的必要性。
• 可通过开放模块（open）等方式优化代码结构。
• 有关于 Alloy 的书籍和参考文档，作者还在开展新的 Alloy 研讨会并通过 newsletter 更新。

引用：

1. 在其他规范语言中，这通常是运行时约束或对系统规范的直接修改。返回