プログラムに証明が付く日

この記事は「Theorem Prover Advent Calendar 2013」6日目の記事です。

http://qiita.com/advent-calendar/2013/theorem_prover

神田「野らぼー」にて、地下の薄暗い店内で…

「そう言えばこないだ隣で起こってたポインタオーバーラン、対応大変そうだったですけどちゃんと家に帰れてたんでしょうかね、新婚なのに…」

「ヌルポとかポインタオーバーランとか、どうして無くならないんだろうね。その時はみんな手を抜いてるつもりなんて毛頭なくて、一生懸命考えて大丈夫だと思ってるはずなんだけどね。レビューもして、それでも起こった後でみんなでソース見てみると、なんで気づかなかったんだよ!ってことになる。」

「人間って、そういうの苦手なんでしょうねきっと。ほら、『何かほかにありませんか』って聞かれても出てこないじゃないですか。静的な解析って、過去の経験を軸に見ていくことはできますけど、人を集めたところで結局集まった人の中では大丈夫だと思った、っていうレベルにしかならないんですよね。もちろんやらないよりずっといいんでしょうけど。」

「テストを書いて、テストを流して、静的解析を通して、レビューもして、でも絶対大丈夫って気になることってあまりないよね。なんかモヤッとしたものが残ることがあって。そうそう、僕はTさんのこういう直観を割と信用してて、あの人がテスト結果を見て何か不審な顔を見せた時は必ず何かそこに撃ち漏らしがあると思うことにしてる。」

「そういう人って頼りになりますよね。でもできればそういう人に頼らずに枕を高くして寝たいじゃないですか。」

「何かいい方法ないもんかねぇ・・・」

鶏のモモ肉をパリパリに焼いた『丸亀焼き』をスチールの皿の上で転がしながら先輩が考え込む。

ソフトウェアの形

「結局のところ、ソフトウェアの正しさを、納品前にどう示せるか、ってことですよね。図形でいうと、目指す形があって、その形になっていることをちゃんと確認する方法があるか、ということじゃないですか。」

「まぁ、そうかな」

後輩らしき方が、ちょっと考えた後でナプキンを出してペンで図を書き始めた。

「たとえば、まぁ目指すソフトウェアがこういう形だったとするじゃないですか。」

fig01

「丸だな」

「話をややこしくしたくないんで。このプログラムは、二つの入力をとってboolを返す関数だとしましょう。横軸は入力1で、縦軸が入力2です。白はtrue、黒はfalseを返す出力を表しています。こういう要件のプログラムだと思ってください。」

「ほう。」

「で、プログラムのテストを書くじゃないですか。これでできることって、この中の特定のケースに限って、特定の値が返ることを試してみることですよね。つまり、こんな特定の点ごとに、true、falseであることを確認するわけです」

fig02

「まぁ、そうだよな。」

「でも、考えてください。座標は無数にあって、とてもすべての点を試すことなんてできませんよね。これが2軸の整数ならまだ何とか総当たりもできなくないかもしれませんが、軸がもう一つ付くとアウトでしょうきっと。テストというのは、プログラムの形を確認する上でとても大切なものですが、結局のところ「点」でしか形を確認することができないんですよ。この点をどれだけ増やそうが、それをすり抜けている部分が無いことを示すことはできないんです。」

「まぁ、テストする方だってただ漫然とテストの点を選んでるわけじゃなくて、いろんなテスト技法を使って一つ一つの『点』の意義を上げていく努力はしているんだけどな。」

「そうなんですが、テストケースをすり抜けてしまう事象が後で見つかるという悲劇はこれを見ると避けられない気がしてきませんか?」

「静的な解析や、レビューなんかはどうなんだろう」

「これはあくまでイメージなのですが、静的解析やレビュー、それに最近の言語に取り入れられている『静的型』の効果というのは、こんな感じです。」

と言いながら彼はナプキンに線を引き始めた。

fig03

「こういったソースの論理を機械的に解析する作業は、こんな風に設計を『線』で追い込んでる感じなんですよ。単発のテストケースみたいにキワキワを目がけて攻めていけるわけじゃないけど、一定の条件の入力においては、要件を満たすことが連続的に示されるということです。うまくすれば、面で塗りつぶすこともできるかもしれません。」

「これだけ見てると、テストの方がよりプログラムの形に迫りやすいように見えるけど、どうなんだろう」

「これが難しいところで、テストだけでは対応できないものもあるかもしれないんですよ。こんなケースとかだと、テストはすり抜けてしまって、静的な解析でないと捕まえられないケースもあるかもしれません。」

fig04

