3

合金新手在这里。

我真的很喜欢在 Alloy 中创建约束并让分析器根据约束检查模型是否有效。

但我问自己，“这些约束定义仅仅是心理体操，还是有助于构建更好的软件？”</p>

让我们举一个具体的例子。在电子邮件客户端地址簿的模型中，可以定义此约束以将新条目添加到地址簿中：

新书 b' 中的地址映射与旧书 b 中的地址映射相同，但增加了从名称到地址的链接。该约束在合金中表示为： 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 集合函数adjoin将列表 ( na ) 添加到b。”</p>

该函数似乎正确地实现了一个简单的添加函数。我如何处理我在 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)

编写这样的代码似乎需要做很多工作，而且没有明显的好处。

所以我的问题是：在代码中实现合金模型时，我应该如何处理合金中定义的约束？

此外，是否有描述如何将合金模型转换为代码的教程，包括如何在代码中使用合金约束定义的描述？

谢谢你。

[1] 注意：我意识到 Common Lisp 中有一个名为 Screamer 的语言扩展，用于约束编程

4

1 回答 1

4

我相信这个问题源于对一些建模语言（如 Alloy）的目标和能力的轻微误解，并涉及形式化方法、验证和软件建模的一些基本方面。获得背景故事以使事情更清楚的可能很好的资源包括诸如计算微积分之类的书，以及您提到的有关合金的书。

约束是 Alloy 建模语言的一等公民。这个想法是约束反映了一个想要建模的代码的语义（并检查属性）。因此，从一个角度来看，Alloy 程序代表了代码本身，不需要编写额外的代码（例如用函数式语言）或将声明的约束与代码混合。但是，Alloy 程序不能直接执行；相反，它们只能用于根据此类程序（即约束集）生成模型。

更具体地说，b'.addr = b.addr + n->a在适当的解释下，Alloy 约束可能确实捕获了 Lisp 中添加操作的行为，因此检查涉及约束的某些属性对应于检查这些属性是否适用于 Lisp 中的给定操作。这是 Alloy 用于软件建模和验证的标准（并且可以说是预期的）用途。（此外，Alloy 经常用于对没有明确映射到程序的系统进行建模，例如某些类型的网络物理系统 [1]。）请注意，这当然意味着在 Alloy 中编写的模型必须正确建模手头的程序（就其语义而言），以便使属性检查有意义。

如前所述，Alloy 本身无法生成可执行代码（例如您给出的用 Common Lisp 编写的代码）。但是，有多种方法使用 Alloy 和 Alloy 生成的模型来生成代码片段或测试用例。（同样，根据手头的具体程序。）此外，Alloy 的一个扩展，称为 Alloy* [2]，它增加了在 Alloy 内解决高阶约束（关系上的量化）的可能性，可用于生成程序；执行操作并接受不同输入的实际代码（类似于 add 函数，根据模型）。同样，此类程序用合金模型表示，并且需要（执行额外的努力）将这些模型翻译成某种所需编程语言的程序。

话虽如此，请注意某些（验证）系统确实允许您将规范与代码混合，其中规范可能是：以与要执行的代码相同的方式编写（如验证/综合框架 Leon [3] ); 或以不同的语言编写（与可执行代码的语言不同），而规范通过其他方式绑定到代码（如 Dafny [4] 中的注释）。

[1] 康、恩淑等人。“基于模型的水处理系统安全分析。” 第二届智能信息物理系统软件工程国际研讨会论文集。ACM，2016 年。

[2] 米利切维奇、亚历山大等人。“Alloy*：一种通用的高阶关系约束求解器。” 第 37 届国际软件工程会议论文集 - 第 1 卷。IEEE 出版社，2015 年。

[3]布兰克、雷吉斯等人。“Leon 验证系统概述：通过转换为递归函数进行验证。” 第四届 Scala 研讨会论文集。ACM，2013 年。

[4] Leino, K. Rustan M. “Dafny：功能正确性的自动程序验证器”。国际编程人工智能和推理逻辑会议。施普林格柏林海德堡，2010。

于 2016-09-06T23:47:10.173 回答