EventBの書き方について

前に、ツールの話は書いたので、今回は、書き方について。

Event-Bは、Bとちがって、２つの部分に分かれる。
MachineとContext（別々のファイルになる）

Contextは、おもにSet（集合）の内容を記述する。記述項目は、こんなかんじ

CONTEXT
EXTENDS
SETS
CONSTANTS
AXIOMS

一方、MACHINEは、Contextを取り込んで、実際にいろんな記述をしていく。項目内容はこんな感じ
MACHINE
(REFINES)
SEES
VARIABLES
INVARIENTS
THEOREMS
EVENT
(VARIANT)
END

このうち、REFINESとVARIANTはリファインメント（あるEvent-B記述をさらに詳細化したもの）で使用します。
SEESで、参照するCONTEXTを指定する。

ってことで、以下、CONTEXTから。

---

■CONTEXTの内容について

CONTEXTは、以下のことを書く。
CONTEXT
EXTENDS
SETS
CONSTANTS
AXIOMS

　つまり、集合と定数という、型とか、固定的な値（変数のように、インスタンスでないもの。クラス定義するようなもの）を宣言する。
　以下、それぞれについてみていく。

●CONTEXT
　CONTEXT　コンテキスト名
　コンテキストの名前を指定する
　
●SETS
　SETS
　　　集合名１;
　　　　：
　　　集合名N

　集合を宣言していく。

●CONSTANTS
　CONSTANTS
　　　定数名１;
　　　　：
　　　定数名N
　定数を「宣言」していく。

●AXIOMS
AXIOMS
ラベル１: 定数１：型１

　ここで、定数の型を指定する。
　型は、NAT1など、あらかじめあるものか、上記SETSで指定したもの

(例）
CONTEXT SampleContext1
SETS
MYSET
CONSTATNTS
val1
AXIOMS
　　axm1 : val1 : MYSET
END

---

■MACHINEの内容について

　実際の記述は、MACHINEでやる。Bとちがい、リファインメントしたものでもなんでも
MACHINE。MACHINEには、以下の内容を書く。

MACHINE
(REFINES)
SEES
VARIABLES
INVARIENTS
THEOREMS
EVENT
(VARIANT)
END

以下、こんなかんじ。
●MACHINE
　MACHINE マシン名

　マシン名を適当に決めて書く

●SEES
　SEES
　　コンテキスト名

　利用するコンテキストを指定する

●VARIABLES
　VARIABLES
　　変数名

　利用する変数を宣言する

●INVARIANTS
　INVARIANTS
　　ラベル名：変数：不変条件
　変数の不変条件をかく。つまり、変数が満たすべき制約を書く。
　ということは、変数の型とか、範囲とか、変数間の関係とか。
　条件をいくつか書くと、条件間のANDとなる
　（ORは条件内にORと書く）

●EVENTS
　イベントをかく。
　はじめに、INITIALIZATIONがあるので、そこに初期化条件を書く。
　BEGINのあとに、
　　　ラベル名：式
　の形。代入は：＝

　INITIALIZATIONを書いたら、つぎから、書きたいイベント（処理）をかく。
　処理自体は、BEGINの中に、同じように書く。

●VARIANT
　変わっていく変数(負のすうにはならない）で、どんどん減少していくもの
　停止性を証明するためには、必要

---

こんなかんじかな。一部しか書いてないけど・・・
まちがってたら、ごめん。