かじもとにっき

ゆるふわなおはなしをかきます

Assertの話(1)

これはDelphi Advent Calendar 2013 - Qiitaの五日目用の記事です。

Delphi使いの皆様、System.Assert手続きは活用されていますか?もちろんされていますよね。今回はそんなAssertに関連する話を少しだけ詳しく書いていきます。
具体的には、表明(assertion)とは何かというところから始めて、証明の道筋に沿ったプログラムの記述方法、ルーチン本体の事前条件と事後条件がルーチンとその呼び出し側との契約になっていると言う話等を通し、最終的にはabstract datatypeとしてのクラスとdesign by contractの関係、Liskov substitution principleを保証する方法あたりに着地するかと思います。
全十回くらいで終われば良いなあ。

プログラムの正しさ

プログラムが何を成すかということを記述したものを仕様、その仕様を満たすプログラムのことを実装と言います。あるプログラムが正しいという場合、普通は対象のプログラムがその仕様を満たしていることを意味しています。すなわちプログラムの正しさとは、その仕様に対して決まる相対的な概念だと考えられます。
そしてプログラムの仕様はプログラマの意図を出来るだけ明確に表現したものであることが望ましいので、形式的な仕様を記述する為に便利な記法をいくつか導入しておきます。
まず、プログラムの事前条件と事後条件を表すのにHoare tripleと呼ばれる記法を導入します(実際の所、HoareはP\{S\}Qと言う記法でプログラムの部分正当性を表現しました。一方ここで定義する記号はプログラムの全正当性を表していますが、今回その辺の話は省略します)。

定義

Sが述語Pが満たされる任意の状態で実行された時、有限時間のうちに述語Qが満たされる状態で終了することが保証されるという主張を、
\{P\}S\{Q\}
と書く。
ここで、PSの事前条件、QSの事後条件と言う。

ただし\{P\}S\{Q\}と言う記法では、変化する変数が示されていないため、プログラムの仕様としては不十分です。そこで、代入される可能性のある変数のリストをxとし、\{P\}x:=?\{Q\}でプログラムの仕様を示すことにします。
続いて計算上便利なように、事後条件に対する最弱事前条件を表す為の記号を導入します。これはDijkstraによって考案された述語変換子wpと同じものです。

定義

Sの実行が状態Qを満たして終了するような最弱事前条件を\omega_SQと書く。

ここで、P\Rightarrow\omega_SQ\{P\}S\{Q\}は同値です。
ところで、falseを満たす状態に達して終了するような文は存在しないはずなので、これを\omegaに関する公理の一つとします。

公理 奇蹟排除律

\omega_Sfalse=false

今、状態t\omega_SP\wedge\omega_SQを満たしていると仮定します。Sの実行をtから開始すると、PQの両方を満たします。従って、t\omega_S(P\wedge Q)を満たします。逆に、t\omega_S(P\wedge Q)を満たすとします。この時、Sの実行をtから開始すると、P\wedge Qを満たす状態t'で終了します。従って、t'PQも満たすから、t\omega_SP\omega_SQも満たします。このことも公理として採用することにします。

公理 論理積上の分配律

\omega_SP\wedge\omega_SQ=\omega_S(P\wedge Q)

次の2つの定理が成り立ちます。

定理 単調律

(P\Rightarrow Q)\Rightarrow(\omega_SP\Rightarrow\omega_SQ)

証明

\omega_SP\Rightarrow\omega_SQ \\ \Leftrightarrow \omega_SP\wedge\omega_SQ=\omega_SP \\ \Leftrightarrow \omega_S(P\wedge Q)=\omega_SP \\ \Leftrightarrow \omega_SP=\omega_SP \\ \Leftrightarrow true

定理 論理和上の半分配律

\omega_SP\vee\omega_SQ\Rightarrow\omega_S(P\vee Q)

証明

P\Rightarrow P\vee Qより\omega_SP\Rightarrow\omega_S(P\vee Q)が、Q\Rightarrow P\vee Qより\omega_SQ\Rightarrow\omega_S(P\vee Q)がそれぞれ成り立つ。以上から、\omega_SP\vee\omega_SQ\Rightarrow\omega_S(P\vee Q)が従う。

