VDMのお勉強－その４ 使い方

シリーズ「VDMのお勉強」
前回、VDMToolをインストールしたので、今回は、使い方です。

---

■手順

まず、使い方の手順なのですが、こんなかんじです

１．自分の好きなエディタで、VDMを記述する
２．VDMToolをたちあげ、プロジェクトから、１のファイルを追加する
３．とりあえず、チェック
４．テストデータを書いて実行
　　　→スクリプトに書いておくこともできる

ってなかんじです。ではまず、１から・・・

---

■１．自分の好きなエディタで、VDMを記述する

　VDMTool上では、たぶん、VDMを新規作成できないと思うので、
　（「外部エディタ」は、すでに登録したファイルを修正するもの？）
　まあ、とりあえず、なんでもいいから、エディタで、VDM記述を書いて、保存します。

---

■２．VDMToolをたちあげ、プロジェクトから、１のファイルを追加する

　VDMToolを立ち上げてください。
　立ち上がったら、「プロジェクト」→「ファイルを追加」を実行
　ファイルのダイアログが出てくるから、そしたら、１．で作った
　ファイルを選択

　問題ないと、こんなかんじで、出て来る

---

３．とりあえず、チェック

構文チェックと型チェックが、下に書いてあるボタンをクリックするとできるので、
一応確認。

---

４．テストデータを書いて実行

まず、以下の亀さん一方通行をクリック。

すると、「実行ウィンドウ」がでてくる。
まず、真ん中の＞＞にinitと入力し、初期化

つぎに、

print 操作名（引数）

って形になる。たとえば、

print Hello("Hello")

など。


なお、事前条件、事後条件をチェックする場合は、
「プロジェクト」→「プロジェクトオプション」
で、チェックをいれること。

それと、あらかじめ、実行する内容をファイルに書いておいて

script そのファイルの絶対パス

で書いても、実行できる。

---

次回は、VDMの書き方。

Moodleの教材内で、ログインIDを知りたいとき、どうするか？

Moodleにおいて、たとえば、

　　SCORMの教材内とか、
　　トピックとして追加したリソースのウェブページ内で

いま使っているユーザー名を知りたい場合、どうするか？
（ウェブページに＜？PHPとかけない。
　また、SCORMの教材内で書くと、テキストとして扱われるのでPHPは解釈されない）

---

　もっと、いい方法がありそうな気がするけど、はんそくわざ。

教材内に

　＜iframe　SRC="/moodle/a.php"＞＜/iframe＞

とかかいて、moodleのディレクトリの下に、a.phpをつくる。
a.phpの内容は、以下のとおり

＜?PHP
require_once('config.php');
require_once($CFG-＞dirroot .'/course/lib.php');
require_once($CFG-＞dirroot .'/lib/blocklib.php');

echo $USER-＞id . "＜BR＞";
echo get_moodle_cookie();
?＞

こうすると、ユーザーIDと、ユーザー名が表示される。
このa.phpの中に教材を作ってしまえばOKだし、
iframeじゃなくってAJAXにすれば、
教材からユーザーIDやユーザー名だけ、取ってこれる・・・かな？

形式仕様を開発で使う意義－設計のテストとして（レビューを超えて）

　VDMやBといった形式仕様を、開発で使う意義を考える。

　特にVDMは、スクリプトを使って確認することになる。
　このとき、スクリプトで利用する値は、実装後のテスト、すなわちJUNITなどで使うテストデータの値と同じにすることもできる。


　これは結局、プログラムを作る以前、設計の段階で、仕様を機械的に確認していることになる。
　従来、実装する前の設計レベルの確認は、レビューしかなかったが、
　それが、機械的に確認できることになる。

　ただ、そのために形式仕様を利用するのはハードルが高いわけで、
　ここに何らかしらの工夫が必要になる。