C++言語解説:3-3.検証/assert
2003-02-16
[C++ Index Top] [Prev] [Next]

[概要]　プログラムが正しいことはどうすれば検証できるのでしょうか。ここでは検証論
　　　　の土台となるホーア論理の基礎とassertの使い方について考えていきます。

[構成]・ホーア論理の基礎
　　　　　* プログラムの検証に関する素朴な疑問
　　　　　* 表明付きプログラム
　　　　　* 複合文の正しさ
　　　　　* while文の正しさ
　　　　　* 表明の記述
　　　・assertの適用
　　　　　* 不変条件
　　　　　* assert()関数
　　　　　* 例外の利用

●ホーア論理の基礎 (*1)

　◆プログラムの検証に関する素朴な疑問

　　・プログラムの正しさを検証する。ソフトウェア/システムの開発に携わった経験のあ
　　　る方であれば「耳の痛い」言葉だと思います。
　　
　　・C/C++で検証に関して調べると、必ず出てくる言葉が assert() です。assert()関数
　　　を簡単に説明すると
　　　　　+ 指定論理式がtrueでなければプログラムを停止
　　　　　+ 停止の際、ソースファイルと行番号を出力する
 　　　というものです。
　　
　　・しかし、assert()に関する最も多く、かつ素朴な疑問として
　　　　　「どう書けば良いかわからない」
　　　というものがあります。「前提条件を書けば良い」とよく言われますが、「前提条
　　　件を書く」ことと「プログラムの正しさを証明する」ことが頭の中で結びつかない
　　　のです。(この前提条件という説明にも誤解が含まれているようです。)
　　　
　　・このassert()関数について原著を読んでみると、以下の言葉を見つけることができ
　　　ます。
　　　　┌──────────────────────────────────┐
　　　　│ 不変条件の概念は、Floyd, Naur, Hoareの前条件、後条件の仕事に起源を │
　　　　│ 持つもので、過去30年ほどの抽象データ型、プログラムチェックのほぼす │
　　　　│ べての仕事に生きている。　　　　　　　　　　　　　　　　　　　　　 │
　　　　└──────────────────────────────────┘
　　　つまり、assert()で記述する論理式は「不変条件」であり、それはHoareの前条件と
　　　後条件に関連すると言っています。
　　
　　・従って、assert()を有効に使うためには「不変条件...前条件/後条件」とは何かを
　　　理解することが必要です。これがホーア(Hoare)論理の基礎を学ぶ動機です。


　◆表明付きプログラム
　
　　・プログラムの正しさは仕様に対して相対的に決まります。例えばList1のような最大
　　　公約数を求める関数があったとします。

　　　[List1.最大公約数を求める関数:gcd]
　　　┌───────────────────────────────────┐
　　　　#include <iostream>
　　　　using namespace std;
　　　　
　　　　int main() {
　　　　　　int gcd(int a, int b); //引数はa,bとする
　　　　　　
　　　　　　cout << "最大公約数(greatest common divisor)" << endl;
　　　　　　cout << " gcd(a,b):( 12, 32) = " << gcd(12,32)　<< endl;
　　　　　　cout << " gcd(a,b):(128, 48) = " << gcd(128,48) << endl;
　　　　　　cout << " gcd(a,b):(　0, 12) = " << gcd(0,12)　 << endl;
　　　　　　
　　　　　　return 0;
　　　　}
　　　　
　　　　//最大公約数関数
　　　　int gcd(int a, int b) {
　　　　　　int temp;
　　　　　　int x = a; //┐説明の都合で付けた
　　　　　　int y = b; //┘冗長ステートメント
　　　　　　
　　　　　　while(y) {
　　　　　　　　x = x % y;
　　　　　　　　temp = x;
　　　　　　　　x = y;
　　　　　　　　y = temp;
　　　　　　}
　　　　　　
　　　　　　if (x < 0) x = -x;
　　　　　　
　　　　　　return x;
　　　　}
 　　　└───────────────────────────────────┘