論理積上の分配律では右辺と左辺が同値によって結ばれているのに対し、こちらは含意で結ばれていることに注意して下さい。これは、指令の実行が非決定性を持つ可能性があるからです。非決定性とは、同じ状態から実行を開始しても、同じ状態で実行が終了することが保証されないことを意味します。

系 論理和上の分配律

Sが決定性を持つ時、
\omega_SP\vee\omega_SQ=\omega_S(P\vee Q)

プログラミング言語の形式的定義

話の都合上、\omegaに基づいてDelphi言語そのものよりは数学的に扱いやすい簡易言語を定義していきます。
まず、skip文を定義します。これはDelphiでの空文に相当します。記述の都合上skipと言う名前を与えました。

定義

\omega_{skip}P=P

\omega_{skip}が述語の恒等変換となっていることに注意して下さい。

定義

\omega_{halt}P=false

halt文は、そこに到達した時点でプログラムの実行を放棄することを意図しています。falseを満たすような状態は存在しないので、この文を実行することは絶対にできないからです。Delphiにおいては、System.Halt手続きがhalt文に相当します。\omega_{halt}が定数値関数であることに注意して下さい。

定義

\omega_{S;T}Q=\omega_S(\omega_TQ)

S;Tは、文Sと文Tを順次実行するような文を意図しています。これはDelphiでの複合文に相当します。
明らかに、次の結合律が成り立ちますので、(S;T);US;(T;U)を単にS;T;Uと書くことにします。

定理 結合律

\omega_{(S;T);U}P=\omega_{S;(T;U)}P

証明

関数合成の結合律から明らか。

Delphiとの対応

仕様\{x=X\wedge y=Y\}x,y:=?\{x=Y\wedge y=X\}を満たすプログラムを考えてみましょう。ここで、大文字のXYは、単に変数の初期値を参照する為に導入した固定変数です。
さて、この仕様を満たす実装として、t:=x;x:=y;y:=tが考えられます。実際にこのプログラムが仕様を満たしていることを示すということは、\{x=X\wedge y=Y\}t:=x;x:=y;y:=t\{x=Y\wedge y=X\}が真であることを示すということです。
そしてその為には、x=X\wedge y=Y\Rightarrow\omega_{t:=x;x:=y;y:=t}(x=Y\wedge y=X)を示せば十分です。
次回詳しく書きますが、代入文x:=Eに対して\omega_{x:=E}P=P^x_E(ここでP^x_Eは式Pに表われるxを全て(E)で置き換えた式)なので、
\omega_{t:=x;x:=y;y:=t}(x=Y\wedge y=X) \\ \Leftrightarrow\omega_{t:=x;x:=y}(\omega_{y:=t}(x=Y\wedge y=X)) \\ \Leftrightarrow\omega_{t:=x;x:=y}(x=Y\wedge t=X)
\Leftrightarrow\omega_{t:=x}(\omega_{x:=y}(x=Y\wedge t=X)) \\ \Leftrightarrow\omega_{t:=x}(y=Y\wedge t=X) \\ \Leftrightarrow y=Y\wedge x=X
より、x=X\wedge y=Y\Rightarrow\omega_{t:=x;x:=y;y:=t}(x=Y\wedge y=X)が成り立つことが分かります。
しかしながら、このような計算はプログラムが大きくなるとすぐに分かり難くなるので、次のような記法を導入します。
\{x=X\wedge y=Y\}\\t:=x;\\\{y=Y\wedge t=X\}\\x:=y;\\\{x=Y\wedge t=X\}\\y=t\\\{x=Y\wedge y=X\}
すなわち、複合文を構成するそれぞれの文の前後に、その事前条件と事後条件を書き入れます。このようにプログラムの途中に書かれた述語を表明(assertion)と言います。
\{P\}S\{Q\}\{Q\}T\{R\}、すなわちP\Rightarrow\omega_SQQ\Rightarrow\omega_TRが証明できれば、\omega_Sの単調性と\Rightarrowの推移律からP\Rightarrow\omega_{S;T}R、すなわち\{P\}S;T\{R\}が言えますので、先ほどのプログラムに現れた全ての事前条件、文、事後条件の三つ組みを証明すれば、プログラムが仕様を満たしていることを確かめたことになります。
また、このプログラムの途中の表明を補うことは容易なので、先ほどのプログラムを、
\{x=X\wedge y=Y\}\\t:=x;\\x:=y;\\y:=t\\\{x=Y\wedge y=X\}
と略記しても良いことにします。
このプログラムを素直にDelphiで記述すると、

