Bメソッドによる形式仕様記述 - ソフトウェアシステムのモデル化とその検証

著者名：本位田真一【監修】/中島震【監修】/来間啓伸

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

• ISBN：9784764903470

内容説明

仕様の段階で誤りをなくす注目の手法「Bメソッド」を実践活用するための解説書。安心安全を含めてますます高度な機能や性能が要求されるソフトウェアシステムの開発において、厳密な仕様記述を基に開発を行う形式手法に対する関心と期待が高まっている。本書は、我が国初のBメソッドの書き下ろし入門書である。実際の開発への適用を意識した実用指向の内容が、平明でわかりやすく記述されている。

目次

第1章　形式手法概論
第2章　形式仕様の作成
第3章　抽象機械
第4章　仕様から実装へのステップ
第5章　リファインメント
第6章　インプリメンテーション
第7章　事例研究
第8章　次のステップ

付録A　演習問題の解答
付録B　B言語の記号
付録C　Bによる事例研究の記述

感想・レビュー

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

[carbon_twelve]

とりあえず斜め読みしただけ。簡単な例題を用いてBの文法規則や使い方を解説していくスタイルで書かれていて分かりやすかった。7章で事例研究として例題よりやや大きなシステムを取り上げているのもよかった。しかし、Bメソッドに適した仕様の抽出やモデリングには余り触れられておらず、また、証明責務やその証明が長々と書かれているなどしてあまり面白くなかったと感じた。

2012/09/17

[Q]

ざっくり読みました。「証明責務」という用語が突如あらわれ、この用語の責務は機械か人間のどちらが負うべきなのかわかりませんでした。もしこの証明責務が機械による導出ではなく、人力に頼るのであれば、実際のシステムを実装まで現実的な工数で落とすのは難しいのではないかと感じました。またBメソッドはEvent-Bを含めて方言が多そうなので、具体的なツールのマニュアルを読んだ方が(回り道かもしれませんが)理解しやすいのではとも感じました。

2018/12/20