02.verification+validation

変幻する実行可能知識 2

「ただしひとゐふこと」

このコラムではソフトウェアを実行可能な知識を表すものとして見る視点から, ソフトウェアを作るということを問い直そうと考えている. 「実行可能な知識」とはさまざまな知識を表しているソフトウェアがCPUの上でまさに実行可能であるということだ. これは従来の紙のうえに書かれているだけの知識にはなかった特徴だろう. ただし「知識」の範囲を少しだけ広げて考えれば, 例えばビジネス・プロセスも実行可能な知識 (ビジネス組織が実行する) だし, 遺伝情報も実行可能な知識 (生命体が実行する) と思ってもよさそうだ. ソフトウェアは実はこういうものたちとつながっている.

知識にはいろいろな性質がある. モジュール性, 伝達可能性, 柔軟性, 抽象性, 具体化可能性などなど. 単に知識があればといいということでは全くない. 「知識の質」, 特に「知識のダイナミクス」を支える質が重要なのだ. 今回はその一つ, 知識の検証可能性ということを考えてみることにしよう.

知識の「正しさ」を知る方法には実は2種類ある (「正しさ」に2種類あると言ってもいい). 一つは検証 (verification) と呼ばれるもの, もう一つは妥当性確認 (validation) と呼ばれるものだ. この使い分けは微妙で難しいが (分野によっても違うかもしれない), おおざっぱに言うと検証とは自分たちがこういうものを作ろうと決めたとおりにできているかどうかを確かめること, 妥当性確認とはできたものが本当に欲しかったものかどうかを確かめることだ.

例えばテスト仕様書を書き, テスト仕様にしたがってソフトウェアを実行したときにどのような答えが出るかをチェックする. これが検証. 検証できたからと言って, そのソフトウェアが「本当に」正しいとは限らない. だって仕様書にすべての場合を列挙することはできないし, そもそも仕様書が顧客の意図したものになっているとは限らない. それに対してユーザや顧客が欲しかったソフトウェアになっているかどうかをチェックするのが妥当性確認.

極端な話, 100万行のシステムの仕様上, コード1000行当たり欠陥密度が0.001だったとしよう. 検証を行ってその仕様を満たしていることは分かったとする (注1). ところがその一つの欠陥がユーザのニーズにとって決定的な欠陥だったとしたら, そのシステムは妥当とは言えないだろう. ある仕様に対してシステムが検証されているということは, システムが妥当であることの必要条件とはなっても十分条件にはならないのである.

注1: ここで何か変と思った人はおそらく正しい. 100万行のシステムのコード1000行当たりの欠陥密度が0.001ということは (おそろしく信頼性の高いシステムだが) システム全体で一つの欠陥しかないということだ. ん? 欠陥が一つしかないということはなぜ分かるのだろう? 欠陥が一つあるということが分かっていたら直せばいいではないか!

工業製品の信頼性は例えば100万個に一個の割合で不良品が発生するというもので, これは考え方として分かりやすい. 製品一個一個はほとんど独立したものと考えていいのだから. ところがソフトウェアの一行一行は独立しているどころか, 同じ一つのものの一部なのだ. 100万行に一つしか欠陥がないということにはほとんど意味がない. そのことによって残りの99万9999行も使い物にならないかもしれないのだから.

製品の妥当性は顧客の満足度につながっている. だからこそ重要なのだが, 妥当性を確認するためにはどうすればいいだろう? いろいろな考え方があるが, 僕は多くの種類のソフトウェアでは最終的には「実際に動かしてチェックする」しかないだろうと考えている. だって動かないソフトウェアをみても何も分からないから. できるだけ早い段階で「実際に動かしてチェックする」ために僕たちは繰り返し的な開発を行う. そして同時に常に検証を繰り返す. 検証によって妥当性が保証されるわけではないけれど, 有効な検証ならばいかにも妥当性に一歩一歩近づいている感じがするではないか!

ではもう一方の検証はどうすればいいだろうか? 僕たちは「知識」に基づいてソフトウェア開発を考えようとしているのだから, 検証も知識の変換過程として考えよう. すると検証とは「今こう動く (as-is)」という知識と「かくあるべし (should-be)」という知識をすりあわせる過程 (注2) だと考えることができる. そのためには「今こう動く」ということと「かくあるべし」ということが (実行可能) 知識としてうまく表されていて欲しいわけだ.

