Alloy

概述

是一种轻量级的、描述性的、面向对象的结构建模语言,灵感来自于Z规范语言和语义学方法的关系演算；

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

分析器

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

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

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

模型

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

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

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

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

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

安装

按照以下步骤

基本概念

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

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

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