第１章まずはじめよう！
- １．１すでにある演算を使う
- １．２演算を合成する
- １．３式に名前を付ける
- １．４演算を定義する
- １．５データ構造を定義する
- １．６さらにデータ構造を定義する
- １．７モジュールを定義する
- １．８組込みモジュールＢＯＯＬ
第２章ペアノ自然数と証明スコア法
- ２．１ペアノ自然数のＣａｆｅＯＢＪ仕様
- ２．２ペアノ自然数の等価性判定
- ２．３ペアノ自然数の加算
- ２．４加算の右０の証明
- ２．５加算の右ｓ＿の証明
- ２．６加算の可換則の証明
- ２．７加算の結合則の証明
- ２．８ペアノ自然数の乗算
- ２．９乗算の右０と右ｓ＿の証明
- ２．１０乗算の可換則の証明
- ２．１１階乗演算の等価性の証明
第３章リストとパラメータ化モジュール
- ３．１パラメータ化モジュールによるリストの定義
- ３．２パラメータ化モジュールＬＩＳＴの具体化
- ３．３リストの等価性の定義
- ３．４パラメータ化モジュールＬＩＳＴ＝の具体化
- ３．５リストの連接
- ３．６連接の右ｎｉｌの証明
- ３．７リストの反転
- ３．８反転の逆分配則の証明
第４章列，集合と仕様計算
- ４．１列の定義
- ４．２列の反転
- ４．３列の等価性
- ４．４多重集合の定義
- ４．５集合の定義
- ４．６集合の和と積
- ４．７メンバー述語の積集合への分配則の証明
- ４．８場合分けと仕様計算
- ４．９仕様計算命令：：ｇｏａｌ，：ａｐｐｌｙ，：ｒｅｄ，：ｄｅｆ，：ｃｓｐ
- ４．１０仕様計算命令：：ｓｈｏｗ，：ｄｅｓｃ
- ４．１１仕様計算命令：：ａｐｐｌｙ（〈ｐｒｏｏｆＲｕｌｅＳｅｑ〉）
- ４．１２証明スコアのモジュール化
- ４．１３積集合演算の結合則の証明
- ４．１４積集合演算の可換則と冪等則の証明
- ４．１５集合の等価性
第５章遷移システムの仕様と検証
- ５．１相互排除プロトコルＱＬＯＣＫ
- ５．２ＱＬＯＣＫシステムの仕様
- ５．３検索述語によるシミュレーション
- ５．４検索述語による反例発見
- ５．５遷移システムの不変特性と帰納不変特性
- ５．６初期状態条件の証明スコア
- ５．７検索述語による遷移の検索
- ５．８帰納不変条件の証明スコア
- ５．９遷移システムの到達特性
- ５．１０帰納到達条件の証明スコア
- ５．１１継続到達条件の証明スコア