Alloy (specification language) とは

コンピュータサイエンスとソフトウェアエンジニアリングでは、合金システムは複雑な構造上の制約と動作を表現するための宣言的な仕様言語です。 Alloyは、一次ロジックに基づくシンプルな構造モデリングツールを提供します。合金は、自動的に正確性をチェックできるマイクロモデルの作成をターゲットにしています。合金仕様は、合金アナライザを使用して確認できます。
合金は自動解析を念頭に置いて設計されていますが、合金は無限モデルの定義を可能にする点でモデル検査用に設計された多くの仕様言語とは異なります。 Alloy Analyzerは、無限のモデルでも有限範囲のチェックを実行するように設計されています。
Alloy言語とアナライザーは、米国のマサチューセッツ工科大学のDaniel Jacksonが率いるチームによって開発されています。