第 1 章 形式手法概論
　1.1 ソフトウェア開発過程
　1.2 形式手法
　1.3 Bメソッド

第 2 章 形式仕様の作成
　2.1 形式仕様
　2.2 算術演算を使う例題―ポイント計算
　2.3 抽象機械の書き方
　2.4 抽象機械の整合性の検証
　2.5 ツールを使った整合性の検証
　2.6 演習問題

第 3 章 抽象機械
　3.1 集合と関係を使う例題―座席予約
　3.2 抽象機械の記法
　3.3 抽象機械の構造化
　3.4 抽象機械の整合性検証
　3.5 ツールを使った整合性の検証
　3.6 型チェック
　3.7 抽象機械における事前条件の意味
　3.8 演習問題

第 4 章 仕様から実装へのステップ
　4.1 仕様の段階的詳細化
　4.2 開発過程で使われる記述

第 5 章 リファインメント
　5.1 データ詳細化の例題―有向グラフ
　5.2 リファインメントの記法
　5.3 詳細化の正当性検証
　5.4 ツールを使った整合性と正当性の検証
　5.6 演習問題

第 6 章 インプリメンテーション
　6.1 実装段階のための例題―座席予約
　6.2 インプリメンテーションの記法
　6.3 ライブラリ
　6.4 詳細化の正当性検証
　6.5 ツールを使った整合性と正当性の検証
　6.6 輸入における事前条件の役割
　6.7 演習問題

第 7 章 事例研究
　7.1 アドホックネットワーク
　7.2 題材の概要
　7.3 モデル化の方針
　7.4 モデル１
　7.5 モデル２

第 8 章 次のステップ
　8.1 B メソッドのまとめ
　8.2 Event-B

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