第13回 「表明」と「契約」による命令型プログラムの形式的検証

　この連載では，OCamlやλ計算など，いわゆる関数型言語を中心に，プログラミング言語理論に関連する話題を紹介してきた。λ計算などの関数型言語は，クロージャや型推論といった高度な機構を簡潔に議論することができるので，基礎研究では非常に便利だ。第10回や第12回に出てきたMyFun言語も，実はλ計算の一種だ（MyFun言語の「fun x -> 式」が，λ計算の「λx. 式」にあたる）。

　しかし，プログラミング言語理論の研究者も，関数型言語ばかり研究しているわけではない。現存する最古の高級プログラミング言語であるFortranは命令型言語だし（Fortranの直後に登場したLispは関数型言語だが），そもそも現代のコンピュータの機械語は，ほぼすべて命令型言語だ。命令型言語の研究をしないわけがない。

　実際に，命令型言語に関する理論は数多い。その中でも命令型プログラムの仕様を記述・証明する「ホーア論理」は特に有名だ。今回はホーア論理とその応用について紹介する。

歴史的背景

　ホーア論理の内容を説明する前に，歴史的背景について触れておこう。ホーア論理は，クイックソートで有名なトニー・ホーア卿により，1960年代後半に提案された。ただし，ホーア論理の元となったアイディアは，その少し前にロバート・フロイド氏（グラフ理論における「フロイドのアルゴリズム」で有名）により提案されたという。

　両氏とも，これらの理論を中心とする複数の業績により，計算機科学のノーベル賞とされる「チューリング賞」を受賞した（参考リンク1，参考リンク2）。ホーア卿は，第16回京都賞も受賞している（参考リンク1，参考リンク2）。

　ちなみに，ホーア「卿」というのは，氏が2000年にナイトの称号を授与され，敬称が“Sir”となったためだ。ホーア卿は現在も存命で，オクスフォード大学名誉教授およびマイクロソフト研究所（ケンブリッジ）上級研究員を勤めている。フロイド氏は，2001年に65歳で死去した。

　このように，ホーア論理自体はもはや歴史的・古典的とも言えるぐらい古い研究だ。しかし，その実用化への道のりは長く，最近になって，ようやく可能性が見えてきた感がある。そのような意味で，ホーア論理（およびホーア論理を発展させた理論）の重要性は再注目すべき段階にあると言えるかもしれない。

ホーア論理の基本：「事前条件」と「事後条件」

　ホーア論理の基本となるのは，{P}C{Q}という形の式だ。この式は，「条件Pが成立するときに，プログラムCを実行して停止したら，条件Qが成立する」ことを表す。このような式のことをホーアの三つ組（Hoare triple）という。

　また，条件Pのことを事前条件，条件Qのことを事後条件という。PやQのような条件のことを表明（assertion）という。これはC言語のassertマクロなどでおなじみだろう。さらに，あるプログラムの事前条件と事後条件を合わせて，そのプログラムに関する契約（contract）という。これはEiffelというプログラミング言語の「契約プログラミング」という概念で有名だ（関連記事）。

　例えば，プログラムCとして「x = y + z」という，簡単な足し算と代入を考えてみよう。すると，例えば下のようなホーアの三つ組はすべて成り立つ。いずれも，Pの部分が成り立っている状態で「x = y + z」を実行すれば，Qの部分が成り立つからだ。

 { y == 1 ∧ z == 2 } C { x == 3 }

 { y ≧ 0 ∧ z ≧ 0 } C { x ≧ 0 }

 { 0 ≦ y ≦ 10 ∧ 0 ≦ z ≦ 10 } C { 0 ≦ x ≦ 20 }

 { 0 ≦ y ≦ I ∧ 0 ≦ z ≦ J } C { 0 ≦ x ≦ I + J }

　ただし，∧は「かつ」を表す論理記号だ。また，最後の例でのIとJは，任意の整数を表すものとする。xやyのようなプログラム中の変数とは別なので注意してほしい。

　ホーア論理は，このような「事前条件が成立する状態でプログラムを実行したら事後条件が成立する」という性質を，数学的な証明により形式的に検証することを目標としている。もしそれができれば，いわゆるテストによるデバッグよりも強力な検証が可能になる。テストではあくまで有限の場合しか確認できないが，数学的証明による形式的検証ができれば，無限のケースを一度にチェックできるからだ。例えば上述の最後の例だったら，
　(I, J)が(0, 0)の場合，(1, 0)の場合，(0, 1)の場合，(1, 1)の場合…
などと順に試すのではなく，任意の(I, J)について証明するわけだ。

　そのような証明は一般には「決定不能問題」といって，全自動では不可能であることが昔から知られている。そのためか，ホーア論理は実用にならないと考えられた頃もあったらしい。しかし，最近になって，いわゆる定理証明器の研究が発展し，意外と様々なプログラムの性質について全自動ないし半自動の検証が可能だとわかってきた。実際に，JavaやCなどのプログラムについて，ホーア論理の一種に基づいて形式的検証を行うためのツールも現われている（参考リンクなど）。