「あくまで概念的なものですが。ただ、単体テストも進化してきて、テストケースをある程度境界線を意識しながら自動的に無数に作成してテストしてくれるツールもあって、そういうものを使うとテストをすり抜けることもグッと少なくなると思います。ただし、こういうものにはある程度限界があると思うんですよ。」

テストの行き着く先

「限界というと?」

「例えば、上のプログラムなら、境界線付近のどの入力がtrueでどの入力がfalseか、人間があらかじめ計算して確かめておく必要がありますよね。」

「そうしないとテストをしても正しいかどうか分からないね」

「そうやってテストケースを追加していく訳ですが、テストケースが増えれば増えるほど、テストケースを作る人間の側がミスをする可能性も増えていくわけですよ。」

「まぁ、実際にテストケースを流してから、エラーになったものだけ、プログラムとテストケースの両方を確認して、間違っているのがどっちなのか確認してるね。」

「そうなんですよ。人間が人手でテストケースの入力に対応する『正しい』出力を予想しようとすると、必ず一定の割合でミスは起こるんです。もっと悪いのは、テストケースを自動的に生成してくれるのはいいんですが、結果の確認は後で人間にさせる、というツールです。」

「そういうのあったあった。ソースを解析して網羅率の高いテストケースを自動生成して流してくれるんだけど、結果は出力を見て一つ一つ人間が確認するようになってるやつ。」

「人間って、そういうの無理なんですよ。入力を見せられて『この出力結果を予想して』って言われるとちゃんとできる人でも、結果を見せられて『これは正しいですか?』って確認を求められると、あまり考えずに『うん』って言ってしまいがちなんです。一つや二つならともかく、自動生成ツールはテストケースを作るのが仕事ですから、何百というテストケースを作って流し、表の形で見せて一つ一つ確認してチェックボックスをONにしろっていうわけです。相当な精神力がないと正しい判断はできなくなりますよ。」

「となると、テストケースと結果予想は先に作っておかないとダメということだよね。」

「そうなんですが、そうやってテストケースとその実行結果予想を沢山作っているうちに、ふと一つの考えが頭に浮かんでくるわけですよ。『これ、入力を決めたら、実行予想結果を計算するマクロをExcelで書けばいんじゃね?』って。」

「まぁプログラマならそう思うのも無理はないだろうな。」

「そして、嬉々としてExcelのVBA画面を起動し、マクロを書き出してふと思うわけですよ。『入力から出力を計算するプログラムって、テスト対象のプログラムそのものじゃん』って。同じプログラム二度書いてどうすんだよと。」

「確かにそうだね。」

「でもですよ、この話は決してバカな話でもないんですよ。最初に手作業でやっていたテストケース作成作業だって同じことなんです。このテストケースの数を増やしていくという行為は、同じプログラムを二度書くのと、意味合いでは等価な行為に収束するんですよ。」

「...」

「何が言いたいかというと、同じプログラムを二つ書いて、両者に同じ入力をしたら同じ出力が出るということを無数に確認するということは、テストケースを無数に書くというのと究極的には同じことで、これは決して無意味なことではないんです。」

「...そうかもしれない」

「ただ、同じ人が同じ詳細設計書を見て同じ言語で書くと本当に同じプログラムが出来てしまうので、機能設計レベルから二つのチームに分かれて、なるべくパラダイムの違う別のプログラミング言語で同じプログラムを作るのが一番いいということなんです。で、完成した二つのプログラムの結果をつき合わせて、違いがあればどちらが間違っているか確認して、時間の許す限り気の済むまでテストをして、気が済んだらどちらか実行が速いとか使用メモリが少ないとか、都合のいい方のプログラムを採用すれば済むことなんです。さらに言えば、両者に仕様の誤解があったなら、それは仕様書にあいまいさが残っていることも示唆してくれるんです。」

「こ・・コストは倍になるけどな」

「実際にはテストの自動化が出来ることを考えると1.5倍ぐらいで済むんじゃないかと思うんですよ。実はもう一つあって、両者のプログラムの作り方はできれば逆向きであることが理想なんです。」

「逆向き?」

「例えば、一方は『trueとなる条件を一つ一つ組み立てていくように』してもう一方は『falseとなる条件を積み重ねていくように』作るといった具合です。この図で言うと、trueチームは白い部分の外側から内側に包み込んでいくように、falseチームは黒い円の内側から外側に成長するようにプログラムを定義するということです。」

fig05

「そして境界線あたりでせめぎ合うということか」

「そうです。両者正しく出来れていれば境界線で交わることはないはずですし、どちらにも属さない領域もできないはずです。これをモンテカルロ的に確認できれば、プログラムは高い確率で矛盾なくできていると思えるんじゃないかと。」

