Event-Bの最近のブログ記事

ここしばらくのRodinインストールから自分の環境設定までの流れです。

１．アーカイブを展開して起動

２．Atelier B proversのインストール
　　（Help > Software Updates...）

３．Perspectiveの作成　（詳細は チュートリアル を参照。）
　　Proving Perspectiveをベースにして、Event-B ExplorerとProof TreeをFast Viewに。
　　Fast Viewを右端に移動。
　　保存。（Window > Save Perspective As...）

４．Auto-Tacticの設定
　　（Window > Preferences > Event-B > Sequent Prover > Auto Tactic）
　　プロジェクト保存時の自動証明をオフに。
　　　（Enable auto-tactic for provingのチェックを外す。）
　　　（モデルが大きくなると自動証明の時間が長くなるので保存毎に実行しないように。）
　　PP restrictedとAtelier P0を追加。
　　　（詳細は http://wiki.event-b.org/index.php/Rodin_Provers に書かれています。）

５．必要なプラグインをインストール
　　（Help > Software Updates...）

以上で完了です。

"モジュール"による構造化を可能にするModularisation Plug-inを使い始めました。

概要メモを書いておきます。
（理解が進んだらWikiにも書きます。）

－－－－－－－－－－

各モジュールは"インタフェース"を持っており、モジュール間のやり取りはこのインタフェースを介する形でモデル化します。インタフェースには変数（他のモジュールが認識可能な抽象状態を表す変数）およびオペレーションを定義します。

モジュールは階層構造になっており、上位のモジュールは下位のモジュールのオペレーションの呼び出しおよび変数の参照を行うことができます。

インタフェースによって上位モジュールのモデルに影響を与えることなく下位モジュールのモデル（インタフェースの実現）を変更することができます。

【ざっとプラグインの説明を読んだところでの疑問】
インタフェースには初期化がなく、初期化は利用する側（上位モジュール）で適切に行うこととなっているが、インタフェースを実現するモデルを作ったときに初期化イベントの正当性をどうやって保証するのか。

RodinのRule-based Prover Plug-inが公開されていました。

このプラグインではRewrite Rulesの追加ができます。

集合・メタ変数・Rewrite Rulesで定理を構成し、健全性が保たれることの証明を行った上で、その定理を実際のモデルの証明に利用可能になるようです。

まだユーザマニュアルを見ただけで実際には使っていないので、少し使ってみてからまた記事を書きます。