簡単な命令型言語のためのホーア論理

　さて，事前条件PとプログラムCと事後条件Qが与えられたとして，{P}C{Q}が成立するかどうかを検証するためには，何をどうすれば良いのだろうか。実はここでも第9回（命令型言語MyCのインタプリタ）で触れた，「プログラムCの形に従って場合わけと再帰をする」という考え方が有効だ。説明のために，Cは以下のいずれかの形の文であるとしよう（特定の命令型言語ではなく，適当な文法を使用する）。

Cが「x = 式」のような代入文の場合

　ただし，右辺の「式」には副作用がないとする。

　この場合，Cを実行した後に条件Qが成り立つためには，Cを実行する前に「Qの中のxを右辺の式でおきかえた条件」（Q'とする）が成立していれば良い。つまり，「P ⇒ Q'」であることを証明すれば良い（⇒は「ならば」を表す論理記号）。

　例えば，事前条件Pが「y == 1 ∧ z == 2」，プログラムCが「x = y + z」，事後条件Qが「x == 3」だったとしよう。すると，Q'は「y + z == 3」になるから，P ⇒ Q'は「(y == 1 ∧ z == 2) ⇒ y + z == 3」となり，確かに成り立つ。よって，{P}C{Q}も確かに成り立つといえるわけだ。

Cが「文1 ; 文2」のような複合文の場合

　この場合は，まず文2について，「文2を実行する前に成り立っているはずの条件」Q'を求める。そこから，さらに文1について，「文1を実行する前に成り立っているはずの条件」Q''を求める。その上で，「P ⇒ Q''」が成り立っていることを確かめれば良い。

　例えば，次のようなホーアの三つ組を考えよう。

 { x == I } x = x + x; x = x + 1 { x == I * 2 + 1 }

　ただし，Iは先と同じく，任意の整数とする。この例では，x == I * 2 + 1が事後条件Qにあたる。まず，x = x + 1（文2にあたる）を実行する前に成り立つはずの条件Q'は，x + 1 == I * 2 + 1となる。これは先に述べた代入の場合からわかる。次に，x = x + x（文1にあたる）を実行する前に成り立つ条件Q'' は，(x + x) + 1 == I * 2 + 1となる。これも代入の場合からわかる。すると，全体としては「P ⇒ Q''」つまり「x == I ⇒ (x + x) + 1 == I * 2 +1」を検証すればOKということになる。これは確かに常に成り立っている。

Cが「if 式 then 文1 else 文2」のような条件文の場合

　ただし，ifの条件の「式」には副作用がないとする。

　まず文1について，「式」が真だった場合に，文1を実行する前に成り立っているはずの条件Q'を求める。さらに文2について，「式」が偽だった場合に，文2を実行する前に成り立っているはずの条件Q''を求める。すると，if文全体を実行する前に成り立っているはずの条件は，「(式∧Q')∨(￢式∧Q'')」と表される（∨は「または」を，￢は「否定」を表す論理記号）。「式」が真の場合はQ'が成り立つはずだし，「式」が偽の場合はQ''が成り立つはずだからだ。

