Alloy Analyzer で形式仕様記述
Alloy Analyzer で形式仕様記述
まずは簡単な事例で、Alloy で仕様を記述/検査する一通りの流れを説明します。

1. 題材

今回は、単純な「ボタン」の仕様を題材にします。

以下のようなボタンの仕様を考えています。
  • ボタン上にカーソルがないときは、ボタンは Normal 状態です。
  • マウスカーソルが上に来たら、ボタンは Over 状態になります。
  • ボタンが押されたら、ボタンは Press 状態になります。
  • ボタンは自身の幅と高さを管理しています。

ボタンは以下のイベントを受け取ります。
これらのイベントはいつでも送られてくる可能性があります。 
- mouse_move (x : Int, y : Int)      //マウス移動
- mouse_pressL (x : Int, y : Int)    //マウス左Press
- mouse_releaseL (x : Int, y : Int)  //マウス左Release
※ この仕様はかなり曖昧で不完全な仕様です。どういう曖昧さがあるのか、Alloy で形式的に仕様を書いていきながら確認してみましょう。


2. 状態空間の記述

では早速上記の仕様を Alloy で記述していきたいと思います。
Alloy に限らず形式的に仕様を記述する場合、まず最初に「状態空間」と「型」を定義します。
「状態空間」とは、対象のモデルが取りうるすべての状態の集合のことをいいます。
状態の集合は、変数の値の組み合わせで定義します。
「型」は、変数の値の取りうる範囲を定義するためのもので、集合で定義します。

このボタンの状態空間は、Alloy で以下のように記述することができます。 
enum Type {Normal, Over, Press}
sig Button {
	type : Type, 	//ボタンの種類
	width : Int, 	//ボタンの幅
	height : Int 	//ボタンの高さ
}

上から順番に説明します。

2.1. enum

enum A {a, b, c, ...}
と書くと、A という集合を定義することができます。
A の具体的な要素は a, b, c, ... になります。

今回はボタンの状態を表すために、具体的な要素が Normal, Over, Press の、Type という集合を定義しました。
この集合は　Button のところで型として使います。

2.2. sig

sig A {a, b, c, ...}
と書くと、A という集合を定義することができます。
A の各要素は、a, b, c, ... というパラメータを持っています。
sig で集合を定義した場合、enum と違って具体的に要素を指定できません。

今回はボタンを表すために、type, width, height というパラメータを持っている Button という集合を定義しています。
この Button の集合で、ボタンの状態空間を表すことにします。

2.2.1. パラメータ

sig のパラメータは 
名前 : 型
というフォーマットで定義します。

type の型は先ほど定義した Type です。type は Normal, Over, Press のいずれかの値になります。
width と height の型は Int です。Int は整数の集合を表します。
Int はあらかじめ Alloy で用意されている型で、自分で定義しなくても使えます。

2.3. コメント

必要に応じてコメントを記述することができます。
  • 一行コメント
//コメント
--コメント
  • 複数行コメント
/*
  コメント
*/


3. 状態空間の検査

状態空間が定義できたので、定義した状態空間を Alloy で検査してみます。

状態空間について検査したい項目は、以下の 2 つです。
  • 期待する状態が含まれているか?
  • 期待しない状態が含まれていないか?
検査する方法はいくつかありますが、今回は愚直に「目視」で検査してみます。
目視で検査するには、Alloy の「指定した論理式を満たす例を探す」機能を利用します。
ボタンが取りうる状態の例を探してもらって、その例が期待しているものかどうかを目視で確認します。

3.1. 検査コマンドの記述

ボタンが取りうる状態の例を探してもらうには、以下のように書きます。 
pred show {}
run show
これはどこに書いてもかまいません。適当に sig Button の下あたりに書いておくとよいでしょう。 

pred A {論理式}
と書くと、A という名前の論理式を定義することができます。
今回は特に探してもらう条件を指定しないので、論理式が空 (True) の show という名前の論理式を用意しました。 

run A
と書くと、A の論理式を満たす例を探してくれ。というコマンドを定義することができます。
今回は、何でもいいから例を見つけてくれ。というコマンドを定義しました。