注2: この「すりあわせる」というところが肝心. 僕たちの立場では「かくあるべし」が最初から絶対に正しいとは思わないのだ.

JUnitをはじめとするxUnitと呼ばれる単体テスト・フレームワークもその方法の一つだ. 今やデファクト・スタンダードとなり, 一緒の納品を求められることも多いだろう. 「今どう動くか」は実際にボタンを押せば, 結果が赤や緑で表示される. とても「感情的な」知識表現になっている. 「どう動くべきか」という知識はテスト・コードが表す. 面白いのはどう動くべきかという知識も検証対象となっている知識と同じプログラミング言語で同じように記述されていることだ. xUnitを使ったプログラムの書き方 (テスト駆動開発) から言っても, テストされるコードとテストするコードが依存し合い, 渾然一体となっている. 非常にソフトウェアらしい側面で面白いんだけれど, 「何を検証しているか」はやっぱり分かりやすいとは言いにくい (回りくどい).

「どう動くべきか」を表すもう一つの方法は「契約」という考え方だ. 契約はサービスを提供する側とサービスを受ける側の間で結ぶ. 例えばホテルに泊まるときには, 宿泊客の義務 (= ホテルの権利): 1週間前までに予約して, 宿泊時にクレジット・カードを提示する ホテルの義務 (= 宿泊客の権利): 一つの決められたグレードの快適な部屋を提供する 宿泊客が義務を果たしていれば, ホテルも義務を果たしてくれるというのが契約だ.

ソフトウェアの検証という立場からはサービスとはメソッドや関数の呼び出しということになる. 例えば平方根を計算するサービスを提供するメソッド

double sqrt(double x)

に関する契約は

  • サービスを受ける側の義務: 0か正数の引数xを渡す
  • サービスを提供する側の義務 : 結果を自乗すると引数に等しい

となる (もっとも現実のdoubleには誤差が含まれるから, まったく等しくなるとは限らない). サービスを受ける側の義務を事前条件 (pre-condition), サービスを提供する側の義務を事後条件 (post-condition) という. 契約とは事前条件が満たされたら事後条件が満たされることを保証するということだ.

これをJML (Java Modeling Language)という契約記述言語ではJava言語のJavaDoc風に次のように書く.

//@ requires x >= 0.0;
//@ ensures JMLDouble.approximatelyEqualTo(x, \result * \result, eps);
public static double sqrt(double sqrt) { ... }

epsは誤差の範囲を表す定数, JMLDoubleはJMLが提供するライブラリ, \resultは結果を表す変数だ. この契約をみれば, 引数が正かどうかチェックするのは呼び出す側の仕事ということが一目で分かる. また呼び出した側は結果が自乗すると引数と (一定誤差範囲で) 同じということを信頼してその先の仕事を進めることができる.

JMLのオープンな処理系ではこのJavaDocを解析して, メソッドの呼び出し前後に事前条件, 事後条件をチェックするコードを吐き出してくれる. 契約が満たされていなければ例外が発生する. もっとも製品コード中にこんなコードを埋め込んでおくのはもったいないから, 十分テストが終わったら普通にjavacでコンパイルすればよい.

「契約」という考え方をサポートしてくれる処理系は他にもいくつかある. xUnitに較べていい点は「かくあるべし」という知識が明確に表現されている点だ. xUnitでは結局テスト・コードを読まなければ, 何がテストされているのかよく分からない. すべてのメソッドに契約を書いてから (注3) メソッド本体を書くというプラクティスを身につければ, それは「契約駆動開発」と言っていいだろう. 「契約」という知識を, それを満たしつつ動作するソフトウェアという知識に変換する (ミクロな) 過程なのである. もしちゃんとできれば間違いなく, ソフトウェアの質は向上する.

注3: 単なるsetter/getterは多分契約を書かなくてもいいだろう. 誤差や時間を含むような場合には簡単にいかないこともある. また意図したこと以外には何も変わっていないことを確認するのは実際には難しい.

2004.02.21
山田正樹 (メタボリックス)

Comments