Preface: 前書き
この本はプログラムとプログラミング言語に対する数学的基礎の基本的コンセプトをまとめたものです。
主な内容は、Coqの高度な利用方法、操作的意味論、ホーア論理、静的型システムです。
解説は、学部生から博士課程の学生や研究者に至るまで、広範囲の読者を想定しています。
論理学やプログラミング言語についての知識は仮定しませんが、ある程度の数学的素養は理解に有用です。
他の「ソフトウェアの基礎」シリーズと同様、ここで取り扱う内容もすべて形式化されて、さらに機械によって確かめられています。
これは、それぞれのテキストがCoqのスクリプトファイルそのものとなっていることで実現されています。
このシリーズでは、Coqのインタラクティブモードを横で動かしながら（またはエディタで一行ずつ進めながら）読み進めることを想定しています。
内容の細部まですべてCoqで形式化され、また演習もCoqを使って行うように設計されています。
内容としては、主要部とそれ以外の「派生」からなります。
主要部は1学期分の講義として十分な量が、順序だって記述されています。
また、派生部分は主要部に関連する項目をカバーしています。
主要部は学部後半の学生や院生にちょうどいい内容でしょう。
この本は、「論理の基礎(Logical Foundations)」（「ソフトウェアの基礎」第一巻）を基本としています。
これと合わせて、プログラミング言語の理論に関する一学期分の講義ができると思います。
また、「論理の基礎」の内容に既に馴染んでいる学生向けには、この本の派生部を利用して単体で講義を構成できるでしょう。
この本は二つの主題があります。
(1) 「特定のプログラムの仕様の推論」に関する形式手法
（例：ソート関数やコンパイラが形式仕様を満たす）
(2) あるプログラミング言語で書かれた「全ての」プログラムの挙動を保証する「型システム(type system)」
（例：Javaの型付けされたプログラムは実行時に型が原因で止まったりしない）
これらはそれぞれ単体でも講義を構成できるほど豊富な内容を含んでいるので、両方を同時に進めるということは言及しない部分があるということでもあります。
それでも、皆さんが、これらのテーマ同士が互いに関連して理解を深め、その全体像がそれぞれをより深く掘り進めるための基礎となることに気づいてくれれば幸いです。
この本の後に読むとよい資料については、Postscriptの章に記載しています。
これらの本の参照情報はBibファイルにあります。
この本の前半ではまず、高信頼ソフトウェア（またはハードウェア）を構築するのに非常に重要な二つの内容に関して述べます。
一方は「プログラム」における特定の性質の証明、そしてもう一方は「プログラミング言語」における一般的性質の証明です。
このどちらも、まず最初にすることはプログラムを数学的対象として正確に表現することです。
これにより、プログラムについて正確な議論をできるようになります。
加えて、数学における関数や関係(relation)によってその動作を記述することもできます。
プログラミング言語を数学的対象として表現するために、「抽象構文(abstract syntax)」と「操作的意味論(operational semantics)」を用いて抽象解釈器を記述します。
初めはまず、いわゆる「大ステップ("big-step")」形式の操作的意味論を使います。
これは利用可能な範囲では単純で読みやすい定義になっています。
その後、より細かな「小ステップ("small-step")」形式に移行します。
これはプログラムの区別に有用で（例えば「異なる要因で終了しない」プログラムの区別）、また並行性など広範の言語機能に対応できます。
最初に対象とするプログラミング言語は、 Imp と呼ばれる非常に小さな、おもちゃのような言語ですが、命令型プログラミングの核となる機能を持っています。
変数、代入、条件分岐、そして繰り返しです。
この本では、Impプログラムに対して、二つの観点で性質を解釈していきます。
一つ目は、Impプログラムの任意の初期状態に対する振る舞いが同じか、という直観的な意味で「等しい(equivalent)」か、というものです。
この観点は、「メタプログラム(metaprogram)」に対する正当性の基準につながります。
メタプログラムとは、他のプログラムを操作するプログラムのことで、例えばコンパイラや最適化器があります。
この本では、Impへの簡単な最適化器を作り、それが正しいことを示します。
二つ目は、与えられたImpプログラムの振る舞いがある形式仕様を満たすか、というものです。
これを記述するために「ホーアの三つ組(Hoare triple)」を導入します。
ホーアの三つ組は、Impプログラムと、事前条件、事後条件の三つで構成されていて、事前条件を満たす状態から始めてImpプログラムを実行すると、終了するなら終了時の状態は事後条件を満たす、ということを表します。
また、ホーアの三つ組について論じる「ホーア論理(Hoare Logic)」を導入します。
ホーア論理は命令型プログラムの合成的検証に特化した領域特化論理(domain-specific logic)であり、「ループ不変条件("loop invariant")」などの概念が組み込まれています。
この部分では、実世界のソフトウェアやハードウェアの検証に広く利用されるアイディアと数学の道具を経験してもらいます。
この本の後半で述べるもう一方の主題は「型システム(type system)」です。
これは、導入した言語の全てのプログラムに対する性質を保証する強力な道具です。
型システムは形式検証技術の中でも「軽量形式手法(lightweight formal method)」と呼ばれるものの一つで、大きな成功を納めています。
形式検証としては、型システムの保証する性質は控えめですが、その控えめさ故に自動検査としてコンパイラやリンカや解析器に組み込め、またその理論に精通していない人にも使いやすいものとなっています。
他の軽量形式手法としてはハードウェアやソフトウェアのモデル検査器(model checker)や契約検査器(contract checker)、実行時モニタリング手法などがあります。
ここまで来るとこの本の最初の目標に戻ってきます。
ここでは「単純型付きラムダ計算(simply typed lambda-calculus)」と呼ばれる言語について学びます。
これはCoqの核をさらに単純化したものなのです。
この本は単体で読めるようにしてありますが、それぞれの内容でより進んだ話を見たければ、Postscript章に挙げた参考文献を見ると良いでしょう。
この資料を自分のコースで使おうと思った場合、ほぼまちがいなく書き直しや追加したいところが出てくるでしょう。
そういった貢献は大歓迎です。
「論理の基礎(Logical Foundations)」のPreface章にある案内を見てください。