Alloyとは

Alloyとは、「ソフトウェアのモデル化のためのオープンソースの言語およびアナライザ」であり、「セキュリティホールの発見から電話交換ネットワークまで、幅広く応用」される。

Alloy is an open source language and analyzer for software modeling. It has been used in a wide range of applications, from finding holes in security mechanisms to designing telephone switching networks. - Alloy - Website

Alloyは、形式手法の困難さを克服するために、ある種の制約を仮定する代わりに表現力と自動検証能力を両立した「軽量形式手法（Lightweight Formal Method）」の一種である。

一般に、形式手法の言語としての表現力と自動検証能力はトレードオフの関係にある。要は便利な文法が用意されてる言語ほど、複雑で自動検証の計算コストが大変なことになる(ということらしい)

Alloyが仮定する「ある種の制約」は、小スコープ仮説と呼ばれる。

小スコープ仮説とは、「ほとんどのバグは小さな反例を持つ」というもの。要は、同値分割・境界値分析的な考え方で、「たいがい0とかnullを含む同値クラスでバグるでしょ？」というニュアンス。感覚的にはナットクできる。

この小スコープ仮説を仮定して、モデルの網羅的全通り検証の代わりに、適切な小スコープを設定して反例の有無を検証する。

「適切な小スコープ」とは、例えば「全ての配列のlengthが0,1,2の時にバグがないか探索する」というようなもん。lengthが任意の値の時にバグを探索するのはすごく大変だが、0,1,2ならサクッと計算できる。

なお、Alloyの開発環境は特にAlloy Analyzerと呼ばれる。

環境構築

Alloyのダウンロードサイトから実行ファイルをダウンロードする。WindowsとLinuxの場合はalloy.4.2.jarを、OS Xの場合はalloy4.2.dmgを選択する。（なお、現在(2017/4/30)ダウンロード可能な最新バージョンは4.2である。）

alloy4.2.jar Alloy 4.2 (platform independent). Requires Java 6.
alloy4.2.dmg Alloy 4.2 (for OS X). Requires Java 6.

ダウンロードしたファイルを任意のディレクトリに格納すれば、インストール完了である。

Hello World!

Alloy 起動

ダウンロードしたalloy4.2.jarをダブルクリックすると、Alloyが起動する。なお、javaと拡張子jarとの関連を設定していない場合は、コマンドプロンプト（又はshell）でjava -jar alloy4.2.jarを入力すると起動できる。

ファイル作成

Alloyのエディタ内に以下のコードを記述する。

今回の例では、「1つのディスプレイに表示したただ1つのコンソール上に1つの"Hello World!"というメッセージを表示する」ような状況をモデル化する。

なお、Alloyの文法はEBNF形式で定義されており、Alloy Grammarサイトで閲覧できる。

/**
 * 
 * Hello World のモジュール
 * 
 */
module sample/HelloWorld

//=====================================================
//
// シグニチャ
//
//=====================================================

/** ディスプレイ */
one sig Display {
    console : one Console
}
one sig Console {
    message : some Message
}

/** メッセージ */
abstract sig Message {}

/** Hello World */
sig HelloWorld extends Message {}

//=====================================================
//
// 事実
//
//=====================================================

/** 全てのメッセージはコンソールに表示される */
fact {
    all m : Message | m in Console.message
}

//=====================================================
//
// 実行
//
//=====================================================
pred show{}
run show

モジュール宣言
- 一行目のmodule sample/HelloWorldはモジュールの宣言である。モジュールは、Alloyを構成する最大単位であり、複数のモジュールを連接させてモデルを構成する。
- この例では、sampleがJavaで言うとパッケージ名で、HelloWorldがJavaで言うとクラス名に相当する。
コメント
- コメントの書き方は、Javaと同様である。
シグニチャ
- シグニチャは、Javaで言うとクラスに相当する概念。
- ただし、Alloyでは１つのモジュール内に複数のシグニチャが含まれる。
- シグニチャ宣言は、簡単には<sigQual> sig <name> {<decl>}と記述される。
- <sigQual>はシグニチャの数やアクセスを示す修飾子である。
- oneはシグニチャが１つしかないこと（つまりJavaで言うとシングルトンのこと）を示す修飾子であり、abstractは実体を持たない抽象的なシグニチャであることを示す修飾子である。
- <name>はシグニチャの名前を指す。<decl>はシグニチャの定義であり、Javaで言うとメンバ変数を定義する。
- ただ1つのDisplayシグニチャは、ただ1つのConsoleシグニチャを有するものとして定義される。すなわち、1つのディスプレイ上にコンソールがただ1つだけ表示されている状態をモデル化する。
- ただ1つのConsoleシグニチャは、0個以上のMessageシグニチャを有するものとして定義される。すなわち、1つのコンソール上に1つ以上のメッセージが表示される状態をモデル化する。
- Messageシグニチャは、抽象シグニチャである。すなわち、様々なメッセージを抽象化した抽象シグニチャである。
- HelloWorldシグニチャは、Messageシグニチャを継承extendsした具象シグニチャである。すなわち、コンソール上に表示されるHello World!をモデル化したシグニチャである。
事実
- 事実は、シグニチャが満たすべき条件を列挙したものである。
- 「全てのメッセージはコンソールに表示される」という事実は、全てのメッセージ（all m : Message）が、コンソールに含まれる（in）なければならない（m in Console.message）ことを示す。
実行
- 実行関数（pred show{}）を定義して、実行（run show）することにより、モデルを検証する。

実行

メタモデル表示

Show アイコンをクリックして、メタモデルを表示する。メタモデルとは、Alloyモデルの静的構造を示したクラス図のようなものである。シグニチャの包含関係及び継承関係を表現する。

メタモデルを通じて、ディスプレイ、コンソール、メッセージ及びHello World!のシグニチャの包含関係や継承関係を確認する。

実行結果表示

Executeアイコンをクリックして、検証する。検証結果はAlloyで定義したモデルを満たすインスタンス例として表現される。

今回の例では、Hello Worldをただ1つだけ表示する場合と2つ表示する場合が出力された。これは、モデル上でコンソールに表示するHello Worldの数を規定しなかったためである。

1つのディスプレイ上のただ1つのコンソールにHello Worldが1つだけ表示される場合

1つのディスプレイ上のただ1つのコンソールにHello Worldが2つ表示される場合

このように、とくに検証方法を指定しなくても、Alloyは不具合を作り込みがちな境界条件や同値クラスを優先的に検証して表示する。

Alloy入門