VDM++による形式仕様記述 - 形式仕様入門・活用の第一歩

著者名：本位田真一【監修】/荒木啓二郎【監修】/石川冬樹

近代科学社（2018/08発売）

• ISBN：9784764904095

内容説明

明確な仕様の記述と検証を行わずして、抵当な開発を行うことは出来ない！ ソフトウェア開発では、上流工程を自然言語で表現する。このため論理的不一致などがおき、手戻りが発生する。これを解決する方法として考えられたのが、数学を用いた形式手法である。本書は、この手法の一つであるVDMとオブジェクト指向記述言語VDM++について実践的に解説する。

目次

第1章　形式手法とVDM
第2章　VDM概要
第3章　VDM++記述の構成要素
第4章　VDM++によるクラス記述
第5章　VDM++によるモデル化と例題(1)：集合
第6章　VDM++によるモデル化と例題(2)：列
第7章　VDM++によるモデル化と例題(3)：写像
第8章　VDM++ Toolboxの活用
第9章　VDM++ Toolboxにおける実装への展開
第10章　VDM++・VDM++ Toolboxを用いた開発
第11章　関連情報

付録A　VDM++簡易リファレンス
付録B　練習問題解答

感想・レビュー

※以下の感想・レビューは、株式会社ブックウォーカーの提供する「読書メーター」によるものです。

[carbon_twelve]

日本語による数少ないVDM++の入門書の一つ。形式手法とVDMの説明から始まり、VDM++の文法と使い方を例題を用いて解説している。最後の2章ではVDM++ Toolboxの利用についても簡単に触れている。VDM++がどういう性格の言語なのかを知ることができると思う。

2012/11/19

[Q]

VDM++という形式仕様記述の概説。VDM++はモデル検査ではないので、網羅的な検証を行なうことはできない。しかし事前/事後条件や不変条件を付記したオブジェクト志向なモデルをインタープリタで実行でき、またカバレッジも求めることができる。さらにJavaやC++のスケルトンコードを生成でき、さらにJavaの実装からVDM++のモデルを導出できるツールもあるようだ。オブジェクト志向言語に落とす前提であれば機能する場面もあるように感じた。一方もっと抽象度が高く網羅的な検査が必要な場面には別のツールが良いと感じた

2019/01/21