「しかしそれは両チームストレスだろうな~きっと。」

「もちろんこれは理想的には、という話なのですが。」

二つのプログラムが同じであることの証明

山盛りだった煮干しバラシ天がすっかりなくってしまった。

「理想的には、という流れのついでに、もう一つお話ししましょうか」

「何だまだあるのか。何か頼んでからにしようぜ」

揚げうどんと新しい酒が来るのを待ってから話を続けた。

「さっきの『二つプログラムを作る』という案なんですが、実はまだ弱点があるんですよ。分かりますか?」

「コストとかモチベーションとかかなぁ・・・どっちかテストケースにされると分かってると元気でないかもしれない」

「それもあるかもしれませんが、そういうことじゃなくて、この二つのプログラムのつき合わせも結局のところ『時間の限り』でしかないところなんですよ。有限の時間で、無限に近い入力のある実際のプログラムの入力を全パターン試すことなど結局できないんです。もちろんテストケースを手書きするよりもずっと良好な結果が得られるとは思いますが。」

「そんなのしょうがないんじゃないか。そんなもんだろ」

「それが、そうでもないような仕組みも無くはないんですよ。ただしかなり険しい道のりですが」

「ほう。まだ終電まで時間があるし聞かせてもらおうじゃねぇか」

「これがまた難しい話でですね...」

また新しいナプキンを抜いて書き始める。

「例えば、先ほど話した二つのチームが

f (x, y) = x * y;

という関数と

g (x ,y) = y * x;

という二つの関数を作ったとします。さっきまでの流れだと、この二つの関数が同じ入力で同じ値を返す関数であることを確認するためには、xとyに想像がつく限りの組み合わせを総当りで入れて、戻り値が同じであることを確認する作業を時間の限りやるということですよね。」

「まぁ、例え話だとそうだけど、この二つの関数が同じ結果を返すのは見ればわかるよな」

「まぁそうなんですが、それは今は気づかないことにしてこの二つの関数を議論しましょう。たったこれだけの関数でも、32bitなら40億の2乗回の計算をしないと二つの関数が同じ機能を持っていることを保証することはできないということです。これは大変です。」

「気づかなければ、そうだな」

「しかしです、この二つの関数が、任意の入力で必ず同じ値を返すという証明を数学的に書くことができれば、わざわざ40億の2乗回も計算する必要はないわけです。」

「この式なら、証明など書かなくてもいいだろう。」

「僕らは掛け算の計算順は入れ替えても答えが変わらないと学校で習っているからそういうことが言えるわけで、コンピュータはそんなこと知らないんですよ。でも、定理証明機能を持っている言語だと、コンピュータに対して『この二つの関数はどんな入力をしても必ず同じ結果が返ることを示してやるから見てろ』と宣言して、その後にその証明を書いて納得させることが出来るんですよ。」

「証明してくれるんじゃなくて、書くのか!」

「基本的には、書きます。ある程度の範囲なら勝手に証明を導いてくれますが、期待するほどの範囲ではないと思ってください。」

「その証明を、わざわざコンピュータで書く理由はあるのか?」

「コンピュータを使ったほうが楽だから、コンピュータで証明を書くんです。この関数fとgが同じだということを示すのにも数十行のコードが必要になりますが。それに、人間が書いた説明を人間が読んで『確かに同じだね』と納得したところでどこに穴があるかわかりませんし、人間が証明を検証するのは、さっき出た『自動テストの結果を人間が検証する』のと同じ愚を冒すことになります。」

「そんな掛け算ぐらいで何十行も書かないといけないなら、実際の仕事で使えるのかな」

「その辺は考えようで、本気で40億の2乗回テストをするなら、証明を書いたほうが早い場合も多いでしょう。実際のプログラムではもっと入力のパターンは多くなるでしょうから、証明の方が有利になることももっと増えるかもしれません。ただ、我々はこれまで全パターンテストしないで『たぶん大丈夫』と言ってしまっているので、証明を書くことが不経済だと感じるだけなんですよ。」

「プログラムの正しさにそういうコストをかけて構わない業界もあるのかもな・・・」

「ただ、実際に証明を書くのにはかなり勉強が必要なのも事実です。記号論理学とか、数理論理学とかの知識が絶対的に必要になります。その辺はしょうがないといえばしょうがないのですが、ハードルが高いと言われれば否定はできないですね。ただ証明つきのプログラムにはもう一つ機能があるんです。」

「まだあるのか!もう終電近いぞ」

関数について「考え切る」ということ

「この手の言語は、これまでの言語よりもずっと『型』の奥行きが深いんです」

