合金新手在这里。
我真的很喜欢在Alloy中创建约束并让分析器根据约束检查模型是否有效。
但是我问自己：“这些约束定义仅仅是心理体操，还是它们将有助于构建更好的软件？”
让我们举一个具体的例子。在电子邮件客户地址簿的模型中，可以定义此约束以在地址簿中添加新条目：
新书b’中的地址映射等于地址
在旧书b中进行映射，并添加来自
地址的名称。此约束在Alloy中表示为：
b'.addr = b.addr + n-> a
那个好漂亮。
但是，当在代码中执行添加操作时，我很难看到它的相关性。例如，我在Common Lisp中实现了添加操作：
(defun add (b n a)
"Add a new entry, (n a), to address book b"
(adjoin (list n a) b :key #'first))
换句话说：“这是一个名为add的函数的定义，该函数具有三个参数：b，n和a（书，名称，地址）。使用Common Lisp设置函数adjoin将列表（n a）添加到b。”
该功能似乎正确实现了一个简单的添加功能。
如何处理我在Alloy中定义的约束？我是否应该编写其他代码来表达约束？用伪代码：[1]
(defun add (b n a)
"Add a new entry, (n a), to address book b"
(adjoin (list n a) b :key #'first)
Check that nothing has changed in the
address book except that it now has
a n->a mapping)
编写此类代码似乎需要大量工作，并且没有明显的好处。
所以我的问题是：在代码中实现Alloy模型时，应如何处理Alloy中定义的约束？
另外，是否有教程描述如何将Alloy模型转换为代码，包括如何在代码中使用Alloy约束定义的描述？
谢谢。
[1]注意：我意识到在Common Lisp中有一个名为Screamer的语言扩展用于约束编程。
最佳答案
我认为，这个问题源于对一些建模语言（例如Alloy）的目标和功能的轻微误解，并涉及了形式化方法，验证和软件建模的一些基本方面。可能的有用资源，可以使背景故事更加清晰，包括Calculus of Computation之类的书，以及您提到的book about Alloy。
约束是Alloy建模语言的一等公民。这个想法是约束反映了人们想要建模（并检查属性）的代码的语义。因此，从一个角度看，Alloy程序代表代码本身，不需要编写其他代码（例如，以功能语言编写）或将声明的约束与代码混合。但是，Alloy程序不能直接执行。相反，它们只能用于根据此类程序（即约束集）生成模型。
更具体地说，Alloy约束b'.addr = b.addr + n->a在适当的解释下可能确实捕获了Lisp中add操作的行为，因此检查涉及该约束的某些属性对应于检查这些属性是否对Lisp中的给定操作成立。这是Alloy用于软件建模和验证的标准（并且可以说是预期的）用途。 （此外，Alloy通常用于对没有明确映射到程序的系统进行建模，例如某些类型的网络物理系统[1]。）请注意，这当然意味着必须在Alloy中编写的模型必须正确建模程序（就其语义而言），以便使属性检查有意义。
如前所述，Alloy本身无法生成可执行代码（例如，您使用Common Lisp编写的代码）。但是，有多种方法使用Alloy和Alloy生成的模型来生成代码或测试用例的片段。 （同样，根据手头的具体程序。）此外，可以使用称为Alloy * [2]的Alloy扩展来生成解决Alloy中更高阶约束（关系量化）的可能性；执行该操作并接受不同输入的实际代码（根据模型，类似于add函数）。同样，此类程序用Alloy模型表示，并且需要（执行额外的工作）将这些模型转换为某种所需编程语言的程序。
话虽如此，请注意，某些（验证）系统确实允许您将规范与代码混合，其中规范可能是：以与要执行的代码相同的方式编写（例如在验证/综合框架Leon [3]中） ）;或以不同的语言（与可执行代码的语言）编写，而规范则通过其他方式（例如，Dafny [4]中的注释）绑定到代码。
[1]姜恩淑等。 “水处理系统的基于模型的安全性分析。”第二届智能网络物理系统软件工程国际研讨会论文集。 ACM，2016年。
[2] Milicevic，Aleksandar等。 “合金*：通用的高阶关系约束求解器。”第37届软件工程国际会议论文集1. IEEE出版社，2015年。
[3] Blanc, Régis, et al. "An overview of the Leon verification system: Verification by translation to recursive functions." Proceedings of the 4th Workshop on Scala. ACM, 2013.
[4] Leino，K. Rustan M.“ Dafny：功能正确性的自动程序验证器。”人工智能和推理编程逻辑国际会议。施普林格·柏林·海德堡，2010年。
关于modeling - Alloy中定义的约束如何产生更好的软件？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/39309422/