　したがって，全体としては「P ⇒ (式∧Q')∨(￢式∧Q'')」が成り立つかどうかを検証すれば良い。

　例えば，次の例を考えよう。

 { xは整数 } if xは奇数 then x = x + 1 else x = x + 2 { xは偶数 }

　「x = x + 1」が文1に，「x = x + 2」が文2にあたる。if文全体の事後条件Qは「x は偶数」だから，文1を実行する前に成り立つべき条件Q'は「x+1は偶数」となる。また，文2を実行する前に成り立つべき条件Q''は「x+2は偶数」となる。したがって，if文全体を実行する前に成り立つべき条件は，「(xは奇数∧x+1は偶数)∨(xは偶数∧x+2は偶数)」となる。xが整数ならば，これは確かに常に成り立つ。

Cが「while 式 do 文」のような反復文の場合

　これも，（whileの条件である）「式」には副作用がないとする。

　実は，このケースがもっとも難しい。「文」の部分が何回実行されるか，一般には予測不能だからだ。そこで，whileなどの反復があるプログラムの場合は，反復の回数にかかわらず常に成り立つ不変条件を（通常は人間が）指定する必要がある。その不変条件をRとしよう。すると，Rが本当に適切な不変条件かどうか，以下のように確認することができる。

　まず，while文全体が実行される前と後の条件PとQについて，「P ⇒ R」と「(R ∧ ￢式) ⇒ Q」が成立することを検証する。「P ⇒ R」は，while文全体が実行される前に，Pが成り立っていれば，Rが成立することを意味する。

　「(R ∧ ￢式) ⇒ Q」は，while文全体が終了したときに，Rが成り立っていれば，Qが成立することを意味する。「while文全体が終了したとき」という前提なので「￢式」が付いているわけだ。

　また，それとは別に，（whileの本体である）「文」の後でRが成り立つためには，「文」の前でR'が成り立てば良いはずだ，という条件R'を計算する。その上で，「(R ∧ 式) ⇒ R'」が成り立つことを確かめる。そうすれば，Rと「式」が成立している状態（つまりR'が成立している状態）で「文」を実行したら，再びRが成り立つことになる。つまり，「式」が成り立っている限り，「文」が何回実行されようと，Rは成り立つといえる。

　一般論だけではわかりにくいと思うので，具体例を考えてみよう。下のようなプログラムを考える。

 while (x ≠ 0) do (s = s + x; x = x - 1)

　これは，1からxまでの整数の総和を計算する（つもりの）プログラムだ。このプログラムが実際に総和を計算することを証明するために，次のようなホーアの三つ組を考えよう。

 { x == I ∧ s == 0 }
 while (x ≠ 0) do (s = s + x; x = x - 1)
 { s == 1 + 2 + 3 + ... + I }

　これが成り立つことを示すには，どうすれば良いだろうか。上で述べたように，一般にwhile文についての証明を行う場合は，不変条件Rを指定する必要がある。ここでは，不変条件Rとして，次のような式を考えてみよう。

 s == (x + 1) + (x + 2) + (x + 3) + ... + I

　このRに対して，上で述べた，いくつかの条件を確認すればOKのはずだ。

　まず，「P ⇒ R」つまり「(x == I ∧ s == 0) ⇒ R」は明らかに成り立つ。xがIならば，(x + 1) + (x + 2) + (x + 3) + ... + Iという列は空なので，和も0になるからだ。次に，「(R ∧ ￢式) ⇒ Q」つまり「(R ∧ x == 0) ⇒ s == 1 + 2 + 3 + ... + I」を確かめる。これも，xが0ならば，条件Rより，sは1 + 2 + 3 + ... + Iとなるので明らかだ。

　一方，whileの本体である「文」つまり「s = s + x; x = x - 1」を実行した後でRが成り立つためには，どのような条件R'が「文」を実行する前に成り立てば良いはずだろうか。「s = s + x; x = x - 1」は代入文の複合文だから，前述の代入文および複合文の場合に従おう。Rの中のxをx-1で置き換え，それからsをs+xで置き換えると，R'は以下のような条件になる。

 s + x == x + (x + 1) + (x + 2) + ... + I

　このR'に対し，「(R ∧ 式) ⇒ R'」つまり「(R ∧ x ≠ 0) ⇒ R'」を証明すれば良い。これはRとR'の定義より，明らかに成立する。

　以上により，事前条件「x == I ∧ s == 0」が成り立つ状態で，プログラム「while (x ≠ 0) do (s = s + x; x = x - 1)」を実行して停止したら，事後条件「s == 1 + 2 + 3 + ... + I」が成り立つことが証明できた。

ホーア論理の拡張

　さて，以上の説明では，{P}C{Q}は「条件Pが成立するときに，プログラムCを実行して停止したら，条件Qが成立する」という意味だと定義した。しかし，{P}C{Q}自体は，プログラムが停止することは保証しない。実際に，while文の例でも，もしIが負だったら（整数アンダーフローが起こらない限り）プログラムが止まらない。プログラムが停止することも証明したい場合は，ホーア論理を拡張するか，別個の解析が必要になる。プログラムの停止性判定も，一般には典型的な決定不能問題だが，最近の研究の進展により，様々な場合について全自動ないし半自動の証明が可能になりつつある。

　また今回は，代入文・複合文・条件文・反復文の4種類しか構文がない，非常に単純な命令型言語を想定してホーア論理を紹介した。しかし，当然ながら現実のプログラミング言語には，関数やポインタなどの機構もある。関数については事前条件・事後条件の考え方を応用すれば，比較的単純に取り扱うことが可能だが，問題はポインタだ。

　例えば，次のような（C言語風の）関数を考えよう。

 int f(int *p, int *q) {
   *p = 1;
   *q = 2;
   return *p + *q;
 }

　この関数の返り値はいくつになるだろうか？ 素朴に考えれば，*pは1に，*qは2になるので，1+2で3になると思いたくなる。しかし，もしpとqが同じメモリー領域を指していたら，*q = 2により*pも上書きされて，返り値は2+2で4になる。あるいは，pかqのいずれかが無効なメモリー領域を指していたら，（C言語の仕様では）プログラムの動作が全く不定になってしまう。

　このような困難があるために，ホーア論理などによる形式的検証にとって，ポインタは一種の「鬼門」だった。が，最近になって，ポインタを使用するプログラムも検証できるようにホーア論理などを拡張する研究が進展し，OSやメモリー管理ライブラリの検証などにも応用されつつある（参考リンク1，参考リンク2など）。