概述
Alloy的基本思想：在語言上，所有的值都是有聯系的，它可以表達所有數據類型的關系，包括集合、标量和元組；适用範圍廣泛，例如發現漏洞的安全機制、設計電話交換網絡等等。
分析器
是由MIT軟件設計組開發的，主要功能是進行模型檢驗，是基于模型檢測理論的模型分析工具。
模型檢驗是一種形式化驗證方法，驗證過程通常是通過使用模型檢驗算法表明特定屬性的可滿足性來實現的。
Alloy分析器所使用的建模語言為Alloy。
模型
包括一個或多個文件，每個文件包含一個單獨的模塊(module).
一個模塊包括三個部分，用于标識該模塊的頭部，若幹導入，以及若幹段落：module::=header import* paragraph*
模塊中的段落可以是簽名、事實、函數、謂詞、斷言，以及運行命令、檢查命令：
paragraph::=sigDecl| factDecl| funDecl| predDecl| assertDecl| runCmd| checkCmd
Alloy分析器在有限界限内自動地尋找一個模型的實例。因為搜索是有界限的，所以有可能雖然存在一個實例，但是搜索失敗。不過被搜索到的實例一定是合法的實例。
基本概念
簽名（sig）用于表示集合，在分析過程中，可以指派具體的取值，扮演的角色類似編程語言中的靜态變量。
事實（fact）、函數（fun）和謂詞（pred）都用于表示約束。
all 和 some 的行為就像謂詞邏輯中的全稱量詞和存在量詞。
