第1部　モデルとソフトウェア開発

第1章　はじめに
　　1.1　ソフトウェア開発の挑戦
　　1.2　複雑さをマスターする：モデリングの役割
　　1.3　ソフトウェア開発におけるモデリングの位置付け
　　1.4　モデリング構造：オブジェクト指向システム
　　1.5　VDM++（データと機能のモデリング）
　　1.6　オブジェクト指向設計におけるVDM++の利用
　　1.7　本書の構成と内容
　　1.8　まとめ

第2章　VDM++でモデルを構築する：その概観
　　2.1　モデルの構築
　　2.2　化学プラントの例
　　2.3　UMLクラス図を用いた構造の選択
　　2.4　モデルをさらに包括的なものにする
　　2.5　モデルの妥当性検証
　　2.6　コード生成
　　2.7　まとめ

第3章　VDM++のツールサポート
　　3.1　はじめに
　　3.2　各ソフトウェアの入手
　　3.3　Roseの利用
　　3.4　VDMToolsの利用
　　3.5　まとめ

第2部　VDM++によるオブジェクト指向システムのモデリング

第4章　データを定義する
　　4.1　はじめに
　　4.2　オブジェクト指向構造
　　4.3　インスタンス変数と不変条件
　　4.4　型と型定義
　　4.5　値と値の定義
　　4.6　まとめ

第5章　機能を定義する
　　5.1　はじめに
　　5.2　関数定義
　　5.3　演算子定義
　　5.4　式
　　5.5　パターン束縛
　　5.6　束縛
　　5.7　文
　　5.8　まとめ

第6章　順序のない集まりをモデリングする
　　6.1　はじめに
　　6.2　集合の概要
　　6.3　ロボットコントローラ
　　6.4　まとめ

第7章　順序のある集まりをモデリングする
　　7.1　はじめに
　　7.2　列の概要
　　7.3　渋滞警告システム（CWS）
　　7.4　まとめ

第8章　関連をモデリングする
　　8.1　はじめに
　　8.2　写像の概要
　　8.3　渋滞警告システム（CWS）の改訂
　　8.4　まとめ

第3部　モデリングの実践-----3つのケーススタディ

第9章　モデルの構造化：エニグマ暗合機
　　9.1　はじめに
　　9.2　エニグマの歴史的重要性
　　9.3　エニグマ暗号機のアルゴリズム
　　9.4　エニグマモデルの構築
　　9.5　VDMUnitフレームワーク
　　9.6　エニグマモデルのテスト
　　9.7　まとめ

第10章　ビューの結合：CSLaMシステム
　　10.1　はじめに
　　10.2　CSLaMシステム
　　10.3　列車に搭載されたCSLシステム
　　10.4　メンバ宣言
　　10.5　車内ディスプレイ
　　10.6　ビーコンクラス
　　10.7　予告と制限
　　10.8　運転士のパフォーマンスをモニタリング
　　10.9　まとめ

第11章　TradeOne：エンタープライズアーキテクチャからビスネスアプリケーションまで
　　11.1　はじめに
　　11.2　エンタープライズアーキテクチャ
　　11.3　TradeOneアーキテクチャ
　　11.4　検証のアプローチ
　　11.5　TradeOneのメトリクス
　　11.6　TradeOneプロジェクトの生産性に関する考察
　　11.7　まとめ

第4部　モデルから実装へ

第12章　VDM++による並行処理
　　12.1　はじめに
　　12.2　並行性のモデリング：スレッドと許可述語
　　12.3　POP3サーバ
　　12.4　POP3サーバ内での通信の同期
　　12.5　まとめ

第13章　モデルの品質
　　13.1　はじめに
　　13.2　内部整合性の評価：整合特性検査
　　13.3　APIを使用して外部整合性を評価する
　　13.4　APIを介してPOP3の例題を検証する
　　13.5　まとめ

第14章　Javaで実装する
　　14.1　はじめに
　　14.2　Javaコード生成の概要
　　14.3　基本的なコード生成
　　14.4　コード生成と並行性
　　14.5　POP3のコード生成
　　14.6　まとめ

付録
　問題解答
　Overture-----形式モデリングのためのオープンソースツール群 [訳者補足]
　参考文献
　略語リスト
　項目索引
　定義索引
　訳者あとがき