合金新手在这里 .
我真的很喜欢在Alloy中创建约束并让分析器根据约束检查模型是否有效 .
但我问自己，“这些约束定义仅仅是精神体操，还是有助于构建更好的软件？”
我们来举一个具体的例子 . 在电子邮件客户端的地址簿模型中，可以定义此约束以将新条目添加到地址簿中：
新书b'中的地址映射等于旧书b中的地址映射，添加了从名称到地址的链接 . 该约束在Alloy中表示为：b'.addr = b.addr n-> a
那个好漂亮 .
但是当我在代码中实现添加操作时，我很难看到它的相关性 . 例如，我在Common Lisp中实现了add操作：
(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 set函数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的语言扩展用于约束编程
1 回答
我认为这个问题源于对像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的扩展，称为Alloy * [2]，它增加了在Alloy中解决更高阶约束的可能性（关系上的量化）可用于生成程序;执行操作并接受不同输入的实际代码（类似于add函数，根据模型） . 同样，这些程序用Alloy模型表示，并且需要（进行额外的努力）将这些模型转换成某种所需编程语言的程序 .
话虽如此，请注意，某些（验证）系统确实允许您将规范与代码混合，其中规范可能是：以与要执行的代码相同的方式编写（如验证/综合框架Leon [3]）;或者用不同的语言（来自可执行代码的语言）编写，而规范通过其他方式（如Dafny [4]中的注释）绑定到代码 .
[1] Kang，Eunsuk，et al . “基于模型的水处理系统安全分析 . ”第二届智能网络物理系统软件工程国际研讨会论文集 . ACM，2016年 .
[2] Milicevic，Aleksandar，et al . “Alloy *：一个通用的高阶关系约束求解器 . ”第37届软件工程国际 Session 论文集 - 第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：功能正确的自动程序验证器 . ”人工智能和推理编程逻辑国际 Session . 施普林格柏林海德堡，2010年 .