Alloy（仕様言語）

コンピュータサイエンスとソフトウェアエンジニアリング において、Alloyはソフトウェアシステムにおける複雑な構造的制約と動作を表現するための宣言型仕様言語である。Alloyは、一階述語論理に基づくシンプルな構造モデリングツールを提供する。^{[1] Alloyは、自動的に}正確性をチェックできるマイクロモデルの作成を目的としている。Alloyの仕様は、Alloy Analyzerを使用してチェックできる。

Alloy は自動分析を念頭に置いて設計されていますが、無限モデルの定義を許可するという点で、モデルチェック用に設計された多くの仕様言語とは異なります。Alloy Analyzer は、無限モデルでも有限スコープ チェックを実行するように設計されています。

Alloy 言語とアナライザーは、米国マサチューセッツ工科大学のDaniel Jackson 氏が率いるチームによって開発されました。

Alloy言語の最初のバージョンは1997年に登場しました。これはかなり制限されたオブジェクトモデリング言語でした。その後の言語の反復では「量指定子、高位関係、ポリモーフィズム、サブタイプ、シグネチャが追加されました」。^[2]

言語の数学的基礎はZ 表記法の影響を強く受けており、 Alloy の構文はObject Constraint Languageなどの言語の影響を大きく受けています。

Alloy Analyzer は、いわゆる「軽量形式手法」をサポートするために特別に開発されました。そのため、Alloy に似た仕様言語で一般的に使用される対話型の定理証明技術とは対照的に、完全に自動化された分析を提供することを意図しています。Analyzer の開発は、もともとモデル チェッカーによって提供される自動分析に触発されました。しかし、モデル チェッキングは Alloy で通常開発される種類のモデルには適していないため、Analyzer のコアは最終的にブール SAT ソルバー上に構築されたモデル ファインダーとして実装されました。^[1]

バージョン 3.0 まで、Alloy Analyzer には既製の SAT ソルバーに基づく統合 SAT ベースのモデル ファインダーが組み込まれていました。ただし、バージョン 4.0 以降では、Analyzer は Kodkod モデル ファインダーを利用し、Analyzer はフロントエンドとして機能します。両方のモデル ファインダーは基本的に、リレーショナル ロジックで表現されたモデルを対応するブール ロジック式に変換し、次にブール式で既製の SAT ソルバーを呼び出します。ソルバーがソリューションを見つけた場合、その結果はリレーショナル ロジック モデル内の対応する定数と変数のバインディングに変換されます。^[3]

モデル発見問題が決定可能であることを保証するために、Alloy Analyzer は、ユーザーが定義した有限個のオブジェクトで構成される制限されたスコープでモデル発見を実行します。これにより、Analyzer によって生成される結果の一般性が制限されます。しかし、Alloy Analyzer の設計者は、小さなスコープ仮説を主張して、限られたスコープ内で作業するという決定を正当化しています。小さなスコープ内のすべてのテスト入力に対してプログラムをテストすることで、高い割合でバグが見つかるという仮説です。 ^[4]

Alloyモデルは本質的にリレーショナルであり、いくつかの異なる種類のステートメントで構成されています。^[1]

• シグネチャは新しいセットを作成することでモデルの語彙を定義します

sig Object{}署名オブジェクトを定義する

sig List{ head : lone Node }Node型と単独多重度のフィールドヘッドを含むシグネチャListを定義します。これにより、 ListとNodeの間に関係が存在し、すべてのList が1 つのヘッドNodeに関連付けられます。

• 事実は常に成り立つと想定される制約である
• 述語はパラメータ化された制約であり、操作を表すために使用できる。
• 関数は結果を返す式です
• アサーションはモデルに関する仮定である

Alloy は宣言型言語であるため、モデルの意味はステートメントの順序によって影響を受けません。

• アロイのウェブサイト
• Alloy Githubリポジトリ
• 合金ガイド
• MIT の Kodkod 分析エンジン Web サイト
• Ecore の Alloy メタモデル