Alloy 例題: グローバルIDのモデリング
※本記事は プロパティベーステストの前にモデルをAlloyで検証する で触れたAlloyによるモデリング方法を前提としています。
Alloyの参考書に抽象によるソフトウェア設計 ―Alloyではじめる形式手法があります。この本では1ページにも満たない短いサンプルが数理論理学などの記号を使わずに丁寧に解説されているのですが、いかんせんAlloyの特徴が一通り詰め込まれているため、ChatGPTを活用しても理解に一苦労します。それと題材がITではないので、ITシステムのモデリングへの応用方法がわかりにくいです。
そこでまず、大抵のシステムで使われるグローバルIDの簡単なモデリングをやってみることにします。グローバルIDでなくてもID全般に応用できると思います。
グローバルIDの仕様
グローバルIDの仕様を以下の通りとします。いずれも一般的な仕様です。
- IDは整数とする
- すべてのIDは重複しない
- 各IDは一つのインスタンスにのみ割り振る。複数のインスタンスで同じIDを共有しない
Alloyは文字列などの具体的な値を扱いませんが、整数は用意されています。実行時にはスコープの範囲に応じた数の様々な数値が生成されます。ただし、整数を使わなくてもシグネチャと制約の組み合わせで済むことが多いです。今回は仕様通りに整数型を使いますが、数値に頼らないほうが抽象化しやすいでしょう。
グローバルIDのシグネチャを定義する
では、グローバルIDを表すシグネチャをファイル GlobalID.als に定義します。
sig GlobalID {
number: Int
}
GlobalID は整数型のフィールド number を持ちます。いくつかインスタンスを生成させてみましょう。手っ取り早く確認するには次のコードが便利です。
pred show {}
run show
show は何も制約を記述しない空の述語です。 run show を実行すると、何ものにも縛られないインスタンスが生成されます。
今回は GlobalID のインスタンスと数値が 2 つずつ生成されました。 2 つの GlobalID はそれぞれ固有の数値を持ち、特に問題ありません。ただし、これはあくまで一例です。 "New" ボタンをクリックすると、新しいインスタンス (の組み合わせ) を生成できます。クリックのたびに生成されるので、何度も試してみてください。
何度も生成し直しても、この組み合わせはほとんど変わらないはずです。ただし、これを見てモデルに問題がないと判断するのは早いです。というのは、デフォルトでは少数のインスタンスしか生成されないからです。もっと多様な組み合わせのインスタンスを生成するには、 スコープ の範囲を広げる必要があります。スコープはインスタンスの探索範囲を限定する要素で、生成されるインスタンスの数と組み合わせはスコープの大きさに比例します。デフォルトは 4 です。
スコープの範囲は run コマンドの for オプションで指定できます。適当に 7 まで広めてみましょう。以下のコードを実行し、 "New" ボタンを何度もクリックして様々なインスタンスを生成して確認してみてください。
run show for 7
何度かインスタンスを生成すると、次の組み合わせが見つかりました。
GlobalID の 2 つのインスタンスが 1 つの数値を共有してしまっています。
ファクトで制約を課す
GlobalID のインスタンスが固有の整数を持つように、ファクトを定義して制約を課しましょう。ファクトは述語と異なり、記述した制約は常に適用されます。
fact {
all g1, g2: GlobalID | g1.number != g2.number
}
たった一行ですが、いろいろ詰まっているので一つずつ見ていきます。
| で区切られた式は内包表記と言い、変数のスコープを限定します。 | の前が変数宣言のリストで、 | の後にそれらの変数を使った式 (制約) を記述します。よって、変数 g1 と g2 はこの式でのみ参照できます。
!= はよくある否定の比較演算子です。 g1.number != g2.number は、 g1 と g2 の number フィールドは異なるべきという宣言です。つまり、 GlobalID のインスタンス間で number の値を共有してはいけないことになります。
そして先頭の all は限量子 (数量詞、量化子、量指定子とも呼ばれます) と言い、式の制約を満たすインスタンスの数を指定します。この式の場合だと、「すべてのインスタンス同士の組み合わせに対して g1.number != g2.number が成立すべき」となります。すべてのインスタンスを 2 つずつ比較していき、 1 つでも number が等しいケースがあれば反例 (制約を満たさない例) となります。
ファクトを定義したら、再び run show for 7 を実行して "New" で新しいインスタンスを生成して確認してください。
どうでしたか？以下のメッセージが表示されて失敗したのではないでしょうか？
このエラーは、 "There are no more satisfying instances." というメッセージの通り、制約を満たすインスタンスが見つからなかったことを示します。「すべてのインスタンス同士の組み合わせに対して g1.number != g2.number が成立すべき」という制約が間違っている可能性があるのでしょうか？
disj
実は「インスタンス同士の組み合わせ」に罠があります。Alloyが生成する組み合わせは 「同じインスタンスの組み合わせ」も含まれる のです。つまり、 g1.number != g2.number で比較される g1 と g2 が同じインスタンスであるケースが存在します。「同じインスタンスを比較したときに number フィールドが異なるべき」は当然成立しませんから、したがって「すべての組み合わせに対して成立すべき」も成立しません。
同じインスタンスの組み合わせを排除するには、変数宣言の前に disj キーワードを追加して「 異なる インスタンスの組み合わせ」を明示的に指定します。以下が変更後のコードです。
fact {
all disj g1, g2: GlobalID | g1.number != g2.number
}
この変更により、何度インスタンスを生成し直しても number が共有されることはなくなりました。
一般的なプログラミング言語では見かけない disj は "disjoint" の略です。 disjointは集合同士 (この場合は GlobalID の集合) が「交わりを持たない」または「互いに素」を意味します。「互いに素」とは、集合同士に共通部分がないことです。 disj g1, g2 は g1 の集合と g2 の集合に共通するインスタンスがないことを宣言します。 g1 と g2 は単体のインスタンスなのになぜ集合が出てくるのか？というと、「すべてのインスタンスという集合」に対する宣言だからです。
最終的なコード
最終的なコードを以下に示します。
sig GlobalID {
number: Int
}
fact {
all disj g1, g2: GlobalID | g1.number != g2.number
}
pred show {}
run show for 7
まとめ
以上でグローバルIDの基本中の基本となる仕様を定義できました。この定義により、システムのモデリング時にグローバルIDのインスタンスが予期しない形で散らばることを防げるようになります。
「こんな当然の仕様をいちいち定義する必要があるのか？面倒くさい」と思っても不思議ではありません。でも、小さな定義の積み重ねがモデルの矛盾を見つけるはずです。
Discussion