合金（規格語言）

在計算機科學和軟件工程中，合金是一種聲明性的規範語言，用於在軟件系統中表達複雜的結構約束和行為。合金提供了基於一階邏輯的簡單結構建模工具。合金的目標是創建微型模型，然後可以自動檢查其正確性。合金規格可以使用合金分析儀檢查。

儘管合金是考慮到自動分析的設計，但合金與設計用於模型檢查的許多規範語言不同，因為它允許無限模型的定義。合金分析儀旨在即使在無限型號上進行有限的示波器檢查。

合金語言和分析儀是由美國馬薩諸塞州理工學院丹尼爾·傑克遜（Daniel Jackson）領導的團隊開發的。

歷史和影響

合金語言的第一個版本出現在1997年。這是一種相當有限的對象建模語言。該語言的隨後迭代“添加了量化詞，更高的Arity關係，多態性，亞型和簽名”。

該語言的數學基礎受Z符號的影響很大，合金的語法更多地歸功於諸如對象約束語言之類的語言。

合金分析儀

合金分析儀是專門開發的，以支持所謂的“輕量級形式方法”。因此，它旨在提供完全自動化的分析，與與合金類似的規範語言使用的交互式定理證明技術相比。分析儀的開發最初是受模型檢查器提供的自動分析的啟發。但是，模型檢查不適合通常在合金中開發的模型，因此，分析儀的核心最終被作為在布爾值SAT求解器上建立的模型 - 框架實現。

通過版本3.0，合金分析儀通過基於現成的SATSOLVER的基於SAT的積分模型 - 模型。但是，從4.0版開始，分析儀利用了Kodkod模型 - 芬德，為此，分析儀充當前端。這兩個模型引導者本質上都將以關係邏輯表達的模型轉換為相應的布爾邏輯公式，然後在布爾公式上調用一個現成的sat-solver。如果求解器找到解決方案，則將結果轉換為關係邏輯模型中變量的相應結合。

為了確保模型調查問題是可決定的，合金分析儀對由用戶定義的有限對像數量組成的限制範圍進行模型調查。這具有限制分析儀產生的結果的一般性的作用。但是，合金分析儀的設計師通過對小範圍假設的呼籲在有限範圍內工作的決定是合理的：可以通過測試在某些小範圍內的所有測試輸入的程序來找到大量的錯誤。

模型結構

合金模型本質上是關係的，由幾種不同類型的陳述組成：

• 簽名通過創建新集合來定義模型的詞彙

sig Object{}定義一個簽名對象

sig List{ head : lone Node }定義了一個簽名列表，其中包含一個類型節點的字段頭和多重性lone-這確立了列表s和節點S之間的關係的存在，因此每個列表與一個不超過一個頭節點相關聯

• 事實是假定始終保持的約束
• 謂詞是參數化的約束，可用於表示操作
• 功能是返回結果的表達式
• 斷言是關於模型的假設

由於合金是一種聲明性的語言，因此模型的含義不受陳述順序影響。