『形式手法の技術講座』

https://gyazo.com/23033a3992c99c40daf1134ed37ab857

2008/5/1

感想

読みやすく内容もかなり良さげ

良いことばかり書いている雰囲気もあるが、本当ならすごいね、という気持ちで読んでる

目次

伝統的手法の問題点

日本語の仕様が曖昧

日本語だけではこの辺の区別が曖昧になりがち

欠陥が発見されるまでが遅い

理想的には要求分析フェーズで洗い出したい

etc.

なんちゃってオレオレ〇〇言語風言語で仕様を書くよりも実際に実行できる言語で書いたほうが良い

日本語の仕様を完全に無くせという話ではない

意図の表明や、非機能要件は日本語のほうが表現しやすい

要は、仕様を書くフェーズでの堅牢性を高めようぜ、というのが目的

もっと具体的に言えば、要求分析や設計段階

コードに着手する前の段階で、仕様のおかしさに気付けると早期に修正ができる

手戻りも少なく、コストが低い

特に、開発者が慣れていないドメインなどでは効果の発揮度合いが大きい

仕様を書く際に、例えば、

TypeScriptの型だけで書く、

TypeScriptの実装も書いちゃう (仕様とは)

みたいなやり方もできるわけで、そうではなく、わざわざ別言語である形式仕様記述言語を使うメリットがあれば知りたい

e.g.

VDM++からC++のコードの生成ができるらしい

値の長さなど、篩型等がなければ難しいようなものも記述できる

まあ、静的じゃないからね

触るなら、よい形式言語を採用してみたい

syntaxに馴染みがある、環境構築が簡単である、生成対象が広い、情報が多い、とか

第2章 「形式手法」技術解説

形式手法を使ってどのように開発していくのか？について

大雑把な進め方

1. 厳密に定義された仕様記述言語で、仕様を記述する

2. 証明 モデル検査・仕様アニメーションのいずれかを使って、 仕様を検証する

3. 仕様アニメーションを使って、 仕様の妥当性検査を行う

4. 仕様を段階的に洗練して、プログラムへ変換していく

自動生成できたり、仕様を見ながら手で書いたりする

5. プログラムをテストする

雑な書き方と雑な例

雰囲気はわかる

これら一覧は人間が証明して上げる必要があるということか？

VDM++は、事前に書いた仕様から証明すべき証明を一覧で出してくれるってことかな

2.4.4 実行可能な陽仕様のテストケース.

2.4.5

オブジェクト指向モデル

オブジェクト指向モデルの仕様

『共通定義』クラス ..

『本』 クラス

31

2.5.3 陰仕様モデル

『巡航制御コントローラー』

『巡航制御コントローラー』 構成子

2.5.4 AutoCruise Type

2.5.5

『巡航制御環境』

2.5.6

『スロットル』

2.5.7 Utilities

陽仕様モデル

2.6.1 『巡航制御コントローラー』

『巡航制御コントローラー』構成子

狀態遷移機械

2.6.2

『スロットル』

2.6.3 『スロットル位置履歴』

2.6.4 回帰テスト仕様

テスト用クラスT.

主な形式手法と形式仕様記述言語の概要

各手法と言語の位置づけ

モデルベース仕様記述言語.

第3章 主な形式手法と形式仕様記述言語の概要

代数仕様記述言語

モデル検査用仕様記述言語

モデル検査の手順

Promela で記述したモデル例

.

.

第４章　「形式手法」の効果的な導入法（問題が大きい工程の解明；仕様のフレームワーク構築　ほか）

問題が大きい工程の解明

仕様のフレームワーク構築 ..

形式手法に則した開発体制.

4.3.1 形式手法適用成功チームの特徴.

4.3.2 開発チームの構成 ..

開発プロセス.

始めよう

付録 A

参考文献

iv

付録 B VDM++ 言語説明

B.1

具象構文表記法.

B.2

クラス.

B.3

データ型定義

B.3.1 基本データ型

ブール型 .

数型

文字型

引用型

B.3.2 合成型

集合型

列型

写像型

レコード型.

合併型と選択型

オブジェクト参照型

あとがき