3.2. 検査の実行

上記のように記述したコマンドを実行するには、メニューの [Execute] - [run show] を選択します。
選択すると、以下のように画面の右側に検査結果が表示されます。
Instance found. と表示されたので、何か例が見つかったようです。

3.3. 目視で検査

見つかった例を表示するには、画面上部の [Show] ボタンを押します。
以下のような画面が表示され、見つかった例が図で表示されます。

3.4. 表示のカスタマイズ

表示された内容の説明をする前に、表示を少しカスタマイズします。
enum で集合を定義すると、図で表示したときに enum の要素間に next, prev という矢印が表示されます。
この矢印はたいていの場合邪魔なだけなので、非表示にすることをお勧めします。

画面上部の [Theme] ボタンを押すと、以下のような画面になります。
ここで、左下の方の next と prev をそれぞれ選んで、左上の方の [Show as arcs] を 何度かクリックして off に変更してください。
それぞれ変更し終わったら、画面上部の [Close] ボタンを押してください。
これで邪魔な next と prev が消えます。

3.4.1. 表示内容の説明

表示された例が何を表しているのか説明します。
これは、Button0, Button1 という名前の、 Button 集合の要素が 2 個見つかったことを表しています。
Button0 の Type は Normal、width は 4、height は 7 です。
Button1 の Type は Over、width は 6、height は 3 です。
(Button とつながっていない Press は、とりあえずゴミだと思ってください。)

つまり、ボタンの状態空間には、少なくとも「幅 4, 高さ 7, Normal」、「幅 6, 高さ 3, Over」という 2 つの状態が含まれているということです。
これらの見つかった状態は、特におかしな状態ではないので問題なさそうです。

3.4.2. 他の例を探す

確認した例が問題なかったので、他の例も見てみます。
画面上部の [Next] ボタンを押すと、別の例を探して表示してくれます。
何度か [Next] ボタンを押しながら出てきた例を目視で確認していきます。

3.4.3. 期待しない状態

何度か [Next] ボタンを押していくと、以下のような状態が出てきました。
Button0 と Button1 の高さが -3 になっています。
これは期待していませんでした。幅と高さは 0 以上を想定していました。

3.5. 状態空間の修正

状態空間に期待しない状態が含まれていた場合、期待しない状態が含まれないように状態空間を修正します。

3.5.1. 不変条件の記述

期待しない状態を含まれないようにするには、「不変条件」を書きます。
「不変条件」とは、すべての状態で常に成り立っていなければならない条件のことです。
状態空間に期待する状態だけが必要十分含まれるように不変条件を追加します。

不変条件は以下のように記述することができます。 
sig Button {
	type : Type, 	//ボタンの種類
	width : Int, 	//ボタンの幅
	height : Int 	//ボタンの高さ
}
{
	width >= 0 && height >= 0
}
sig の後ろに「{ 論理式 }」を追加すると、その論理式が不変条件になります。
今回は「width と height は 0 以上である」という不変条件を追加しました。

3.5.1.1. 論理式の記述
論理式は以下のような演算子を組み合わせて記述します。
演算子 使い方 意味 結果の型
&& A && B A かつ B Bool
|| A || B A または B Bool
=> A => B A ならば B Bool
! ! A A ではない Bool
<=> A <=> B A と B は等しい (A, B がBoolの場合) Bool
= S = T S と T は等しい (S, T がBool以外の場合) Bool
!= S != T S と T は異なる (S, T がBool以外の場合) Bool
> x > y x は y より大きい Bool
>= x >= y x は y 以上である Bool
< x < y y は x より大きい Bool
<= x <= y y は x 以上である Bool
+ x + y x に y を足した値 Int
- x - y x から y を引いた値 Int
※A, B の型は Bool、S, T の型は Bool 以外、x, y の型は Int です。
他にも色々な演算子がありますが、必要に応じて順次紹介していきます。

3.5.1.2. 論理式のシンタックスシュガー
論理式は改行して書くこともできます。 
{
	width >= 0
	height >= 0
}
改行して書くと、各行を && で結んだ論理式と同じ意味になります。