　　　┌───────────────────────────────────┐
　　　 [出力結果]
　　　　 最大公約数(greatest common divisor)
　　　　　 gcd(a,b):( 12, 32) = 4
　　　　　 gcd(a,b):(128, 48) = 16
　　　　　 gcd(a,b):(　0, 12) = 12
　　　└───────────────────────────────────┘
　　　
　　・List1のプログラムは「関数gcdが正しく引数の最大公約数を戻す」ことを前提に記
　　　述されています。アルゴリズムは「ユークリッドの互除法(剰余版)」と呼ばれてい
　　　るものです。
　　
　　・しかしList1の正しさは、関数gcd()の正しさに大きく依存しているとも言えます。
　　　「プログラムが正しい」とは「仕様を満たす」ということです。ホーア論理では、
　　　このことを表明付きプログラム(asserted program)で以下のように記述します。
　　　　　{A}P{B} 又は <A>P<B> (*2)

　　・{A}P{B} の意味は
　　　　┌────────────────┐
　　　　│プログラムPを　　　　　　　　　 │
　　　　│条件Aが成り立つ状態で実行すれば │
　　　　│停止後に条件Bが成立する　　　　 │
　　　　└────────────────┘
 　　　というものです。例として、関数gcd()の中身に対して表明を適用します。

　　　[List2.表明付きプログラムの例(1)]
　　　┌───────────────────────────────────┐
　　　　 { a,b の少なくとも一方が0ではない }
 　　　　　　　int temp;
　　　　　　　int x = a;
　　　　　　　int y = b;

　　　　　　　while(y) {
　　　　　　　　x = x % y;
　　　　　　　　temp = x;
　　　　　　　　x = y;
　　　　　　　　y = temp;
　　　　　　　}
　　　　　　
　　　　　　　if (x < 0) x = -x;
　　　　 { xは a,b の最大公約数 }
 　　　└───────────────────────────────────┘
　　
　　・List2では最初の表明が実行前の条件を、最後の表明が実行の条件を表しています。
　　 よって {A}P{B} において
　　　　 表明A : 前条件(precondition)
　　　　 表明B : 後条件(postcondition)
 　　 と呼びます。「仕様を満たす」ということを「実行前後の条件が成立する」に言い換
　　 えて考えるわけです。


　◆複合文の正しさ
　
　　・プログラムは小さな部分的プログラム(文)が集まってできたものです。よってプロ
　　　グラム全体の正しさは、部分的プログラムの正しさから考えることができます。
　　
　　・つまりプログラムPが「P1;P2;・・・Pn」で構成される場合
　　　　　{A}P1;P2;・・・Pn{B}
　　　　　　　　　↓
　　　　　<A>P1<S1>P2<S2>・・・<Si-1>Pi<Si>・・・<Sn-1>Pn<B>
　　　のように、それぞれのプログラムに対する表明を作り、プログラム全体の正しさを
　　　示すということです。これを複合文の規則(composition rule)と呼びます。
　　　　　┌───────────────────────────┐
　　　　　│複合文の規則　　　　　　　　　　　　　　　　　　　　　│
　　　　　│　{A}P1{S1}P2{S2}・・・{Si-1}Pi{Si}・・・{Sn-1}Pn{B}　│
　　　　　│　─────────────────────────　│
　　　　　│　　　　　　　 {A}P1;P2;・・・Pn{B}　　　　　　　　　 │
　　　　　└───────────────────────────┘
 　　
　　・関数gcd()は、while文/if文/代入文で構成されています。それぞれの「正しさ」を
　　　考えるわけですが、if文/代入文は定型的に扱えるので、ここではwhile文について
　　　説明したいと思います。
　
　
　◆while文の正しさ
　
　　・while文の規則は以下のように表現されます。
　　　　　┌──────────────────┐
　　　　　│whileの規則　　　　　　　　　　　　 │
　　　　　│　　　　{"tはtrue"∧A} P {A}　　　　│
　　　　　│　────────────────　│
　　　　　│　{A} while (t) P {"tはfalse"∧A}　 │
　　　　　└──────────────────┘
 　　
　　・条件tがtrueの間while文は実行され、while文の中身であるPの実行中及び実行前後
　　　で表明Aが成立するという意味です。この表明Aをループ不変表明(loop invarinat
　　　assertion)と呼びます。
　　
　　・while文の正しさを示すには、ループ不変表明の選び方がポイントになります。今回
　　　のプログラムでは、例として以下のループ不変表明が考えられます。
　　　　　gcd(x, y) = gcd(a, b)
 　　　x, yの値はwhileループ中の実行文で変化しますが、その実行状況に関わらず初期値
