ソフトウェアの基礎(beta)¶

本ドキュメントは実験中のものです。安定板は http://proofcafe.org/sf/ を参照してください。

epub版: http://proofcafe.org/sf-beta/software_foundation_1.0.2.epub

mobi版: http://proofcafe.org/sf-beta/software_foundation_1.0.2.mobi

Contents:

前書き
- 概要
- 実際の学習について
- Coqについて
- 練習問題について
- 推奨書籍
- 教育関係者へ
Basics_J: 関数プログラミングとプログラムの証明
- 列挙型
- 簡約を用いた証明
- introsタクティック
- 書き換え（Rewriting）による証明
- Case分析
- Caseへのネーミング
- 帰納法
- 形式的証明と非形式的証明
- 証明の中で行う証明
- さらなる練習問題
Lists_J: 直積、リスト、オプション
- 数のペア
- 数のリスト
- リストに関する推論
- オプション
- applyタクティック
- 帰納法の仮定を変更する
- 練習問題: 辞書
Poly_J:多相性と高階関数
- ポリモルフィズム（多相性）
- データとしての関数
- さらにCoqについて
- まとめ
- さらなる練習問題
Gen_J: 帰納法の仮定の一般化
- 練習問題: ★★★ (gen_dep_practice)
- 練習問題: ★★★, optional (index_after_last_informal)
- 練習問題: ★★★, optional (gen_dep_practice_opt)
- 練習問題: ★★★, optional (app_length_cons)
- 練習問題: ★★★★, optional (app_length_twice)
Prop_J: 命題と根拠
- 命題によるプログラミング
- 根拠
- 全体像: Coqの2つの空間
- 非形式的な証明
- 選択課題
- 追加練習問題
Logic_J: Coqにおける論理
- 全称記号とならば
- 論理積、連言（Conjunction、AND）
- 論理和、選言（Disjunction、OR）
- 偽であるということ
- 否定
- 存在量化子
- 等しいということ（同値性）
- 命題としての関係
- 選択課題
Rel_J:関係の性質
- 関係の基本性質
- 反射推移閉包
SfLib_J: Software Foundations ライブラリ
- Coq スタンダードライブラリから
- Basics.vから
- Props.vから
- Logic.vから
- 使い勝手のいいタクティックをいくつか
Imp_J: 単純な命令型プログラム
- Sflib
- tryタクティカル
- ;タクティカル
- 場合分けを万全にする
ImpParser_J: Coqでの字句解析と構文解析
- 内部処理
- 例
Equiv_J: プログラムの同値性
- 宿題割当てについての一般的アドバイス
- (0 + n)の消去の健全性、再び
ImpList_J: Imp のリスト拡張
- リストを持つ Imp プログラム
Hoare_J: ホーア論理
- ホーア論理
- ホーア論理によるプログラムについての推論
- 修飾付きプログラムの形式化
HoareAsLogic_J: 論理としてのホーア論理
- 練習問題: ★★
Smallstep_J: スモールステップ操作的意味論
- おもちゃの言語
- マルチステップ簡約
- スモールステップ Imp
- 並列実行 Imp
Types_J: 型システム
- さらに自動化
- 型付きの算術式
Stlc_J: 単純型付きラムダ計算
- 単純型付きラムダ計算
- 練習問題: 算術を持つSTLC
Typechecking_J: STLCの型チェッカ
- 型を比較する
- 型チェッカ
- 性質
MoreStlc_J: 単純型付きラムダ計算についてさらに
- STLCの単純な拡張
- 拡張を形式化する
Records_J: STLCにレコードを追加する
- レコードを追加する
- レコードを形式化する
References_J: 変更可能な参照の型付け
- 定義
- 構文
- 副作用と順次処理
- 参照と別名付け
- 共有状態
- オブジェクト
- 参照と合成型
- null参照
- ガベージコレクション
- 場所(Locations)
- 記憶(Stores)
- 簡約
- 記憶の型付け
- 型付け関係
- 型付けできる記憶
- 記憶型付けを拡張する
- 保存、最終的に
- 置換補題
- 代入は記憶型付けを保存する
- 記憶についての弱化
- 保存!
- 進行
Subtyping_J :サブタイプ
- 概念
- 中核部の定義
- サブタイプ
- 型付け
- 性質
- 練習問題: 直積の追加
RecordSub_J: レコードのサブタイプ
- 中核部の定義
- サブタイプ
- 型付け
Norm_J: STLCの正規化
- 練習問題: ★
UseTactics_J:Coq用タクティックライブラリのご紹介
- 導入と場合分けについてのタクティック
- n-引数論理演算のためのタクティック
- 等式を扱うタクティック
- 注記:asserts_rewrite (E1 = E2) in Hと書いた場合、
- 便利な略記法をいくつか
- 高度な補題具体化のためのタクティック
UseAuto_J: Coqの証明自動化の理論と実際
- 証明探索の基本性質
- 証明探索はどのようにはたらくか
- 自動化の使用例
- 証明探索の進んだ話題
- 決定手続き
LibTactics_J: 使いやすい汎用タクティックのコレクション
- Coqのための追加の記法
- Ltacによるプログラミングのための道具類
- 後方/前方連鎖
- 導入と一般化
- 書き換え
- 反転(Inversion)
- 帰納法(Induction)
- 決定可能な等式
- 同値(Equivalence)
- N個の連言と選言
- タイプクラスのインスタンスを証明するためのタクティック
- 自動化起動のタクティック
- 証明コンテキストを整理するためのタクティック
- 開発目的のタクティック
- 標準ライブラリとのコンパチビリティ
PE_J: 部分評価
- 定数畳み込みを一般化する
- ループ以外のコマンドの部分評価
- ループの部分評価
- フローチャートプログラムの部分評価
Postscript_J: あとがき
- ふりかえり...
- さらなる読み物

Indices and tables¶