3.5.2. 再度目視で検査

不変条件を追加したので、[Next] ボタンを何度か押しても先ほどのような期待しない状態が出てこなくなりました。
だいたい良さそうなので、状態空間はこれで完成とします。


4. 振る舞いの記述

状態空間が完成したので、この状態空間を使ってボタンの「振る舞い」を記述していきます。

「振る舞い」は、「どういう状態でどういうイベントを受け取ったら、どういう状態に変化するか」というように、事前の状態、イベント、事後の状態の 3 つの組み合わせで表現することができます。
このうち、事前の状態と事後の状態が何かを表す条件のことを、「事後条件」といいます。("事後"条件ですが、事前と事後の両方の状態に関わる条件です)
Alloy では、イベントと事後条件の 2 つの組み合わせで振る舞いを記述します。

4.1. マウス移動の振る舞い

まずは、「mouse_move (x : Int, y : Int)」イベントを受け取ったときの振る舞いを記述してみます。

4.1.1. 振る舞いの記述

Alloy で振る舞いを記述する場合、pred を使って以下のように記述します。 
pred イベント名 (イベント引数, 事前と事後の状態) {
	事後条件
}

今回のマウス移動の振る舞いの場合は、以下のようになります。 
pred mouse_move (x : Int, y : Int, b : Button, b' : Button) {
	事後条件
}
b が事前のボタンの状態、b' が事後のボタンの状態を表すことにします。
事後条件は、pred の引数で定義した x, y, b, b' を使って記述します。

4.1.2. 事後条件の記述

元の仕様を確認してみます。
  • ボタン上にカーソルがないときは、ボタンは Normal 状態です。
  • マウスカーソルが上に来たら、ボタンは Over 状態になります。

まずは 1 つ目の仕様を事後条件で記述してみます。
  • ボタン上にカーソルがないときは、ボタンは Normal 状態です。
とあるので、事後条件は「x, y が事前の状態のボタン上でなければ、事後の状態は Normal になる」と解釈します。
具体的には以下のようになります。 
pred mouse_move (x : Int, y : Int, b : Button, b' : Button) {
	! ((x >= 0 && x < b.width) && (y >= 0 && y < b.height)) => b'.type = Normal
}
sig の要素のパラメータの値を参照するには、「.」を使います。

同じようにして 2 つ目の仕様を記述してみます。
  • マウスカーソルが上に来たら、ボタンは Over 状態になります。
とあるので、事後条件は「x, y が事前の状態のボタン上だったら、事後の状態は Over になる」と解釈します。
具体的には以下のようになります。 
pred mouse_move (x : Int, y : Int, b : Button, b' : Button) {
	! ((x >= 0 && x < b.width) && (y >= 0 && y < b.height)) => b'.type = Normal
	((x >= 0 && x < b.width) && (y >= 0 && y < b.height)) => b'.type = Over
}

4.1.3. 振る舞いの検査

とりあえず元の仕様を Alloy で記述できたので、問題ないか検査してみます。
検査したい項目は以下の 2 つです。
  • 事後条件に期待する事前と事後の状態の組み合わせが含まれているか
  • 事後条件に期待しない事前と事後の状態の組み合わせが含まれていないか
やり方はいくつかありますが、今回は状態空間の検査でやったように「目視」で確認してみます。

4.1.3.1. 目視で検査
例を見つける検査コマンド run を使って以下のように書きます。 
run mouse_move
Execute すると Instance found になったので、Show で表示すると、以下のようなインスタンスが表示されました。
表示されているものが何か説明します。
Button1 が b、つまり事前のボタンの状態を表しています。
Button0 が b'、つまり事後のボタンの状態を表しています。
カーソルの座標 x は 0, y は 7 です。
事前のボタンの状態は、幅 7, 高さ 4, Over です。
事後のボタンの状態は、幅 1, 高さ 4, Normal です。

まとめると「幅 7, 高さ 4, Over の状態で mouse_move (0, 7) を受け取ったら、幅 1, 高さ 4, Normal の状態になる」という振る舞いが、先ほど書いた pred に含まれていることを表しています。

