一昨日定義した極小プログラミング言語を、TTPL（Tiny Toy Programming Language）というツマンネー名前で呼ぶことにします。
んでまー、TTPLをああいう仕様にしたのは、ホーア論理を直接的に使いたい、という理由があります。つうわけで、ホーア論理をTTPLを使って説明します。ただし、最初に言っておきますが、僕は（ホーア論理のような）プログラム証明を推奨する気はありません（どっちかいうと反対派）。それでも、理屈は知っておかないと、それから先に進めないってことはあります。
内容：
- ホーア式
- ホーア式の正しさ
- プログラムの証明
- こんなにめんどくさい
- なにが重要か
●ホーア式
ホーア論理の式（ホーア式とか、ホーア・トリプルと呼ばれる）は、プログラムの文と仕様記述を一緒にしたようなものです。p, qが論理式（条件）でSが文だとして、p{S}q という形で書きます。中括弧の使い方が逆である {p}S{q} が一般的かと思いますが、僕は p{S}q を使ってますね。理由：
- 多くのプログラミング言語では、文を囲むために中括弧を使っている。
- ホーア自身が最初に使っていた記法が p{S}q だった（とメイヤーが書いている）。
ホーア式の例（4つ）：
var x:Number;/*(1)*/ (x >= 0){x = x + 1}(x > 0)
/*(2)*/ (x >= 0){skip}(x > 0)
/*(3)*/ (x >= 0){hang}(x > 0)
/*(4)*/ (x > 0) {
var y:Number = 1;
var z:Number = 0;
while (z < x) {
z = z + 1;
y = y * z;
}
}(y == factorial(x))
●ホーア式の正しさ
ホーア式 p{S}q が正しいとは：
- 条件pが成立しているとき、Sを実行して正常終了すれば、必ず条件qも成立している。
注意すべきは：
- 条件pが成立していないなら、問答無用にホーア式は正しい。例えば x == -1 のとき、(x >= 0){skip}(x > 0) は正しいホーア式である。
- 文Sが正常終了しないなら、条件qが何であってもホーア式は正しい。条件qがチェックされるのはSが正常に終了した場合に限る。例えば、(x >= 0){hang}(x > 0) は、x == 0 のときも（その他どんなときでも）正しい。
この「正しさ」の基準は、どうも生ぬるい、厳しさが足りない印象がありますが、まー、こんな程度で妥協してください。
ホーア式はプログラムではありませんが、“ホーア式の正しさを表現するプログラム”は書けます。p{S}q に対して次のコードを考えます。
var result:Boolean;
if (p) {
S;
if (q) {
result = true;
} else {
result = false;
}
} else {
result = true;
}
このresultがtrueなら、p{S}q が正しいことになります。ただし、「p{S}q が正しい」ことと「resultがtrue」は同じではありません。Sが無限走行するかもしれないので、「p{S}q が正しい」⇔「resultがtrueとなるか、またはプログラムが正常終了しない」となります。
●プログラムの証明
ホーア式 p{S}q に対して真偽値resultを返すコードを仮にチェッカーコードと呼ぶことにします。すると、次の3つは同じことです。
- ホーア式 p{S}q が正しい。
- 文Sが期待した動作をする（ただし、停止することは保証されない）。
- p{S}q のチェッカーコードがtrueを返すか、または正常終了しない。
ホーア式の正しさは、（原理的には）チェッカーコードを走らせれば確認できます。しかし、停止する保証がないし、停止する場合でも、パラメータを変えて何度も（事実上、無限回かもしれない）チェッカーコードを走らせるのは大変です。そこで、実行をせずにホーア式の正しさを確認できないか？ ってことになります。
プログラムを実行せずにその正しさを確認する手段がプログラム証明です。次を例にします。
上のコードをSとして、(true) {S} (y == n ÷ m) というホーア式を証明します。「÷」は整数の範囲での割り算です。n, mの値によりSが止まらないこともありますが、今は停止する／しないは気にしないことにします。
/* n:Number と m:Numberは外から与えられる */
var x:Number = n;
var y:Number = 0;
while (x >= m) {
x = x - m;
y = y + 1;
}
実際に証明をやってみると、僕が（そして多くの人が）プログラム証明を推奨しない理由がわかるでしょう -- めんどくさいんですよ。どのくらいめんどくさいかを知るためにはやってみないとね。
●こんなにめんどくさい
ここでは、通常の説明とは異なりますが、逆向きの証明（分解・還元、タブロー）の形で示します（たぶん、そのほうが分かりやすいと思うので）。混乱を避けるために、条件の部分をプログラムとは異なった構文で書きます。
最初に方針を言っておくと、結論（事後条件）「y＝n÷m」の一部を変数xを使って「m×y＋x＝n」の形にしておいて、この条件がwhileループの入り口から出口までずっと成立していることを示します。
whileの手前をS1、while文をS2として、Sに関するホーア式を次のように分解します。
- (true){S1}(m×y＋x＝n)
- (m×y＋x＝n){S2}(x＜m ∧ m×y＋x＝n)
1番目は、{x = n; y = 0}の実行後なら(m×y＋x＝n)とは(m×0＋n＝n)を意味するんだからOKですね。2番目を導くには、(m×y＋x＝n ∧ x≧m){x = x - m; y = y + 1}(m×y＋x＝n) を示せばいいのだけど、これはしばらく眺めていると、ホントらしいと分かるでしょう。
さてと、whileのなかの文{x = x - m; y = y + 1}をS3とすると：
- S ≡ S1;S2
- S2 ≡ while(x≧m){S3}
と、SがS1, S2, S3へと分解・還元できて、この分解・還元に沿って逆向きの証明を書き下すと次のような感じ。
(true) {S} (y＝n÷m)
-------------------------↓y＝n÷m を書き換える。
(true) {S} (x＜m ∧ m×y＋x＝n)
-------------------------↓SをS1;S2と分解する。
(true) {S1;S2} (x＜m ∧ m×y＋x＝n)
-----------------------------------↓推論規則によりホーア式も分解する。
(true){S1}(m×y＋x＝n) ｜(m×y＋x＝n){S2}(x＜m ∧ m×y＋x＝n)
-----------------------
これ（S1のほう）はいいとしよう。問題はこれ(↓)だった。
(m×y＋x＝n){S2}(x＜m ∧ m×y＋x＝n)
------------------------------------↓S2をwhile(x≧m){S3}に還元する。
(m×y＋x＝n){while(x≧m){S3}}(x＜m ∧ m×y＋x＝n)
------------------------------------↓推論規則によりホーア式も還元する。
(m×y＋x＝n ∧ x≧m){S3}(m×y＋x＝n)
------------------------------------
これ（S3）もいいとしよう。
「推論規則により」、「いいとしよう」ってところが実は問題だけど、今回は雰囲気でいいや。推論規則そのものはWikipediaとかにも記載されています。今やったのは、証明したいホーア式（結論）からはじめて、より明らかなホーア式に持ち込むような方法ですが、これを逆に（下から上に）たどっていけば、通常の（仮定から結論に向かう）証明になります。
●なにが重要か
これで、例に挙げたプログラムコードSが、整数割り算の答え（商）を求めることが確認できました（って、あんまり確認できてないような）。ご覧のとおりの手間なので、プログラム証明を実用的に使うのは無理でしょう。でも、次のようなことは知っておいていいと思います。
- プログラムの実行によって手に入れたい目的物（計算結果）は、ホーア式の結論（事後条件）として記述できる。
- プログラムの実行に先だって必要な要求物（適切な環境）は、ホーア式の前提（事前条件）として記述できる。
- 正しいプログラムは、前提（事前条件）が満たされている環境で走って停止したならば、結論（事後条件）を満たさなくてはならない。
- さらに、前提（事前条件）が満たされているなら、必ず停止するのが望ましい。
