第1章 数学の予備知識
1.1 論理式
1.2 集合
第2章 プログラミング言語の構文
2.1 BNFによる構文の定義
2.2 構文解析木と文法の曖昧性
2.3 具象構文と抽象構文
2.4 構文解析
2.5 言語Wの構文
2.6 帰納的定義
第3章 操作的意味論
3.1 算術式の評価規則
3.2 ブール式の評価規則
3.3 プログラムの評価規則
第4章 プログラムの性質に関する推論
4.1 プログラムの仕様に関する表明
4.2 プログラムの正当性の証明
4.3 ループ不変条件とループ変動式
第5章 ホーア論理
5.1 ホーア論理の表明
5.2 部分正当性{A}c{B}の推論規則
5.3 ホーア論理の健全性と相対完全性
5.4 プログラムの半自動検証へのホーア論理の応用
5.5 完全正当性のための推論規則
第6章 表示的意味論
6.1 算術式の表示的意味
6.2 ブール式の表示的意味
6.3 プログラムの意味
第7章 λ計算
7.1 構文
7.2 代入と簡約
7.3 λ計算の表現力
7.4 簡約戦略と関数型言語
第8章 型つきλ計算
8.1 単純型つきλ計算
8.2 型推論
8.3 ML多相
参考文献
演習問題の解答
索引
1.1 論理式
1.2 集合
第2章 プログラミング言語の構文
2.1 BNFによる構文の定義
2.2 構文解析木と文法の曖昧性
2.3 具象構文と抽象構文
2.4 構文解析
2.5 言語Wの構文
2.6 帰納的定義
第3章 操作的意味論
3.1 算術式の評価規則
3.2 ブール式の評価規則
3.3 プログラムの評価規則
第4章 プログラムの性質に関する推論
4.1 プログラムの仕様に関する表明
4.2 プログラムの正当性の証明
4.3 ループ不変条件とループ変動式
第5章 ホーア論理
5.1 ホーア論理の表明
5.2 部分正当性{A}c{B}の推論規則
5.3 ホーア論理の健全性と相対完全性
5.4 プログラムの半自動検証へのホーア論理の応用
5.5 完全正当性のための推論規則
第6章 表示的意味論
6.1 算術式の表示的意味
6.2 ブール式の表示的意味
6.3 プログラムの意味
第7章 λ計算
7.1 構文
7.2 代入と簡約
7.3 λ計算の表現力
7.4 簡約戦略と関数型言語
第8章 型つきλ計算
8.1 単純型つきλ計算
8.2 型推論
8.3 ML多相
参考文献
演習問題の解答
索引