「集合を使って仕様を書いてみよう」の編集履歴(バックアップ)一覧はこちら
集合を使って仕様を書いてみよう - (2009/03/14 (土) 22:23:43) の1つ前との変更点
追加された行は緑色になります。
削除された行は赤色になります。
今回は「集合」を使って仕様を記述します。
* 1. 集合
----
集合は高校の数学でやっていると思いますし、分かりやすい説明ページがいくつもあるので、検索して確認しておいてください。
* 2. 今回記述する仕様
----
簡単な「座席予約システム」の仕様を記述してみます。
** 2.1. 日本語の仕様
- 座席予約システムは、ある劇場の座席を管理するシステムです。
- ユーザは座席の予約、キャンセルができます。
- システムは、座席の一覧と、予約済みの座席の一覧を管理しています。
- 座席には A 席と S 席の 2 種類があります。
- A 席と S 席の座席は、それぞれ 1 席以上あります。
- 座席の予約
-- ユーザは A 席か S 席のどちらかを指定します。
-- システムは指定された方のうち、どれか 1 つの座席を予約して、予約した座席をユーザに通知します。
-- 予約は、座席が余っているときのみ可能です。
- 座席のキャンセル
-- ユーザは予約済みの座席を 1 つ指定します。
-- システムは、指定された座席の予約をキャンセルします。
* 3. 状態空間の記述
----
それでは早速 Alloy で仕様を記述してみましょう。
流れは前回のボタンと同じです。
まずはシステムの状態空間を記述します。
** 3.1. システムのパラメータ
システムの状態空間は、前回やったように
sig System{
パラメータ
}
という形で記述します。
まずは座席予約システムのパラメータを決めます。
日本語の仕様を読むと、「システムは、座席の一覧と、予約済みの座席の一覧を管理しています。」とあるので、
- 座席の一覧
- 予約済みの座席の一覧
の 2 種類が必要そうです。
座席は S 席と A 席の 2 種類があるので、
- S 席の座席の一覧
- A 席の座席の一覧
- 予約済みの座席の一覧
の 3 種類のパラメータを用意することにします。
** 3.2. パラメータの型
前回説明したように、パラメータは
名前 : 型
というフォーマットで記述します。
ということで、次はパラメータの型を決めます。
今回のパラメータはどれも「座席の一覧」です。
「座席の一覧」は座席の集まりなので、集合で表すことにします。
** 3.3. 集合
パラメータの値が集合になる場合、Alloy では以下のように記述します。
名前 : set 型
こう記述すると、パラメータの値は、指定した型の要素を&bold(){ 0 個以上}集めた集合になります。
*** 3.3.1. set の例
例えば、
xs : set Int
と書くと、xs の値は要素の数が&bold(){ 0 個以上}の整数の集合になります。
xs は、{0, 1, 2}, {-1}, {} といった値になります。
*** 3.3.2. 他のバリエーション
Alloy には set 以外にも some, lone, one といったバリエーションがあります。
**** 3.3.2.1. some
要素の数が&bold(){ 1 個以上}の集合になります。
set とは異なり空にはなりません。
**** 3.3.2.2. lone
要素の数が&bold(){ 0 個か 1 個}の集合になります。
**** 3.3.2.3. one
要素の数が&bold(){1個}の集合になります。
なお、何も書かずに
名前 : 型
と書いたものは、
名前 : one 型
の省略型です。
前回ボタンの幅を
width : Int
と書きました。
width の値は 1, 2, 3 といった Int のどれか1個の要素になりそうですが、
実は Alloy では、{1}, {2}, {3} というように、要素ではなく、要素が1個の集合で表されます。
これは Alloy を使う上で&bold(){非常に重要な}概念なので、覚えておいてください。
** 3.4. 型定義
では次に、set や some の後ろに書く型を定義します。
今回は「座席の集合」なので、「座席」という型を定義します。
前回やったように、型は sig や enum を使って定義します。
「座席」の型の要素は具体的にまだ決まっていないので、enum ではなく、sig で定義します。
今回の座席はパラメータを持っていないので、単に
sig Seat{}
となります。
** 3.5. 具体的に記述
以上のことを踏まえると、今回のシステムの状態空間は以下のように記述することができます。
sig Seat{}
sig System{
A_seats : some Seat, //A 席の一覧
S_seats : some Seat, //S 席の一覧
reserved : set Seat //予約済みの座席の一覧
}
A 席と S 席は、日本語の仕様に「A 席と S 席の座席は、それぞれ 1 席以上あります。」とあるので、some にしました。
予約済みの座席の一覧は、誰も予約していない状態があり得るので、set にしました。
* 4. 状態空間の検査/不変条件の追加
----
前回同様
pred show{}
run show
でおかしな状態がないか確認してみます。
こんなインスタンスが見つかりました。
#ref(ins1.png)
これは、Seatの要素が1個で、Systemの要素が0個のインスタンスです。
今はSystemの要素にどんなものが入っているかを確認したいので、うれしくないです。
Nextを押すと、今度はこんなインスタンスが見つかりました。
#ref(ins2.png)
今度はSystemの要素が3個あるようです。
今はSystemの要素におかしなものが無いか、1個ずつ見て確認したいので、一度に3個表示されても見づらいだけです。
** 4.1. インスタンスの要素の数を指定する
こういう場合は、見つけてほしい要素の数を指定します。
具体的には run コマンドを以下のように書きます。
run show for 3 but exactly 1 System
これは、
sig の各要素は 3 個以下で探してください。
ただし、System の要素だけは 1 個で探してください。
ということを指定しています。
なお、今まで書いていた
run show
は、
run show for 3
と同じです。
** 4.2. 再度検査
今度は
run show for 3 but exactly 1 System
で検査してみます。
こんなインスタンスが見つかりました。
#ref(ins3.png)
A 席と S 席に同じ Seat が含まれています。
これは期待していない状態です。
** 4.3. 不変条件の追加
期待しない状態は、不変条件で除きます。
同じ座席が A と S の両方に含まれることはない
という不変条件を追加します。
この条件は、集合の演算子を使って次のように記述することができます。
no (A_seats & S_seats)
これは、
A_seat と S_seat の共通部分は空である
という意味の論理式です。
*** 4.4. 集合の演算子
Alloy の集合の演算子には以下のものがあります。
|演算子|構文|意味|結果の型|
|+|A + B|A と B の和集合|集合|
|-|A - B|A から B を引いた差集合|集合|
|&|A & B|A と B の共通部分|集合|
|#|#A|A の濃度 (要素数)|Int|
|=|A = B|A と B の要素はすべて等しい|Bool|
|in|A in B|A は B の部分集合である|Bool|
|some|some A|A の要素は 1 個以上である|Bool|
|one|one A|A の要素は 1 個である|Bool|
|lone|lone A|A の要素は 1 個以下である|Bool|
|no|no A|A の要素は 0 個である|Bool|
※ A と B の型は集合です。
** 4.5. 再度検査
先ほどの条件を不変条件に追加して、再度検査してみます。
何度かNextでインスタンスを確認していると、次のようなインスタンスが見つかりました。
#ref(ins3.png)
A 席でも S 席でもない Seat0 が予約されています。
これは期待していない状態です。
予約されている座席は、A 席か S 席のどちらかの座席のはずです。
** 4.6. 不変条件の追加
不変条件に、
予約されている座席は、A 席か S 席のどちらかの座席である
という条件を追加します。
この条件は、集合の演算子を使って次のように書くことができます。
reserved in (A_seats + S_seats)
** 4.5. 再度検査
先ほどの条件を不変条件に追加して、再度検査してみます。
何度か Next を押してインスタンスを確認してみてもおかしな状態がでてこないので、OKとします。
** 4.6. 状態空間+不変条件完成
sig Seat{}
sig System{
A_seats : some Seat, //A 席の一覧
S_seats : some Seat, //S 席の一覧
reserved : set Seat //予約済みの座席の一覧
}
{
no (A_seats & S_seats) //同じ座席が A と S の両方に含まれることはない
reserved in (A_seats + S_seats) //予約されている座席は、A 席か S 席のどちらかの座席である
}
pred show{}
run show for 3 but exactly 1 System
* 5. 振る舞いの記述/検査
----
** 5.1. 座席の予約
座席の予約の仕様を確認します。
- 座席の予約
-- ユーザは A 席か S 席のどちらかを指定します。
-- システムは指定された方のうち、どれか 1 つの座席を予約して、予約した座席をユーザに通知します。
-- 予約は、座席が余っているときのみ可能です。
まずは pred の引数を決めます。
*** 5.1.1. 入力パラメータ
入力として、A 席か S 席を指定しますが、指定するときの "A 席", "S 席"という名前を定義していないので定義します。
enum SeatType {A, S}
pred の引数で SeatType を受け取ります
pred book(s : SeatType,
*** 5.1.2. 出力パラメータ
予約した座席を返すので、pred
今回は「集合」を使って仕様を記述します。
* 1. 集合
----
集合は高校の数学でやっていると思いますし、分かりやすい説明ページがいくつもあるので、検索して確認しておいてください。
* 2. 今回記述する仕様
----
簡単な「座席予約システム」の仕様を記述してみます。
** 2.1. 日本語の仕様
- 座席予約システムは、ある劇場の座席を管理するシステムです。
- ユーザは座席の予約、キャンセルができます。
- システムは、座席の一覧と、予約済みの座席の一覧を管理しています。
- 座席には A 席と S 席の 2 種類があります。
- A 席と S 席の座席は、それぞれ 1 席以上あります。
- 座席の予約
-- ユーザは A 席か S 席のどちらかを指定します。
-- システムは指定された方のうち、どれか 1 つの座席を予約して、予約した座席をユーザに通知します。
-- 予約は、座席が余っているときのみ可能です。
- 座席のキャンセル
-- ユーザは予約済みの座席を 1 つ指定します。
-- システムは、指定された座席の予約をキャンセルします。
* 3. 状態空間の記述
----
それでは早速 Alloy で仕様を記述してみましょう。
流れは前回のボタンと同じです。
まずはシステムの状態空間を記述します。
** 3.1. システムのパラメータ
システムの状態空間は、前回やったように
sig System{
パラメータ
}
という形で記述します。
まずは座席予約システムのパラメータを決めます。
日本語の仕様を読むと、「システムは、座席の一覧と、予約済みの座席の一覧を管理しています。」とあるので、
- 座席の一覧
- 予約済みの座席の一覧
の 2 種類が必要そうです。
座席は S 席と A 席の 2 種類があるので、
- S 席の座席の一覧
- A 席の座席の一覧
- 予約済みの座席の一覧
の 3 種類のパラメータを用意することにします。
** 3.2. パラメータの型
前回説明したように、パラメータは
名前 : 型
というフォーマットで記述します。
ということで、次はパラメータの型を決めます。
今回のパラメータはどれも「座席の一覧」です。
「座席の一覧」は座席の集まりなので、集合で表すことにします。
** 3.3. 集合
パラメータの値が集合になる場合、Alloy では以下のように記述します。
名前 : set 型
こう記述すると、パラメータの値は、指定した型の要素を&bold(){ 0 個以上}集めた集合になります。
*** 3.3.1. set の例
例えば、
xs : set Int
と書くと、xs の値は要素の数が&bold(){ 0 個以上}の整数の集合になります。
xs は、{0, 1, 2}, {-1}, {} といった値になります。
*** 3.3.2. 他のバリエーション
Alloy には set 以外にも some, lone, one といったバリエーションがあります。
**** 3.3.2.1. some
要素の数が&bold(){ 1 個以上}の集合になります。
set とは異なり空にはなりません。
**** 3.3.2.2. lone
要素の数が&bold(){ 0 個か 1 個}の集合になります。
**** 3.3.2.3. one
要素の数が&bold(){1個}の集合になります。
なお、何も書かずに
名前 : 型
と書いたものは、
名前 : one 型
の省略型です。
前回ボタンの幅を
width : Int
と書きました。
width の値は 1, 2, 3 といった Int のどれか1個の要素になりそうですが、
実は Alloy では、{1}, {2}, {3} というように、要素ではなく、要素が1個の集合で表されます。
これは Alloy を使う上で&bold(){非常に重要な}概念なので、覚えておいてください。
** 3.4. 型定義
では次に、set や some の後ろに書く型を定義します。
今回は「座席の集合」なので、「座席」という型を定義します。
前回やったように、型は sig や enum を使って定義します。
「座席」の型の要素は具体的にまだ決まっていないので、enum ではなく、sig で定義します。
今回の座席はパラメータを持っていないので、単に
sig Seat{}
となります。
** 3.5. 具体的に記述
以上のことを踏まえると、今回のシステムの状態空間は以下のように記述することができます。
sig Seat{}
sig System{
A_seats : some Seat, //A 席の一覧
S_seats : some Seat, //S 席の一覧
reserved : set Seat //予約済みの座席の一覧
}
A 席と S 席は、日本語の仕様に「A 席と S 席の座席は、それぞれ 1 席以上あります。」とあるので、some にしました。
予約済みの座席の一覧は、誰も予約していない状態があり得るので、set にしました。
* 4. 状態空間の検査/不変条件の追加
----
前回同様
pred show{}
run show
でおかしな状態がないか確認してみます。
こんなインスタンスが見つかりました。
#ref(ins1.png)
これは、Seatの要素が1個で、Systemの要素が0個のインスタンスです。
今はSystemの要素にどんなものが入っているかを確認したいので、うれしくないです。
Nextを押すと、今度はこんなインスタンスが見つかりました。
#ref(ins2.png)
今度はSystemの要素が3個あるようです。
今はSystemの要素におかしなものが無いか、1個ずつ見て確認したいので、一度に3個表示されても見づらいだけです。
** 4.1. インスタンスの要素の数を指定する
こういう場合は、見つけてほしい要素の数を指定します。
具体的には run コマンドを以下のように書きます。
run show for 3 but exactly 1 System
これは、
sig の各要素は 3 個以下で探してください。
ただし、System の要素だけは 1 個で探してください。
ということを指定しています。
なお、今まで書いていた
run show
は、
run show for 3
と同じです。
** 4.2. 再度検査
今度は
run show for 3 but exactly 1 System
で検査してみます。
こんなインスタンスが見つかりました。
#ref(ins3.png)
A 席と S 席に同じ Seat が含まれています。
これは期待していない状態です。
** 4.3. 不変条件の追加
期待しない状態は、不変条件で除きます。
同じ座席が A と S の両方に含まれることはない
という不変条件を追加します。
この条件は、集合の演算子を使って次のように記述することができます。
no (A_seats & S_seats)
これは、
A_seat と S_seat の共通部分は空である
という意味の論理式です。
*** 4.4. 集合の演算子
Alloy の集合の演算子には以下のものがあります。
|演算子|構文|意味|結果の型|
|+|A + B|A と B の和集合|集合|
|-|A - B|A から B を引いた差集合|集合|
|&|A & B|A と B の共通部分|集合|
|#|#A|A の濃度 (要素数)|Int|
|=|A = B|A と B の要素はすべて等しい|Bool|
|in|A in B|A は B の部分集合である|Bool|
|some|some A|A の要素は 1 個以上である|Bool|
|one|one A|A の要素は 1 個である|Bool|
|lone|lone A|A の要素は 1 個以下である|Bool|
|no|no A|A の要素は 0 個である|Bool|
※ A と B の型は集合です。
** 4.5. 再度検査
先ほどの条件を不変条件に追加して、再度検査してみます。
何度かNextでインスタンスを確認していると、次のようなインスタンスが見つかりました。
#ref(ins3.png)
A 席でも S 席でもない Seat0 が予約されています。
これは期待していない状態です。
予約されている座席は、A 席か S 席のどちらかの座席のはずです。
** 4.6. 不変条件の追加
不変条件に、
予約されている座席は、A 席か S 席のどちらかの座席である
という条件を追加します。
この条件は、集合の演算子を使って次のように書くことができます。
reserved in (A_seats + S_seats)
** 4.5. 再度検査
先ほどの条件を不変条件に追加して、再度検査してみます。
何度か Next を押してインスタンスを確認してみてもおかしな状態がでてこないので、OKとします。
** 4.6. 状態空間+不変条件完成
sig Seat{}
sig System{
A_seats : some Seat, //A 席の一覧
S_seats : some Seat, //S 席の一覧
reserved : set Seat //予約済みの座席の一覧
}
{
no (A_seats & S_seats) //同じ座席が A と S の両方に含まれることはない
reserved in (A_seats + S_seats) //予約されている座席は、A 席か S 席のどちらかの座席である
}
pred show{}
run show for 3 but exactly 1 System
* 5. 振る舞いの記述/検査
----
** 5.1. 座席の予約
座席の予約の仕様を確認します。
- 座席の予約
-- ユーザは A 席か S 席のどちらかを指定します。
-- システムは指定された方のうち、どれか 1 つの座席を予約して、予約した座席をユーザに通知します。
-- 予約は、座席が余っているときのみ可能です。
まずは pred の引数を決めます。
*** 5.1.1. 入力パラメータ
入力として、A 席か S 席を指定しますが、指定するときの "A 席", "S 席"という名前を定義していないので定義します。
enum SeatType {A, S}
pred の引数で SeatType を受け取ります
pred reserve_seat(t : SeatType,
*** 5.1.2. 出力パラメータ
予約した座席をユーザに通知します
とあるので、引数で予約した座席を返すことにします。
pred reserve_seat(t : SeatType, rs : Seat
*** 5.1.3. 事前と事後の状態
事前と事後の状態も、忘れず引数で定義しておきます。
pred reserve_seat(t : SeatType, rs : Seat, s, s' : System)
これで引数は完成しました。
*** 5.2. 事後条件の記述
事後条件に関係する日本語の仕様は、次の2つです。
- システムは指定された方のうち、どれか 1 つの座席を予約して、予約した座席をユーザに通知します。
- 予約は、座席が余っているときのみ可能です。
まず1つ目について見ていきます。
- システムは指定された方のうち、どれか 1 つの座席を予約して、予約した座席をユーザに通知します。
予約した座席 rs は、t で指定された方の座席なので、その条件を追加します。
t = A => rs in s.A_seats
t = S => rs in s.S_seats
それから、rs は事後の reserved に追加されているので、その条件を追加します。
s.reserved + rs = s'.reserved
次に2つ目について見ていきます。
- 予約は、座席が余っているときのみ可能です。
つまり、事前の状態では、t で指定された方の座席のうち、 reserved に入っていない座席が 1 つ以上ある必要があります。
この条件は次のように書けます。
t = A => some (s.A_seats - s.reserved)
t = S => some (s.S_seats - s.reserved)
最後に、A席とS席自体は振る舞いの前後で変わらないという条件も忘れずに追加しておきます。
s'.A_seats = s.A_seats
s'.S_seats = s.S_seats
これで一通り事後条件が書けました。
pred reserve_seat(t : SeatType, rs : Seat, s, s' : System){ //t 予約する座席の種類, rs 予約された座席
t = A => some (s.A_seats - s.reserved)
t = S => some (s.S_seats - s.reserved)
t = A => rs in s.A_seats
t = S => rs in s.S_seats
s.reserved + rs = s'.reserved
s'.A_seats = s.A_seats
s'.S_seats = s.S_seats
}