きのうのＢメソッドについてのつづき。
つまり、Ｂメソッドは、
モデル → 型チェック → 証明責務生成 → 自動的に証明（一部無理なものを手で証明）
という工程をへて、
事前条件、事後条件、不変条件の関係が正しいものに成っているかを証明する、形式仕様記述の１つ
ってことになる。
で、今回は、そのモデル部分の記述のしかたについて
■モデルのサンプル
ここに、Ｂで書いたモデルのサンプルがある
http://www.tools.clearsy.com/index.php5?title=B_Language_User_Manual_1.2#Modelling_dynamic_properties
引用すると、こんなかんじ
MACHINE
DynamicProperty
ABSTRACT VARIABLES
fifo, cmd
INVARIANT
fifo : {T_0, T_MINUS_1, T_MINUS_2} +-＞ {ON,OFF} ^
cmd : {ON,OFF}
INITIALISATION
fifo := {} ||
cmd := OFF
OPERATIONS
SetCmd(cc) =
PRE cc : {ON,OFF} THEN
cmd := cc
END;
UpdateFifo =
ANY local_fifo WHERE
local_fifo : {T_0, T_MINUS_1, T_MINUS_2} +-＞ {ON,OFF}^
local_fifo[{T_MINUS_2}] = fifo[{T_MINUS_1}] ^
local_fifo[{T_MINUS_1}] = fifo[{T_0}] ^
local_fifo[{T_0}] = cmd
THEN
fifo := local_fifo
END
END
|
（＞は、本当は半角）
MACHINE、ABSTRACT VARIABLES、INVARIANT、INITIALISATION、OPERATIONSがキーワードになる。
オブジェクト指向なんかと同じように、値の部分に関してと、操作の部分に関してのきまりがあって、
値の部分に関して言えば、値には、パラメータと、変数（アブストラクトとコンクリートがある）、定数があって、それぞれ、どこに制約条件が書けるかがちがってくる。
また、値には、型があるけど、その型は、集合の形でSETで規定する。
操作の部分に関して言うと、INITIALISATIONが初期化、OPERATIONSがそれぞれのメソッドに関してになる。
■値の部分に関して
Ｂにおいて、１つの仕様のまとまりがMACHINEになるけど（仕様以外、詳細、実装はまた違うキーワードを使う）、そのMACHINEを宣言するときに、MACHINEに渡す引数がパラメータということになる。
また、変数、定数の定義もできる。
変数、定数の型は、基本的に用意されている型のほか、SETによって、集合の形で自分で定義してもいい。
その際、制約があるが、（たとえば、上記の例だとcmd は ONかOFFとか）その制約は、
パラメータは、CONSTRAINSで制約を書き、
CONSTANT(定数）は、PROPERTIESで制約を書き、
VARIABLES(変数）は、INVARIANTで制約を書くけど、
INVARIANTは不変条件なので、ここではもちろん、パラメータやCONSTANTを使って、いろいろと
制約を書いていくことになる。
なお、SETのところでは、型である、集合をかくことになるけど、
defferd SETの場合は、名前だけ登場する
いなむれーしょんせっと（だったっけかな？）の場合は、値を列挙する。
それらの制約は、PROPERTIESで書く(ちなみに、上記の例では、それらの制約はない）。
※なお、あるセットのサブセットを定義したい場合、両方ともSETに書くことはできない。
この場合、元のセットをSETのところに書き、サブセットをCONSTANTで宣言し、
制約をPROPERTIESで書くという手がある。
■操作の部分に関して
INITIALISATIONで初期化の仕方を指定し、
OPERATIONSがそれぞれのメソッドの事前、事後条件を書く。
不変条件は、INVARIANTで書いている。
上記の例だと、OPERATIONS内の、UpdateFifo 、SetCmd(cc) が
メソッドに相当する（=のところですね）
PREが事前条件で、事前条件が成立する場合、
THEN以降（ENDまで）の、事後条件が成立しないといけない。
もちろん、不変条件INVARIANTは、事前、事後ともに成立することになる。
これが、成立することを証明していくことで、プログラムの正しさを検証するのが、Ｂメソッド。
なお、自動証明に難しい場合、証明を補助するためにASSERTIONSというのを書く。
ここで定理みたいなことを書くけど、いくら定理が不変でも、不変条件に定理は書かない
(証明しなくちゃなんなくなってしまうので）でASSERTIONSに書く。
てなかんじが、モデルの作り方。
このあと（証明責務から先）は、また今度・・
Ｐ．Ｓ ちなみに、上記モデルは、ON,OFFというコマンド(cmd)があって、これをバッファ（T_0, T_MINUS_1, T_MINUS_2）に入れている。ＦＩＦＯでコマンドが入っていく（直近の３つのみキープ）
