在Software Abstractions一书中没有提到enum。
我见过人们在Alloy模型中使用enum，显然它是由Alloy工具支持的。
我猜测在旧版本的Alloy中，enum关键字是该语言的一部分，支持enum的代码已经忍受了，尽管enum已被删除。我猜对了吗？
不，恰恰相反：在本书出版后，enum被添加到语言中。
这些是本书出版后添加的功能。它们都非常有用。
seq - 列表。不幸的是，他们缺少一个字面意思，这使得它们很难使用。let - 可以在谓词，函数或事实之外使用的宏。对于常量和其他小函数非常有用。不要求类型使它们更容易阅读，但错误报告是令人沮丧的。meta - 访问规范中的字段和类型的可能性。非常好，如果你有反思。初学者应该避免。private - 私有命名空间，对更大的规范非常有用。unsat - 允许您在没有解决方案时调试规范。促进使用小事实而不是分组。quick guide中描述了这些新功能