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

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

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

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

包括一个或多个档案，每个档案包含一个单独的模组(module).

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

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

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

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

按照以下步骤

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

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

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