形式手法とモデリング - AlloyAnalyzerを中心に

連載 :

2010年9月22日(水)

先ほど取り上げた仕様は、ごく簡単に、最低限の機能を記述したものでした。以下では、この仕様を拡張してみましょう。

以下の仕様追加を行ないます。

ロール（Role）の階層関係を表現するためには、以下のように記述します。

Alloy Analyzerには、汎化関係の記述もあります。しかし、今回のようなケースでは、汎化は使いません。

ただし、これだけではロールの階層構造がループしてしまます。例えば「経理課職員のスーパー・ロールが経理課職員」という状況が発生してしまいます。これを防ぐため、以下の記述を追加します。

r:RoleはRoleのアトムrを表します
e in Aと書いた場合、「eはAの要素である」ことを表します
no x:A | V(x)と書いた場合、通常の論理式では￢(∃ x:A.V(x))、つまりVを満たすAの要素はないことを表わします
^は推移閉包（Transitive Closure）を表します。r.^superRolesは、rからsuperRolesをたどっていってたどり着ける、すべてのRoleの要素の集合を表します

上記の記述は、ロールrからsuperRolesをたどっていった時、その中にr自身が含まれることはない、という不変制約を表しています。

ユーザーへのロールの追加・削除、およびロールへの権限の追加・削除は、以下のように記述します。

predはPredicate、つまり述語を表しています。結果が真偽で表現される点が、述語の特徴です。機能を記述する際には、集合を返すものはfunで、真偽を返すものはpredを使って記述することになります。

上記の例では、rを事前条件としてのRole、r'を事後条件としてのRole、として考えます。addRoleでのu'.roles=u.roles+rは、「事後条件として、u'の持つrolesは、事前条件uの持つrolesにrを加えた集合」と読めます。

ロールを追加して削除した場合、操作前と操作後で同じロール構成になっていなければなりません。これを表すには、以下のように記述します。

assertは表明です。この表明は真である、と仮定されます。checkコマンドによって、反例を探索します。

all: 「すべての」を表す量化子。|の前に指定した変数すべてにおいて、|以下の述語が成り立つことを表します
disj: u,u',u''が同一アトムを示さないことを表します。Alloy Analyzerでは、この指定を行わなかった場合、uとu'が同じアトムの場合も含まれることになります
implies: 含意。「ならば」を表します

上記の例は、

ということを表します。

このようにして、仕様が正しいかどうかを確認していくことになります。

ここまでの完全な仕様は、以下の通りです。