内容説明
実用システム開発ではまず仕様を書こう！明確な仕様の記述と検証を行わずして正統な開発を行うことはできない―何を開発するのかを表す仕様の実践的なモデリングと、仕様書を基盤とする開発者間の建設的な対話に向けて。
目次
形式手法とＶＤＭ
ＶＤＭ概要
ＶＤＭ＋＋記述の構成要素
ＶＤＭ＋＋によるクラス記述
ＶＤＭ＋＋によるモデル化と例題（１）：集合
ＶＤＭ＋＋によるモデル化と例題（２）：列
ＶＤＭ＋＋によるモデル化と例題（３）：写像
ＶＤＭ＋＋ Ｔｏｏｌｂｏｘの活用
ＶＤＭ＋＋ Ｔｏｏｌｂｏｘにおける実装へのの展開
ＶＤＭ＋＋・ＶＤＭ＋＋ Ｔｏｏｌｂｏｘを用いた開発
関連情報
著者等紹介
荒木啓二郎［アラキケイジロウ］
１９７８年九州大学大学院工学研究科修士課程修了。九州大学工学部助手。１９８２年工学博士。１９８４年九州大学助教授。１９８８年～１９８９年文部省在外研究員（ドイツ連邦共和国パッサウ大学）。１９９３年奈良先端科学技術大学院大学教授。１９９６年九州大学教授
石川冬樹［イシカワフユキ］
２００７年東京大学大学院情報理工学系研究科博士課程修了、博士（情報理工学）。現在、国立情報学研究所助教・総合研究大学院大学複合科学研究科助教（本データはこの書籍が刊行された当時に掲載されていたものです）
※書籍に掲載されている著者及び編者、訳者、監修者、イラストレーターなどの紹介情報です。
感想・レビュー
※以下の感想・レビューは、株式会社ブックウォーカーの提供する「読書メーター」によるものです。
carbon_twelve
0
日本語による数少ないVDM++の入門書の一つ。形式手法とVDMの説明から始まり、VDM++の文法と使い方を例題を用いて解説している。最後の2章ではVDM++ Toolboxの利用についても簡単に触れている。VDM++がどういう性格の言語なのかを知ることができると思う。2012/11/19
Q
0
VDM++という形式仕様記述の概説。VDM++はモデル検査ではないので、網羅的な検証を行なうことはできない。しかし事前/事後条件や不変条件を付記したオブジェクト志向なモデルをインタープリタで実行でき、またカバレッジも求めることができる。さらにJavaやC++のスケルトンコードを生成でき、さらにJavaの実装からVDM++のモデルを導出できるツールもあるようだ。オブジェクト志向言語に落とす前提であれば機能する場面もあるように感じた。一方もっと抽象度が高く網羅的な検査が必要な場面には別のツールが良いと感じた2019/01/21