なぜか幅が狭くなっています。これは期待していません。
なぜ突然幅が狭くなってしまったのかというと、事後条件に条件が足りないからです。
Alloy では、「変わらないものは変わらない」という条件も明記する必要があります。
先ほど書いた事後条件には、mouse_move を受け取っても、事前と事後のボタンの幅と高さは変わらない。という条件を書いていませんでした。
よって、Alloy は変わってしまう例を見つけて表示したという訳です。

4.1.3.2. 振る舞いの修正
というわけで、幅と高さは変わらない。という条件を追加します。 
pred mouse_move (x : Int, y : Int, b : Button, b' : Button) {
	! ((x >= 0 && x < b.width) && (y >= 0 && y < b.height)) => b'.type = Normal
	((x >= 0 && x < b.width) && (y >= 0 && y < b.height)) => b'.type = Over


	b'.width = b.width
	b'.height = b.height
}

4.1.3.3. 論理式をまとめる
ボタン上かどうか判定する論理式が 2 カ所あって冗長です。
pred でボタン上かを判定する論理式を用意して、それを利用してシンプルに書くことができます。 
pred on_button (x : Int, y : Int, b : Button) {
	x >= 0 && x < b.width
	y >= 0 && y < b.height
}
「指定された x, y 座標は、指定されたボタン上である」という論理式を表す pred です。 

pred mouse_move (x : Int, y : Int, b : Button, b' : Button) {
	! on_button[x, y, b] => b'.type = Normal
	on_button[x, y, b] => b'.type = Over


	b'.width = b.width
	b'.height = b.height
}
用意した on_button を利用してシンプルに記述できました。
別の pred を使うときは、 
pred名 [引数, 引数, ...]
という構文です。

4.1.4. 再度検査

振る舞いを修正したので、再度検査してみます。
今度は以下のようなインスタンスが見つかりました。
これは「幅 7, 高さ 4, Normal の状態で mouse_move (4, 7) を受け取ったら、幅 7, 高さ 4, Normal の状態のまま変わらない」という振る舞いが、先ほど書いた pred に含まれていることを表しています。
今度は期待通りです。
なお、Button0 はゴミだと思ってください。

何度か Next を押して、他のインスタンスも確認してみます。
以下のようなインスタンスが見つかりました。
幅 1, 高さ 6, Press の状態で mouse_move (0, 4) を受け取ったら、幅 1, 高さ 6, Over の状態になるようです。
これは期待していませんでした。
Press 中にマウスを動かしたときの仕様を考慮していませんでした。

4.1.4.1. 振る舞いの修正
今回は「Press 中にマウスを動かしたとき、ボタン上であれば Press のまま、ボタン外に出たら Normal になる」という仕様にしたいと思います。
この仕様をもとに pred を以下のように修正しました。 
pred mouse_move (x : Int, y : Int, b : Button, b' : Button) {
	! on_button[x, y, b] => b'.type = Normal
 	on_button[x, y, b] => (b.type = Press => b'.type = b.type && b.type != Press => b'.type = Over)


	b'.width = b.width
	b'.height = b.height
}
移動後の位置がボタン内だった場合、元の type に応じて事後の type が変わるようにしました。
再度 run コマンドでいくつかインスタンスを確認しても期待しないケースが出てこないので、mouse_move の振る舞いはこれで OK とします。

4.1.4.2 シンタックスシュガー
on_button[x, y, b] => (b.type = Press => b'.type = b.type && b.type != Press => b'.type = Over)
この論理式は横に長くて読みにくいです。 

A => (B && C)
のような形の論理式は、{} と改行を使って、以下のように記述することができます。 
A => {
	B
	C
}

今回のマウス移動の事後条件も、同様にして以下のように記述することができます。 
pred mouse_move (x : Int, y : Int, b : Button, b' : Button) {
	! on_button[x, y, b] => b'.type = Normal
	on_button[x, y, b] => {
		b.type = Press => b'.type = b.type
		b.type != Press => b'.type = Over
	}

	b'.width = b.width
	b'.height = b.height
}
ちょっと読みやすくなりました。

4.2. マウス左 Press の振る舞い

