VDM 理解を目的とした概念と文法の構造化

背景
文法要素の階層化
短時間での理解
.
.
大森 洋一
九州大学 システム情報科学研究院
2015. 3.24.
.
.
.
.
.
.
.
.
..
.
VDM 理解を目的とした概念と文法の構造化
背景
文法要素の階層化
短時間での理解
. VDM 理解環境の現状
.
.
現在，包括的な (英語または日本語の) 教科書がない
.
..
初学者は，入門書 (VDMTools.jp, プログラム仕様記述論) −→ 専門
書 (VDM++によるオブジェクト指向システムの高品質設計と検証,
ソフトウェア開発のモデル化技法) −→ 言語マニュアル
(langmanpp a4?.pdf, lanmansl a4?.pdf) と進む．
入門書と専門書にギャップがある？
背景となる集合論，オブジェクト指向モデル，関数型モデルなどがわ
かっていないから？
専門書に教科書を期待して，メンタルモデルがずれているから？
小さな例題では理解しにくいから？
.
.
.
.
.
.
.
.
..
背景
文法要素の階層化
短時間での理解
. 通して読める教科書があると全体が把握できた気になる
.
研究室学生のアンケート結果
..
入門書の内容は使いこなせる (おそらく VDMPad のおかげ)
この次の過程が課題
.
let 文が使えるのは 1/4 名
関数と手続きの違いは分かるが，使い分けが説明できない
関数の参照透過性はよく分かっていない
マニュアルの説明順は言語理解には向いていない
.
.
.
.
.
.
.
.
.
..
.
.
..
.
.
仮説: 入門書と専門書のギャップを埋める解説が有用ではないか .
..
一通りの文法要素に触れられると安心する
背景
文法要素の階層化
短時間での理解
. 作成方針
.
言語マニュアルの走査
..
予約語を網羅する
コンテキストによる意味の違いも網羅する
.
..
.
説明自体はトップダウンに行う
..
新規の概念はトップダウンの方が理解しやすい
.
.
.
.
.
..
階層内でトップダウンに説明する
.
.
.
.
.
.
.
.
文法要素のグループ化を階層化する
背景
文法要素の階層化
短時間での理解
. スモールステップ化の適用
.
文法要素のグループ化
..
簡単な要素も説明する
類似した要素は近くで説明する
.
..
.
VDM 概念の坂を小坂の連続とする
..
.
図: VDM 理解のスモールステップ化
.
.
.
.
.
.
.
.
.
..
.
.
.
背景
文法要素の階層化
短時間での理解
. スモールステップ化の検討
.
具体的な章分け案
..
手続き記述段階
.
1-1 ファイル構成, 1-2 式, 1-3 文, 1-4 制御構造
陰仕様記述段階
2-1 型, 2-2 変数, 2-3 不変条件, 2-4 陰関数, 2-5 陰手続き, 2-6 事前条件，事後条件
陽仕様記述段階
3-1 陽関数, 3-2 陽手続き, 3-3 初期化, 3-4 例外処理
関数型モデル導入段階
4-1 状態集合, 4-2 遷移条件, 4-3 パターンマッチ, 4-4 写像
オブジェクト指向モデル導入段階
5-1 クラス, 5-2 インスタンス, 5-3 オブジェクト参照
6-1 スレッド, 6-2 同期, 6-3 履歴
.
..
Q1: この分割は妥当か？
.
.
.
.
.
.
.
.
非同期並行処理記述段階
背景
文法要素の階層化
短時間での理解
. スモールステップ化の検討
.
具体的な章分け案
..
手続き記述段階
.
1-1 ファイル構成, 1-2 式, 1-3 文, 1-4 制御構造
陰仕様記述段階
2-1 型, 2-2 変数, 2-3 不変条件, 2-4 陰関数, 2-5 陰手続き, 2-6 事前条件，事後条件
陽仕様記述段階
3-1 陽関数, 3-2 陽手続き, 3-3 初期化, 3-4 例外処理
関数型モデル導入段階
4-1 状態集合, 4-2 遷移条件, 4-3 パターンマッチ, 4-4 写像
オブジェクト指向モデル導入段階
5-1 クラス, 5-2 インスタンス, 5-3 オブジェクト参照
6-1 スレッド, 6-2 同期, 6-3 履歴
.
..
Q1: この分割は妥当か？
.
.
.
.
.
.
.
.
非同期並行処理記述段階
背景
文法要素の階層化
短時間での理解
. 文法要素の整理
VDM++ の予約語は 184 語
.
優先順位の設定
..
予約語の使用頻度は大きく異なる
特定のドメインで使用頻度が異なっていても，近い概念は近い時期
に説明する
.
.
..
.
表形式での整理
..
文法要素はボトムアップに調査した
.
とりあえずマニュアルの説明を利用する
.
.
.
.
.
.
.
.
.
..
.
.
背景
文法要素の階層化
短時間での理解
. トップダウンへの並べ替え
.
構文グループの例
..
手続き記述段階
.
1-1 ファイル構成 6, 1-2 式 52, 1-3 文 4, 1-4 制御構造 13
陰仕様記述段階
2-1 型 45, 2-2 変数 1, 2-3 不変条件 3, 2-4 陰関数 16, 2-5 陰手続き 3, 2-6 事前条件，
事後条件 2
陽仕様記述段階
3-1 陽関数 3, 3-2 陽手続き 1, 3-3 初期化 16, 3-4 例外処理 7
関数型モデル導入段階
4-1 状態集合 1, 4-2 遷移条件 0, 4-3 パターンマッチ 0, 4-4 写像 1
オブジェクト指向モデル導入段階
5-1 クラス 3, 5-2 インスタンス 1, 5-3 オブジェクト参照 5
非同期並行処理記述段階
.
..
検証 3
.
.
.
.
.
.
.
.
6-1 スレッド 6, 6-2 同期 3, 6-3 履歴 5
背景
文法要素の階層化
短時間での理解
. トップダウンの記述例
.
.
クラス
..
VDM++ のモデルはクラスにより記述します． 文は ; で終わります．
.
.
図: クラス記述
.
.
.
.
.
.
.
.
..
.
VDM++ は宣言型の言語ですので，明示的に指定しない限り，記述
順序と実行順序は関係ありません．
.
.
クラスには，定数，型，状態変数，関数，手続き，スレッドといっ
たセクションがあります．セクションはなくても，同じセクション
が複数あっても構いません．
背景
文法要素の階層化
短時間での理解
. 半日で概要を理解するにはどうすればよいか
.
前提
..
講義形式が可能なのは半日程度
.
専門書の理解やツールの習得は別途行う
.
VDM をフル活用しなければならないわけではない
.
..
.
.
.
想定される条件
..
対象はフォーマルメソッドには詳しくないソフトウェア検証の専門家
.
..
フォーマルメソッドの良さを理解してもらい，自律的な理解の足が
かりとする
.
.
.
.
.
.
.
.
状態機械やソフトウェアのモデル化の概念は知っているが，具体的
な手法は知らない
背景
文法要素の階層化
短時間での理解
. VDM の場合
.
例
..
.
一階述語論理によるモデル化
不変条件の理解と応用
事前条件・事後条件の理解と応用
(陽仕様による仕様のテスト)
.
..
.
課題
..
理解しやすいサンプルの用意 (自動販売機？)
複数の書き方を示すには，事例そのままではだめ
.
自習教材と講義の組み合わせ
逆転学習を前提に，内容の切り分けを検討する
.
.
.
.
.
.
.
.
.
..
.
.
パターンマッチ，写像の導入