{ (X = OldX) and (Y = OldY) }
T := X;
X := Y;
Y := T
{ (X = OldY) and (Y = OldX) }

となるでしょう。
表明をとりあえずコメントで書きましたが、Delphiには表明を記述する為の手続きSystem.Assertが用意されているので、これは、

OldX := X; OldY := Y;
T := X;
X := Y;
Y := T;
Assert((X = OldY) and (Y = OldX))

と書き直すことが出来ます(事前条件は自明なので省略しました)。
プログラムの正しさを最も確信できる方法はそれを証明することですが、それが難しい場合や、細部に立ち入りたくない場合等、証明を省きたい場合は多くあります。それでも表明をAssertで記述しておけば、少なくとも実行時に表明が満たされているかのチェックは働くので、バグの発見に大きく役立ちます。同時に、Assertで記述された表明は、プログラマの意図を明確に表した、しかも(単なるコメントとは違い)機械的にチェックされるドキュメントとしても優れています。
Assertに与えられた論理式がFalseの場合、DelphiはSystem.AssertErrorProc変数が指している手続きを呼び出します。SysUtilsはこの変数をSystem.SysUtils.EAssertionFailed例外を呼び出す手続きに設定しています(AssertErrorProc変数がNilの場合、Delphiは実行時エラー21(EAssertionFailed例外)を生成します)。
とは言え、Assert手続きが原因で例外が発生した場合、それはプログラムに論理的な誤りが存在するということなので、それをcatchしたところでプログラマに出来ることはほとんどないでしょう。プログラムに出来ることはせいぜい、ログを出力した後すみやかに死ぬことくらいです。
さて、Assert手続きは、$ASSERTIONSあるいは$Cコンパイラ指令によってプログラムから完全に取り除くことが出来ます。
上記のプログラムの変数OldXとOldYは表明の為だけに導入されました。従ってAssertがオフの場合これらの変数は最初の代入を除いて使用されることが無いので、最適化によって除去されることが期待できます。しかしそのこととは別に、Delphiのコンパイラは未使用の変数があることを警告してきます。この警告を抑制する方法は無いでしょうか。
まず考えられるのが、$IFOPTコンパイラ指令を用いる方法です。このコンパイラ指令によって、スイッチコンパイラ指令の状態を検査できますので、変数OldXとOldYがC-のときだけ現れないよう上記のプログラムを次のように書き換えることが出来ます。

{$IFOPT C+}
OldX := X; OldY := Y;
{$ENDIF}
T := X;
X := Y;
Y := T
{$IFOPT C+}
;Assert((X = OldY) and (Y = OldX))
{$ENDIF}

一応これでも目的は達成できますが、コンパイラ指令の散見するコードは読み難いので、代替案としてインライン展開と最適化に頼った次の方法が考えられます。すなわち、

procedure Unused(const X); inline;
begin
end;

のような空の手続きを用意しておいて、

OldX := X; OldY := Y;
Unused(OldX); Unused(OldY);
T := X;
X := Y;
Y := T;
Assert((X = OldY) and (Y = OldX))

とでもしておくのです。

次回予告

次回は配列やレコードの扱い、代入文、条件分岐などについて書く予定です。
また、証明が行えるプログラムを記述するには(形式的にせよ非形式的にせよ)証明の道筋を立てることとプログラミングを並行して進めなければなりません(証明方法を考慮せずに書かれたプログラムに証明を与えることは現実的ではありません)。そのことに関連して、事後条件を道標としたプログラムの記述方法にも少しずつ触れていきたいと思います。