次は、mouse_pressL の振る舞いを書いてみます。
元の仕様は
  • ボタンが押されたら、ボタンは Press 状態になります。
です。

マウス移動の振る舞いと同じように書いてみました。 
pred mouse_pressL (x : Int, y : Int, b : Button, b' : Button) {
	on_button[x, y, b] => b'.type = Press


	b'.width = b.width
	b'.height = b.height
}

4.2.1. 振る舞いの検査

run コマンドで確認すると、以下のようなインスタンスが見つかりました。
ボタン外を押したら、Over でかつ幅と高さがかわってしまいました。

これは、on_button[x, y, b] ではないときの事後条件が書かれていないためです。
何も書かれていないと、Alloy は何でもよいと解釈するので、このようなインスタンスが見つかります。
=> で場合分けするときは、必ずすべての場合について考慮されているか気をつけなければいけません。

4.2.2. 振る舞いの修正
というわけで、「ボタン外を押されたときはNormalになる、かつ、幅と高さは変わらない」という仕様にしたいと思います。
pred mouse_pressL (x : Int, y : Int, b : Button, b' : Button) { 
on_button[x, y, b] => b'.type = Press
! on_button[x, y, b] => b'.type = Normal

b'.width = b.width
b'.height = b.height
}
これで、期待しないインスタンスが出てこなくなりました。


4.3. マウス左 Release の振る舞い

最後に、mouse_releaseL の振る舞いを書いてみます。
元の仕様
  • ボタン上にカーソルがないときは、ボタンは Normal 状態です。
  • マウスカーソルが上に来たら、ボタンは Over 状態になります。

これまでと同様にして書いてみました。 
pred mouse_releaseL (x : Int, y : Int, b : Button, b' : Button) {
	on_button[x, y, b] => b'.type = Over
	! on_button[x, y, b] => b'.type = Normal


	b'.width = b.width
	b'.height = b.height
}
run コマンドで確認しても、特に期待しないケースが出てこないので OK とします。


5. 完成

以上でボタンの仕様が Alloy で形式的に記述できました。 
enum Type {Normal, Over, Press}
sig Button {
	type : Type, 	//ボタンの種類
	width : Int, 	//ボタンの幅
	height : Int 	//ボタンの高さ
}
{
	width >= 0 && height >= 0
}

pred show {}
run show

pred on_button (x : Int, y : Int, b : Button) {
	x >= 0 && x < b.width
	y >= 0 && y < b.height
}

pred mouse_move (x : Int, y : Int, b : Button, b' : Button) {
	! on_button[x, y, b] => b'.type = Normal
	on_button[x, y, b] => {
	b.type = Press => b'.type = b.type
		b.type != Press => b'.type = Over
	}

	b'.width = b.width
	b'.height = b.height
}
run mouse_move

pred mouse_pressL (x : Int, y : Int, b : Button, b' : Button) {
	on_button[x, y, b] => b'.type = Press
	! on_button[x, y, b] => b'.type = Normal

	b'.width = b.width
	b'.height = b.height
}
run mouse_pressL

pred mouse_releaseL (x : Int, y : Int, b : Button, b' : Button) {
	on_button[x, y, b] => b'.type = Over
	! on_button[x, y, b] => b'.type = Normal

	b'.width = b.width
	b'.height = b.height
}
run mouse_releaseL

Alloy で仕様を書いて検査する過程で、以下のような元の仕様の曖昧な点が見つかりました。
  • ボタンの幅と高さは 0 未満にならないこと
  • ボタンの幅と高さは変化しないこと
  • Press中にマウスを動かしたときの振る舞い
  • ボタン外でマウス左が押されたときの振る舞い

このように、日本語で書いた仕様には曖昧な点が含まれることがあります。
しかも、がんばって日本語で仕様を書いても、人手によるレビュー以外に検査する方法がありません。
Alloy を使えば、仕様を記述->検査を Alloy と対話しながら自分一人で繰り返すことができるので、よりバグの少ない仕様をより早く記述することが可能になります。



「ボタンの仕様を書いてみよう」をウィキ内検索
最終更新：2009年03月15日 02:13