「というと?」

「例えば、『10より小さい整数』というような型が定義できるんですよ。」

「それのどこが嬉しいの?」

「例えばこんな関数の定義を考えてみましょう。」

f ( x : x は20未満の自然数 ) : 戻り値は10未満の自然数 = x / 2

「何これ?」

「f は、20より小さい自然数を取って10より小さい自然数を返す関数で、中身はxを2で割ることだぞと。そんな意味です。xは引数で、コロンの後はその型だと思って読んでください。実際のプログラミングではもう少し別の書き方をしますが。」

「やっぱり嬉しさがわからない」

「この関数が宣言しているものは、『xは20より小さい自然数であることを前提として』、xを2で割るという計算をして、『戻り値が10より小さい自然数であることを保証しましょう』ということなんです。」

「・・・?」

「で、この関数をコンパイルするためには、『xは20より小さい自然数であることを前提とする』と、x / 2 が『10より小さい自然数』に収まることの証明を人間がエッチラオッチラ書かないといけないんですね。それが書けないとコンパイルしてくれない。」

「恐ろしいな」

「恐ろしいんですが、嬉しいこともあるんです。この関数が入力に『20より小さい自然数』を要求しているということは、この関数を呼び出す側も、引数の値がこれを満たすことを証明できてないといけないんです。つまり、呼び出せた、というか呼び出すようなコードがコンパイルできたということは、呼び出す側が持つ前提の元で、引数に渡す数が、呼び出す関数の前提を満たしているということが保証されるんですよ。」

「関数というのは、引数として与えられた前提を元に戻り値の前提を満たすことが証明できるものであって、中で他の関数を呼び出す時も、それに渡す引数が呼び出される関数の前提を満たしていることを証明しないといけないんだな。ってまじかよ」

「で、最初の話に戻るんですが、これだけ厳格に型が定義できてそれがちゃんと運用できれば、配列のインデックスがオーバーランしてしまうこともなくなるんです。なにせオーバーランするような値が引数で入ってくることが不可能になりますから。そういう値が入力されないことが、実行時ではなくコンパイル時に保証されるんです。」

「わからなくもないけど、証明が書けないということはないの?」

「書けない時は、前提か、戻り値の型か、計算のどれかもしくは複数が間違っているか、勉強不足か・・・いずれにしても証明が書けるまでの間に、その関数の隅から隅まで考え尽くす必要がありますから、『何となくできたつもり』のものがリリースされてしまうという事態だけは避けられます。」

「それだと何もリリースされなくなるかも・・・ゴールは遠いな。」

「遠い道のりですね・・・・・でもいつか新婚さんが会社に泊まらなくてもいいような日が来ることを夢見るのも悪くないんじゃないでしょうか」

「それに、最初の問題として人間が『作りたいプログラムの形』を、作る前にちゃんと定義できるのか、という疑問もあるよな。」

「そうなんです。正しくて厳格な仕様書というのは、いうなれば自然言語で書かれたプログラムそのものと言ってもいいわけで、それがプログラムより先に書けるならプログラマはこんな苦労しないよ、という気もしますね。」

「でも、それを言っちゃオシマイだよな・・・」

「昔お世話になったというか、今でもエンジニアとしての心の師匠みたいな人と仕事をさせてもらっていた時があったんですが、その人の口癖が、『この設計書じゃ、まだ考え切れてないね・・・』だったんです。僕は結局その人に一度も褒められることがないまま職場が変わっちゃったんですが、証明を考えてると『考え切る』という言葉の意味が少し分かったような気がしてくるんです。証明を書く、ということを通しての『プログラムの隅々まで漏れなく考えることが強制される経験』に大きな意味があると思うんですよ。」

「・・・酒・・・なくなったな。」

「電車もなくなりましたね。」

こうして神田の夜は更けていく・・・・

 

(終)

 

※ 証明付きのプログラミングに興味を持たれて、『ちょっと試してみたい』、という気になられた方は、ぜひ一度『ソフトウェアの基礎』や『プログラミング Coq』を最初のあたりだけでも読んで、できればCoqをインストールして実際に手を動かして試してみてください。

『ソフトウェアの基礎』

http://proofcafe.org/sf/

『プログラミング Coq 〜 絶対にバグのないプログラムの書き方 〜』

http://www.iij-ii.co.jp/lab/techdoc/coqt/

※ 型が値で修飾される『依存型』というものがどんな感じか見たい方は以下のリンクをClick!

にわとり小屋でのプログラミング

http://yosh.hateblo.jp/entry/2013/12/06/202827

※神田「野らぼー」

http://www.norabow.jp/nightmenu/index.html