"addFront" 函数看起来非常程序化（即非声明式）
The "addFront" function looks awfully procedural (i.e., not declarative)
在 Software Abstractions 一书的第 10 页，它强调了 Alloy 的声明性：
Alloy is declarative, and describes how to check whether a change of
state is valid, by comparing the before and after values.
第 9 页是添加新电子邮件地址簿的示例。该示例显示了 "add" 之后图书的状态与添加之前图书的状态有何不同。很好 - 确实非常明确！
第 135 页是参数化 "list" 模块的示例。该示例具有函数 "addFront":
fun List.addFront (e: t): List {
{ p: List | p.next = this and p.element = e } }
我觉得这不是很明确。为了声明，我希望参数列表包含前后列表，我希望代码显示 "addFront" 之后的列表状态与 [=27= 之前的列表状态有何不同]（就像书中的例子）。
为什么addFront是过程式写的？是不是违反了Alloy的声明性？
声明性的意思是（对我来说）不是解释计算是如何一步一步发生的，而是给出一个关于计算的观察。这就是这个函数的作用：它说如果你查看 addFront 的结果，你会发现它的 next 字段包含输入列表，它的 element 字段包含给定的元素。集合理解（结合规范化事实，在书中给出但此处未显示）表示 "return the list p such that ..."。
也许在这种情况下对您来说似乎是非声明性的是 Alloy 看起来非常像您在 ML 等函数式语言中的代码。但在我看来，该代码本质上也是声明性的——事实上，术语 "declarative" 已被广泛用于描述函数式语言。
我还应该指出，虽然 Alloy 确实是为支持声明式建模而设计的，而且我相信对于复杂的状态转换，声明式方法通常是最好的，但我认为这并不意味着必须更具操作性的描述形式有任何问题（参见 Pamela Zave 早期的 paper）。模型中的问题是存在对行为不重要的细节，但由于建模语言的弱点，或者因为建模者无意中引入了实现问题而被包含在内。
在 Software Abstractions 一书的第 10 页，它强调了 Alloy 的声明性：
Alloy is declarative, and describes how to check whether a change of state is valid, by comparing the before and after values.
第 9 页是添加新电子邮件地址簿的示例。该示例显示了 "add" 之后图书的状态与添加之前图书的状态有何不同。很好 - 确实非常明确！
第 135 页是参数化 "list" 模块的示例。该示例具有函数 "addFront":
fun List.addFront (e: t): List {
{ p: List | p.next = this and p.element = e } }
我觉得这不是很明确。为了声明，我希望参数列表包含前后列表，我希望代码显示 "addFront" 之后的列表状态与 [=27= 之前的列表状态有何不同]（就像书中的例子）。
为什么addFront是过程式写的？是不是违反了Alloy的声明性？
声明性的意思是（对我来说）不是解释计算是如何一步一步发生的，而是给出一个关于计算的观察。这就是这个函数的作用：它说如果你查看 addFront 的结果，你会发现它的 next 字段包含输入列表，它的 element 字段包含给定的元素。集合理解（结合规范化事实，在书中给出但此处未显示）表示 "return the list p such that ..."。
也许在这种情况下对您来说似乎是非声明性的是 Alloy 看起来非常像您在 ML 等函数式语言中的代码。但在我看来，该代码本质上也是声明性的——事实上，术语 "declarative" 已被广泛用于描述函数式语言。
我还应该指出，虽然 Alloy 确实是为支持声明式建模而设计的，而且我相信对于复杂的状态转换，声明式方法通常是最好的，但我认为这并不意味着必须更具操作性的描述形式有任何问题（参见 Pamela Zave 早期的 paper）。模型中的问题是存在对行为不重要的细节，但由于建模语言的弱点，或者因为建模者无意中引入了实现问题而被包含在内。