概述
是一種輕量級的、描述性的、面向對象的結構建模語言,靈感來自於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 的行為就像謂詞邏輯中的全稱量詞和存在量詞。
