Alloy（结构建模语言）

Alloy

结构建模语言

Alloy是一种轻量级的、描述性的、面向对象的结构建模语言,灵感来自于Z规范语言和语义学方法的关系演算。Alloy 是用于描述结构（structure）的语言，也是探索结构的工具。从发现安全机制的漏洞到设计电话交换网络，它已被广泛用于各种应用中。

概述

Alloy的基本思想：在语言上，所有的值都是有联系的，它可以表达所有数据类型的关系，包括集合、标量和元组；适用范围广泛，例如发现漏洞的安全机制、设计电话交换网络等等。

分析器

是由MIT软件设计组开发的，主要功能是进行模型检验，是基于模型检测理论的模型分析工具。

模型检验是一种形式化验证方法，验证过程通常是通过使用模型检验算法表明特定属性的可满足性来实现的。

Alloy分析器所使用的建模语言为Alloy。

模型

包括一个或多个文件，每个文件包含一个单独的模块(module).

一个模块包括三个部分，用于标识该模块的头部，若干导入，以及若干段落：module::=header import* paragraph*

模块中的段落可以是签名、事实、函数、谓词、断言，以及运行命令、检查命令：

paragraph::=sigDecl| factDecl| funDecl| predDecl| assertDecl| runCmd| checkCmd

Alloy分析器在有限界限内自动地寻找一个模型的实例。因为搜索是有界限的，所以有可能虽然存在一个实例，但是搜索失败。不过被搜索到的实例一定是合法的实例。

基本概念

签名（sig）用于表示集合，在分析过程中，可以指派具体的取值，扮演的角色类似编程语言中的静态变量。

事实（fact）、函数（fun）和谓词（pred）都用于表示约束。

all 和 some 的行为就像谓词逻辑中的全称量词和存在量词。

参考资料

1.Alloy 结构描述语言·开源中国社区