hisa's tech blog

ここしばらくの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で定理を構成し、健全性が保たれることの証明を行った上で、その定理を実際のモデルの証明に利用可能になるようです。

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

CogToolは、カーネギーメロン大学で作られているUIのプロトタイピングツールです。
（この記事の時点ではフリーです。）

KLM（Keystroke Level Model）をベースとしたモデルが作成され、ユーザが課題を遂行するために必要な時間が自動的に計算されることが特徴になっています。

画像とウィジェットを組み合わせて画面を作り、これをつなぎ合わせてストーリーボードを構成することによってプロトタイプが出来上がります。

このストーリーボードに対して、ユーザーの課題であるタスクとその遂行ための手順であるスクリプトを作ることにより、この課題の遂行に必要な時間が計算されます。

人文系のブログとは別にソフトウェア開発に関するブログを立ち上げました。

しばらくは形式手法 Event-B を中心に書いていく予定です。