　　　a, bのgcdと一致するという表明です。
　　
　　・ループ不変表明を見つけるのは非常に難しいのですが、幸いなことに「必ず見つけ
　　　出せる」ことはわかっているそうです。
　
　
　◆表明の記述
　
　　・では関数gcd()に表明を付加してみます。

　　　[List3.表明付きプログラムの例(2)]
　　　┌───────────────────────────────────┐
　　　　 { aの値はa, bの値はb
　　　　　 a,b の少なくとも一方が0ではない }
 　　　　　　　int temp;
　　　　 { aの値はa, bの値はb
　　　　　 a,b の少なくとも一方が0ではない }
 　　　　　　　int x = a;
　　　　 { xの値はa, bの値はb
　　　　　 a,b の少なくとも一方が0ではない }
 　　　　　　　int y = b;
　　　　 { xの値はa, yの値はb
　　　　　 a,b の少なくとも一方が0ではない
 　　　　　　　while(y) {
　　　　　 {"y != 0"がtrue ∧ gcd(x,y) = gcd(a,b) }
 　　　　　　　　x = x % y; //┐
　　　　　　　　temp = x;　//│本当であれば
　　　　　　　　x = y;　　 //│ここでも代入文の表明が必要
　　　　　　　　y = temp;　//┘
　　　　　 { gcd(x,y) = gcd(a,b) }
 　　　　　　　}
　　　　 { |x|は a,b の最大公約数 }
 　　　　　　　if (x < 0) x = -x;
　　　　 { x は a,b の最大公約数 }
 　　　└───────────────────────────────────┘
　　　
　　・ステートメント単位では、前条件と後条件が付きます。しかし複合文の正しさから
　　　後条件と次行の前条件が一致するように表明を記述するので、実質的には前条件だ
　　　けを記述するように見えるわけです。そしてステートメントの内容から表明を記述
　　　するのに苦労するのは、while文のループ不変表明です。
　　　
　　・ようやくassertion(表明)の記述内容である「前提条件」という言葉の意味がつかめ
　　　てきたと思います。そしてループステートメントの表明に不変表明が絡むこともわ
　　　かったと思います。
　　　
　　・そこで、この後はassertの適用について考えていくことにします。
　　
　
●assertの適用
　◆不変条件
　
　　・原著では、前条件/後条件の考え方を一歩進めて「不変条件」を提唱しています。こ
　　　れはオブジェクトの定義時と解体時に成立するある明確な状態を決めることです。こ
　　　の状態を不変条件(invarinat)と呼んでいます。
　　
　　・Stroustrup氏は、その経験からassertに記述できる論理式の語彙が貧弱なことより
　　　多くの場合、十分に前条件と後条件を記述することができないと言っています。そ
　　　こで記述可能な不変条件を定義/適用すべきと考えているようです。(*3)
　　
　　・不変表明は実行前と実行後に成立する条件です。実行中は必ずしも成立しません。
　　　これはループ不変表明と異なる点です。


　◆assert()関数
　
　　・assert()(assertマクロ)はCの標準ライブラリ<assert.h>で提供されています。
　　　引数に記述した式の評価結果がfalseの場合、abort関数を呼び出してプログラムを
　　　終了します。
　　
　　　[List4.assert()使用例]
　　　┌───────────────────────────────────┐
　　　　#include <iostream>
　　　　#include <cassert>　//<assert.h>
　　　　using namespace std;
　　　　
　　　　void main(){
　　　　　　int i_a;
　　　　　　int i_b;
　　　　　　
　　　　　　cout << "オペランド1:";
　　　　　　cin >> i_a;
　　　　　　cout << "オペランド2:";
　　　　　　cin >> i_b;
　　　　　　
　　　　　　assert(b!=0);
 　　　　　　cout << "結果:" << a/b << endl;
　　　　}
　　　└───────────────────────────────────┘
　　　┌───────────────────────────────────┐
　　　 [出力結果]
　　　　 C:>test
　　　　 オペランド1:20
　　　　 オペランド2:10
　　　　 結果:2
　　　　
　　　　 C:>test
　　　　 オペランド1:20
　　　　 オペランド2:0
　　　　 Assertion failed: i_b!=0, file test.cpp, line 14

　　　　 abnormal program termination　　　　
　　　└───────────────────────────────────┘
　　
　　・assert()を使用するのはデバッグ時のみとしたい場合、NDEBUGマクロを#defineで
　　　定義します。NDEBUGマクロは<assert.h>をincludeする前に定義します。

　　　[List5.NDEBUGマクロ使用例]
　　　┌───────────────────────────────────┐
　　　　#include <iostream>
　　　　#define NDEBUG
 　　　　#include <cassert>
　　　　using namespace std;
　　　　
　　　　void main(){
　　　　　　int i_a;
　　　　　　int i_b;
　　　　　　
　　　　　　cout << "オペランド1:";
　　　　　　cin >> i_a;
　　　　　　cout << "オペランド2:";
　　　　　　cin >> i_b;
　　　　　　
　　　　　　assert(i_b!=0);
 　　　　　　cout << "結果:" << i_a/i_b << endl;
　　　　}
　　　└───────────────────────────────────┘


　◆例外の利用
　
　　・assert()を使用すると、abort()関数を呼び出してプログラムを強制終了しますが、
　　　大抵の場合「強制終了」の前に施したい後処理があります。
　　
　　・またassert()の機能をdisable化するときはNDEBUGマクロを使用しますが、これはコ
　　　ンパイル対象ソース単位以下のコントロールが効きません。
　　
　　・そこでC++では、例外によるassertの実装が提唱されています。以下のテンプレート
　　　が実装例になります。
　　　
　　　[List6.Assertテンプレート実装例]
　　　┌───────────────────────────────────┐
　　　　#include <iostream>
　　　　using namespace std;
　　　　
　　　　template <class A, class T>
　　　　inline void Assert(A assert_arg, T except)
　　　　{
　　　　　　if (!assert_arg) throw except;
　　　　}
 　　　　
　　　　void main() {
　　　　　　int i_a;
　　　　　　int i_b;
　　　　　　int i_except;
　　　　　　
　　　　　　cout << "オペランド1:";
　　　　　　cin >> i_a;
　　　　　　cout << "オペランド2:";
　　　　　　cin >> i_b;
　　　　
　　　　　　try {
　　　　　　　　Assert(i_b!=0, i_except=10);
　　　　　　　　cout << "結果:" << i_a/i_b << endl;
　　　　　　}
　　　　　　catch(int i_catch){
　　　　　　　　cout << "0で割り算を実行しました" << endl;
　　　　　　}
 　　　　}
　　　└───────────────────────────────────┘
　　
　　・例外を使用すれば、終了方法を実行状況に合わせた穏やかな形で定義することがで
　　　きます。そして、assert()のようにNDEBUGマクロで一括enable/disable制御ではな
　　　く、有効条件を含めて記述することで、任意の制御が可能となります。
　　
　　・assert()、Assertテンプレートを使用する別の利点は、プログラマの意図する条件
　　　が明確に記述されることです。動作の論理とは異なるものであることも容易に判断
　　　できるので、コードの可読性が上がり、レビュー/デバッグ等にも有効に生かされる
　　　でしょう。
　　
(*1)この章におけるHoare論理の説明内容は「プログラム検証論(林晋著,共立出版)」に沿
　　っています。詳しい内容が知りたい方は、この本を読んでみて下さい。

(*2)<A>P<B> では P が必ず停止する「完全停止性」の意を含みます。{A}P{B}ではPが停止
　　しなくてもよく、表明Bは停止時のみ成立します。

(*3)もちろん「プログラム検証論」でも、語彙と検証能力の関係ついて詳しい説明が為さ
　　れています。これを考慮するとStroustrup氏の主張は妥当であると思われます。
[Revision Table]
　|Revision　|Date　　　 |Comments
　|----------|-----------|-----------------------------------------------------
　|1.00　　　|2003-02-16 |初版
[end]
Copyright(C) 2003 Altmo
[C++ Index Top] [Prev] [Next]