文法クイックリファレンスやVDM仕様記述等を置いています．随時整理，追加予定です．
文法クイックリファレンス
個々の構文の役割はだいたいわかる，というときに，細かいところを確認するためのものです．著者がVDMToolsの文法マニュアルから代表的なものを抜き出しているので，正式な情報・詳細については，個々のツールの公式Webサイト・マニュアルをご確認下さい．
クイック文法リファレンス （最終更新2011/6/28，PDF，48KB）
書籍内の仕様記述
書面の都合上，特にテストについてはごく簡単なものしか記述していません．
書籍内の仕様記述一式 （zip，21KB）
初期例題（第2章）のバリエーション
一括ダウンロード
2章例題バリエーション一括ダウンロード（zip，15KB）
追加操作定義
書籍内の例題に対し，下記のような操作を加えてみたものです．2章まで読んだ時点では難しいかと思いますが，例えば5.1（集合演算）まで読んでいただいた後であれば，演習としてぜひご自身で加えてみていただくのもよいと思います．
- 指定されたユーザのイベントに対する参加登録を取り消す操作
- 指定された複数のユーザをイベントに対し参加登録する操作
- 指定されたユーザの集合から，まだ参加登録していない複数のユーザを選択し，イベントに対し参加登録する操作（陰定義のみ）
さらに，テスト操作も増やしその中にIOライブラリの使用例も含むようにしました（IOライブラリについてはこちらのページで解説しています）．
2章例題拡張版ダウンロード（zip，4KB）
バリエーション
下記のバリエーションも必要に応じ参考にして下さい．
- VDMUnit利用サンプル（zip，8KB）
- 同じ拡張版記述やテスト仕様のVDM-SL版（zip，3KB）
- 型や変数などの名前を日本語にした場合の記述例（zip，1KB）
© Fuyuki Ishikawa, National Institute of Informatics, Japan, 2011-