形式手法とモデリング - AlloyAnalyzerを中心に
2.3. モデリング・セッション1: 最小限の仕様を作る
今回、実際にモデリングする対象は、以下に示す、簡単なロール・ベース・アクセス制御（Role-Based Access Control: RBAC）の仕様です。
- 集合
- ユーザー（User）: ユーザー・アカウント
- ロール（Role）: ユーザーに割り当てられる役割。Administrator、Guestなど
- 権限（Permission）: 役割に割り当てられる権限。Read、Write、Read Writeなど
- ユーザーは、0以上のロールを持つ
- ロールは、0以上の権限を持つ
|
|
| 図3: RBACのクラス図（クリックで拡大） |
Alloy Analyzerでは、最初から一気に仕様を書き上げることは、あまり行ないません。まずは最小限の仕様を作成したうえで、検証を繰り返しながら仕様を追加していきます。
2.3.1. 集合の記述
最初はまず、最低限の仕様を作りましょう。
これだけです。
いくつかAlloy Analyzerのキー・ワードが出てきました。
- sig: Signatureの略です。集合を表します。sig User {}と記述すると、Userという名前の集合を記述したことになります。{}の中には、ほかの集合との関係を記述します。
- run: 述語（pred）を実行するコマンドです。{}の中に、例を出力する条件を記述します。
ここで実行（Executeボタン。Ctrl+Eでも可）すると、検証が実行されます（図4）。右側の結果から「Instance」のリンクをクリックすることで、インスタンスを確認できます（図5）。もしアトムが1つも表示されない場合は、次のインスタンスを表示しましょう。「Next」ボタンによって次のインスタンスを表示することができます。
|
|
| 図4: 実行（クリックで拡大） |
ここで、Alloy Analyzerの強力な機能である「Evaluator」を試してみましょう。「Evaluator」ボタンを押すことで、Evaluatorを開くことができます（図6）。
Evaluatorでは、任意のAlloy式を記述できます。これにより、インスタンスの内容を詳細に確認できます。
試しに、Userと記述すると、Userのアトムが出力されます。User+Roleと記述すると、UserとRoleの和集合が表示されます。
主な集合演算は、以下の通りです。
- A + B: 和集合
- A & B: 積集合
- A - B: 差集合
具体的に、入力して確認してみましょう。
|
|
| 図5: インスタンスの表示（クリックで拡大） |
|
|
| 図6: Evaluator（クリックで拡大） |
2.3.2. 関係の記述
先ほどの仕様には関係が記述されていません。このため、各アトム同士にはつながりがありません。以下では、関係を記述して、アトム同士のつながりを表現します。
関係は、上記の仕様のように、シグニチャの{}の中に記述します。
代表的な記述例は、以下の通りです。
- lone: 0または1
- one: 1
- set: 0以上
- some: 1以上
関係は、集合をつなぎます。これは、以下のように、テーブルとして表現できます（以下は、Alloy Analyzerの仕様ではありません。説明用の記述です）。
先ほどの仕様を実行して、インスタンスを表示してみましょう（図7）。
関係に対し、関係演算を行うことができます。ここでは、いくつかの関係演算を紹介します。
|
|
| 図7: 関係の表示（クリックで拡大） |
- → : アロー。集合同士に対して使い、新しい関係を作り出す
- . : ドット・ジョイン。2つの集合をジョインする
ドット・ジョインの動作には、注意が必要です。ドット・ジョインは、ジョインの左右で、対応する要素同士を消去するかたちで結び付けます。
上記の場合、roles.permsとすると、rolesの右側の要素Riと、permsの左側の要素Riのそれぞれ対応する要素が消去され、以下の集合ができることになります。
この動作さえ理解してしまえば、Alloy Analyzerの関係演算は、マスターしたも同然です。
2.3.3. 関数の定義
集合同士の関係が記述できたので、関係をたどって「あるユーザーの持つ権限の集合を取得する」関数を記述しましょう。
関数は、以下のように記述します。
- fun: 関数。「関数名 [引数]:集合 {本体}」の形式で記述する
上記の例では、あるUserのアトムuを引数として受け取り、uが持つロールにヒモ付いた権限の集合を返すことになります。
この関数も、Evaluatorで直接試すことができます。UserのアトムUser$0がインスタンスに存在するとしたとき、以下のようにEvaluatorで実行すると、結果として、権限の集合が得られます。
完成した仕様を、以下に示します。
分からないところは、どんどんEvaluatorに入力して試すことができます。簡単に実行できることが分かると思います。
