形式仕様記述には、Bメソッドというのがある。これは、どちらかというと、下流よりだが、もっと、上流工程までもサポートしたものとして、Event-Bがある。今日は、そのEvent-Bのお話。
■Event-Bのインストール
今回は、Rodin-Platformというのを使う。
（１）まずは、Event-Bのページにアクセス
http://www.event-b.org/
（２）左側に、Rodin Platformというのがある。それをクリック
（３）まんなからへん（表のInstallationとかかれた桁のなか）に
Download the Core: Rodin Platform file for your
とかかれている。ここのCore以降をクリックすると、ダウンロードページに飛ぶ
（４）Download Nowとかかれたところをクリックして、ダウンロード
（５）ダウンロードが終わったら解凍
（６）解凍したものの中を見ると、rodin.exeというのがあるから、それをダブルクリックすると
立ち上がる。
→Eclipseのプラグインってことです。
つぎに、こいつがAtrlierBを使うみたいなので、それをインストールする
はじめに出てくる画面（きたないピンク色の画面。出てこなかった場合、
Help→Welcomeで表示できる）の下のほう（Important Installation notes）
に書いてあるんだけど、
（７）Help → Install New Software....
で、インストール画面を出して
（８）出てきた画面の一番下、
Contact all update sites during install to find required software
のチェックをはずす
（９）一番上、WorkWithのプルダウンのリストを開いて、
Atlier B Provers ・・・（URLが書いてある）・・・
を選択。
（１０）下のリストに、Atlier Bが出てくるので、
それを、チェックしてNext
（１１）あとは、普通のプラグインインストールと同じ
■Event-B、コンポーネントの作成
インストールが終わり、Welcome画面を修了させると、こんなふうに、プロジェクトの画面になる
右上をクリックして、わざと、全部のパースペクティブがわかるようにしている。Event-B
Prove
Resource
の３つのパースペクティブがある。
この状態で、まずは、作成してみる。
メニューバーから
File→New→Event-B Projectを選択
出てきたダイアログで、プロジェクト名を適当に入れる。
プロジェクトが出来たら、コンポーネントをつくる。
下のように、プロジェクトを右クリック、
New→Event-Bコンポーネントを選択する。
出てきたダイアログで、コンポーネント名を入れる（changeMeのところ）
なお、Event-Bは、Bと違い、Machineのほかに、Contextというのも使う。
(使わないときもある）。今回は、Machineにする
■コンポーネントの編集
そうすると、以下のような画面になる。
このツールは、あらかじめ、こんなふうに大枠が出来ていて、
記入したいところの左側三角形をクリックし、＋の丸囲みを
クリックして、書き込んでいく
（－をクリックすると、その行削除）
そうすると、こんな感じになる
■証明
で、証明するには、「Proving」のパースペクティブにして、
チェックマークをクリックする
うまくいくと、チェックになって、そこをクリックすると、
したに、緑のひげくんがでる
だめだと、？になって、そこをクリックすると、
したに、あかいがっかりくんがでる。
ツールの使い方は、ここまで
アクセス
トータル
ランキング
