― バーを目指して歩いている
私「秋も深まってきましてねぇ、今年も清水は盛況でした」
私「え、ご覧になってない？ それはもったいない。紅葉の季節になると、いつも夜行くんですよ。あそこの池を夜に見るのが大好きでねぇ」
私「必ず紅葉が散り始める前に行くんですよ。はい、お勧めなので是非」
私「そういえば、12月になりまして、技術系advent calendarが流行っていますねぇ」
私「私もいくつか見てますよ。プログラムに証明のなんたらっていう記事、あ、あなたもご覧になりましたか。かなり人気の記事のようですねぇ」
私「そうですそうです。非常に面白いですねぇ。この記事について、あなたとバーでお話しようかと思いまして」
私「あ、私の行きつけのバーはこちらです。やぁ、マスター。また来たよ」
― バーにて
私「マスター、いつもの」
私「え、いいでしょう？ 行きつけのバーを作るのは重要ですよ」
私「で、そうそう。証明の話ですよ。あなたはプログラムに証明って...」
― 奥の方の席から話し声が聞こえてくる
Z「この記事だよこの記事。え、読んだ？」
Y「読んだ読んだ。証明のやつでしょ」
私「おやおや、ちょうどこの記事についてお話なさっているようですよ」
私「どうやらプログラマーさんお二人のようです。これは興味深いですねぇ」
私「どうでしょう、少し彼らの話に耳を傾けてみませんか。いや、これ、私の悪い癖なんですけどね」
私「ここのバーに来ると、他のお客さんのお話を盗み聞きするのが楽しいんですよ」
私「あなたも少し聞いてみませんか。はい、それでは少しだけ、お二人のお話を聞いてみましょう...」
...
......
.........
............
Z「自分も昔はテストは糞だと思ってたなぁと」
Y「今もそうなんじゃないの」
Z「人の心は変わるものなのさ」
Y「あ、マスター、ジントニックで」
Z「じゃあ僕はジンジャーエールで」
どのようなテストが糞か
Y「まぁあれだよ、テストが糞かどうかは置いておいて、糞なテストはある」
Z「そう！ まさにそれなんだよ！」
Y「人力テスト」
Z「人力(笑)」
Y「二つとか三つとか」
Z「それそれ。三つとかね、五つかもしれないけど、人力でテストケース与えるやつね」
Y「糞だな」
Z「10あったら良いってもんじゃない」
Y「わかる」
Z「広い意味ではテストなんだろうけどさ」
Y「そのプログラムが幾つかのケースで正しいだろうなっていうテスト」
Z「それ」
Y「いやー 確かにねー まぁそれがダメなんじゃなくて、それだけ、そのー 確かめるだけで満足する人間が糞なんだよ」
Z「うんうん」
ランダムテスト
Y「昔さー」
Z「ん？」
Y「おまえHaskellやってたじゃん」
Z「うんうん。まぁ今はほとんど触ってないけどねー」
Y「QuickCheckだっけ？ あるじゃん」
Z「あーうんうん」
Y「あれはいいと思うけどな」
Z「うーん、まぁあれは確かに良い感じがするなぁ」
Y「君が言ったら言語に対する主観が入る気が」
Z「(苦笑)」
Y「でも手動よりはいくらかはマシな」
Z「確かにね。ランダムテストは一万十万ってケースで確かめられるからね」
Y「その安心さはあるね」
Z「文字列のデータとかさ、まぁabcとかなわけ。手動でやるとね」
Y「うん」
Z「ランダムチェックで与えられる文字列ってさ、もうバイナリーなわけ(笑)」
Y「あー分かる。そんな糞みたいな入力でも正しいっていうなら」
Z「糞って言っちゃったよ(笑)」
Y「糞なのがいいんだよ」
Z「そういうことね」
コーナーケース
Z「あとさ―、ああいうランダムチェックのテストケースを自分で作ろうと思ったらさ、なんでかは分からないけどコーナーケースから与えようって思っちゃうよね」
Y「うーんと」
Z「テスト用のリスト作ってって言われたらまず空リストから始めたくなるじゃん」
Y「あーなんとなく分かる」
Z「最初は空リストにして、長さ100以下でランダムに長さ決めて1000ケースとか与えてさ、次に長さ1000以下で100ケースとか、まぁ適当だけど」
Y「うんうん」
Z「手動テストじゃコーナーケース忘れちゃうじゃん」
Y「慎重な人なら書くと思うけどなぁ」
Z「例えばさ、引数が三つあってさ」
Y「うん」
Z「一つでも空リストなケースって7通りあるじゃん」
Y「えーっと、うんまぁそうかな」
Z「手動でコーナーケース書くの大変だぞ」
Y「コーナーケースとは何かっていうのもアレだけどね」
Z「空リストとか空の文字列とかはそうなんじゃないの」
Y「いやいや、アルゴリズムによってコーナーケースが何かは変わってくるよ」
Z「あー、まぁそれはそうかもな」
Y「まぁとにかく、コーナーケースが空リストだったら、それって一個だから問題なんだよね」
Z「一個...？」
Y「その型になるデータすべての中で、一個だけじゃん」
Z「そうそう。それ考えるの超重要...その型になるデータすべてが幾つあるか」
Y「本当にランダムなケースが与えられるならさ、コーナーケースになる確率って大体の型で0に収束しちゃうよね。どんなアルゴリズムでもね」
Z「そこなんだよなー ランダムてか、まぁ確率がユニフォームに分布するならね」
Y「真の意味でランダムなチェックより、コーナーケースの確率を上げたテストのほうが良さそうな」
Z「そこでQuickCheckですよー！」
Y「あーはいはい」
Z「まぁ言語を問わず、ランダムテストのフレームワークって大体そうなってると思うけどね。空の配列からスタート」
Y「そうじゃないと意味ないもんなぁ」
Z「うんうん」
Y「もっとコーナーケースがややこしいようなアルゴリズムだと、確率が0になっちゃうから難しいよね」
Z「次元が低いから必ず0になるんだよね」
Y「次元？」
Z「うん。三つ引数持つ場合は、立方体をイメージするんだよ」
Y「あーなるほど。コーナーケースは側面だから次元が低いのか」
Z「そうそう。コーナーケースの割合は全体の中では0に収束しちゃう」
Y「なるほどね」
テストが糞なのではない、言語が糞なのだ
Z「単純に数字とか考えてもさ、Haskell以外の言語使ってる人って、よく耐えられるなぁって思うわけ」
Y「え？なんで？」
Z「Haskellの整数はさ、無限精度の」
Y「あー (机をぽんと叩いて人差し指でZを指す) 言いたいことは分かった」
Z「だよねー(笑)」
Y「足し算するだけでもさ」
Z「そうそう(笑) 足し算するプログラムさえ、どういう入力で上手く動くのか分からないよね」
Y「足してオーバーフローしない範囲(笑)」
Z「それ(笑)」
Y「要はさ、入力がintって言ってるくせに、その型の全てのデータでは上手く動かないわけ」
Z「オーバーフローするからね」
Y「言語が糞だからだよ」
Z「それ(苦笑)」
Y「まして足し算して割り算して掛け算してっていうプログラムがさ、どういう入力で正しく動くのかなんて、もう誰にも分からない」
Z「その点Haskellは」
Y「あーはいはい」
Z「まぁまぁ」
Y「んー 確かにじゃあC++書く人もみんなgmp使えばってはならないもんなー Haskellはそういうややこしさを言語レベルで解決してくれてる」
Z「関数はtotalであるべきなのだよ」
Y「わかる」
確率論チックに
Y「逆にさ、intって言ったらさ、有限個なわけじゃん」
Z「そうだね」
Y「逆に使えるじゃん。つまり、全てのデータを確かめられる」
Z「まあね。原理上有限時間内でね」
Y「普通は実時間的に無理なわけだけど」
Z「バグを生む可能性のあるケースが何%あるかってことだよ」
Y「まぁそうだよねー」
Z「例えばさ、オーバーフローとか無視してさ、プログラムが動かないケースが、その型のデータの中で0.1%あったとしよう」
Y「うん」
Z「1000個やったら1個はテストが落ちるわけじゃん」
Y「うーん、それはよくある間違いだけどな―」
Z「どういうこと？」
Y「本当はさ、0.999を1000乗してさ...(スマホを取り出して計算する) ...4割以下なわけだ」
Z「あーそうそう。ランダムテストだったら一万個くらいはテストするとしよう。そしたら？」
Y「(0を付け足して) えーっと0.999の10000乗は0.00004...あれ、かなり小さいな」
Z「それなんだよなぁ」
Y「バグが見つかるってわけね」
Z「ケース増やしたら指数関数的に減衰するからね」
Y「バグを見逃す確率がね」
Z「そうそう」
テストケースはランダムか
Z「バグを生む入力ケースが、その型の中で偏ってたりしたらアレかもね」
Y「うーん (少し考えて) でもそれは大丈夫なんじゃないかなぁ」
Z「そうだっけ」
Y「だってさ、テストケースがユニフォームならさ」
Z「真の意味でユニフォームならね」
Y「うーむ」
Z「たしかにアレか。テストが偏っていたとしてもさ、そのテストケースがテストしたい関数にとってランダムならいい気もする」
Y「といいますと」
Z「ランダムテストが吐くテストケースがさ、配列でさ、10以上の長さの配列は含まないとしよう」
Y「それはまずいな」
Z「どうして」
Y「だって、10より長い配列でバグるプログラムなら、そのバグは見つけられないじゃん」
Z「それはそうだけどね、配列に一つだけ0があるときだけバグるプログラムがあるとしよう」
Y「あー」
Z「そういうプログラムにとったらさ、長さの偏りは関係ないわけ。0が偏っていなければ、テストケースはランダムに見えるわけ」
Y「プログラムによって、テストケースのランダムさは違うってわけね」
Z「テストフレームワークとかは、どういう使われ方するかわからないからさ、あらゆるランダム性がいるんだろうけどね」
Y「ランダム性が重要かはいまいちよく分からんのよなぁ」
Z「コーナーケースはテストケースに含めて欲しいけど、それ以外はランダムであって欲しい、みたいな」
Y「コーナーケースはアルゴリズムによって違うんだけどね」
Z「まぁまぁ。でも自明なコーナーケース、例えば空リストとかは入れて欲しい」
Y「文字列だったらスラッシュが入ってたりとかかな」
Z「どうして？」
Y「ファイル名に使えないからだよ」
Z「ああなるほど」
単体テスト不要論
Z「僕はプログラマーじゃないから分からないけどさ」
Y「うん」
Z「めちゃめちゃ実装が難しいプログラムを二つ書いたとするじゃん」
Y「うん」
Z「それの二つを組み合わせたプログラムがさ、殆ど上手く動くなら、どっちのプログラムも高い確率で正しい気がする」
Y「あー何となく分かる」
Z「この感覚を確率論的に説明できないかなぁ」
Y「うーん...(髪の毛をクルクルしすぎて、癖っ毛になってしまっている)」
Z「書いたプログラムがバグる確率が5割としよう」
Y「高いな」
Z「まぁいいじゃん。それらを結合したプログラムにバグがない確率は25%だよね」
Y「あーうん、バグがない確率をかければいいはず」
Z「あーそっか。結合するときにバグを生まないとする」
Y「うん」
Z「つまり、結合したプログラムがバグっている確率は75%なんだよね」
Y「増えた」
Z「そうだよ。バグる確率はどんどん増えていくんだよ」
Y「なるほど...(少し考えている)...」
Z「取り敢えず、結合しまくって、バグを潰せばいい」
Y「(まだ考えている)...」
Z「逆に言うとね」
Y「うん」
Z「結合したプログラムが81%正しいプログラムとするじゃん」
Y「うんうん」
Z「そしたらさ、元々のプログラムはどっちも90%正しいわけ」
Y「おお」
Z「あるいは、一方は100%正しくて、他方が81%正しいっていうケースもある」
Y「なるほどね」
Z「すごくない？」
Y「つまり、結合したプログラムのバグを潰せば、単体のプログラムのバグっている確率も小さくなるはずだと」
Z「大きくなることはないよね」
Y「すごい」
Z「単体テストとは何だったのか(笑)」
Y「結合したプログラムがバグっていたら、バグの特定が難しいんだよー(笑)」
Z「なるほど(苦笑)」
証明は業務に使えるのか
Y「最初の話って証明のアレだったじゃん」
Z「忘れてた(笑)」
Y「証明は...うん(白目)」
Z「証明最高ぉおおおおお！！！ (思わず乾杯の格好をする)」
Y「ってなればいいんだけどね」
Z「うん (グラスを机の上に置く)」
Y「業務で作るようなプログラムに証明なんてあったもんじゃない」
Z「そうなのかなぁ」
Y「Coqとか」
Z「Agdaだっけ」
Y「うん」
Z「どうなの」
Y「使えたもんじゃない」
Z「うーん そうなのかな」
Y「趣味でやってる人は知り合いにいるんだけどね。業務のコード証明してるかって聞いたらその人黙っちゃったよ」
Z「(大爆笑)」
Y「(一緒になって笑う)」
Z「(落ち着いてから) まぁそういう方向に行って欲しいのはあるよね」
Y「難しいだろうなぁ」
Z「一万のテストケースをくぐり抜けたコードより、証明されたコードの方が絶対正しいじゃん」
Y「うん」
Z「コーナーケースの数はどんどん小さくなるからね」
Y「うんうん」
Z「世の中証明されたコードばかりになって欲しいなぁ」
Y「夢物語だね」
Z「停止性との関連も気になるけどね」
Y「どっちにしろ、ランダムテストするほうが、すぐにできて楽でいいよ」
証明のしかた
Z「別にさ、証明して、コードを自動生成しろって言ってるわけじゃないよ」
Y「といいますと」
Z「究極の目標としてはいいかもしれないけどね」
Y「うん」
Z「例えばさ、日付と日付の間の日時を計算するコードを書いたとしよう」
Y「ライブラリーに任せるけどね」
Z「自分で書いたとする」
Y「うん」
Z「証明したくなるじゃん」
Y「うーん」
Z「閏年はちゃんと計算しているのかとか、2100年を超える時は、2000年を超える時はとか」
Y「閏年ねぇ」
Z「自動生成しなくても、書いたコードと証明の式が対応してたらいいんだよ」
Y「対応...」
Z「intの割り算ならガウスの記号を使ってきちんと証明するとか」
Y「なるほど」
Z「まぁユリウス通日使えば楽なんだけどね」
Y「ああ、こないだ教えてもらったやつね」
Z「うん。ユリウス通日の安定感は半端ない」
Y「証明を与えちゃえば、後に書くコードはほぼ間違いなく正しいからなぁ」
Z「そうそう。証明は、コアの部分だけすればいい。整数の計算の部分だけとかね」
Y「あとは、それを使うコードは、ランダムチェックして、テストを通れば証明が外挿されるイメージか」
Z「だいたいそんな感じ」
Y「証明かぁ」
Z「証明できた時のスッキリした感は半端ないよ。なんせ自分が書いたコードを自分の手で証明したんだからね」
Y「それを引き継ぐのは大変だけどね」
Z「ある。自己満足になってしまうかも」
Y「(笑って、ジントニックの追加を頼む)」
何をテストすればいいのか
Z「テストってさ」
Y「うん」
Z「何をテストするのさ」
Y「(笑)」
Z「実装が二つあったらさ、出力が同じになったらいいんだけどさ」
Y「それは結構あるよ。受け継いだコードをリファクタリングしたりね」
Z「あーなるほど。他の言語で実装し直したりした時とかも」
Y「そうそう。割とあるんだよなー」
Z「でもさ、最初に実装する人はどうするんだよ」
Y「そりゃまぁ性質とかさ」
Z「うん」
Y「(また髪の毛をいじる)」
Z「逆関数とかは」
Y「あーそれ結構あるよ」
Z「うんやっぱり」
Y「ある型とある型を双方向に変換するプログラムがあって」
Z「うん。そのプログラムをと
としよう」
Y「うん」
Z「全ての入力に対して
、
を確かめたらいい」
Y「そうそう。そういうのは結構ある」
Z「逆関数チェックね」
Y「うんうん」
Z「完璧に逆関数じゃない場合もあるんじゃないかなぁ」
Y「というと」
Z「ある性質を計算する関数があってさ」
Y「例えば長さとかね」
Z「そう。そんな感じの関数があって、をチェックするみたいな」
Y「うーん (少し考える)...つまりで変換して
で戻してきた時に長さが変わっていないみたいな感じのやつか」
Z「うん」
Y「確かにあるかもなぁ」
Z「例えばさ」
Y「うん」
Z「えっと...すぐにはあまり思いつかないわ」
Y「おいっ(笑)」
Z「まぁまぁ」
Y「うん、まぁ確かにある気がするわ」
Z「(笑って、ハイボールを注文する)」
飛行機のシステム
Z「これは有名だから知ってると思うけどさ」
Y「うん」
Z「飛行機なんかはさ、三つ独立したコンピュータで計算させてさ、多数決をとるらしい」
Y「あー聞いたことある。ロケットなんかもそうらしいよね」
Z「あーそうなのかなぁ。まぁそれってさ、ある意味でテストだよね」
Y「そうなるのかな」
Z「3つの出力が同じなら、どの3つのプログラムも正しいってことじゃん」
Y「正しいんじゃなくて、正しいことにするんだよ」
Z「(笑)」
Y「そうしないと、空飛べないもんなぁ」
Z「間違ってても合ってても意思決定は下さないといけない世界だからね」
Y「そういうシステムは僕はちょっと勘弁かなぁ」
Z「(笑)」
............
.........
......
...
私「おおっと...盗み聞きが過ぎましたかねぇ...話がだんだん面白くなってきたところで申し訳ないのですが...」
私「ちょっと家内から連絡がありましてねぇ...娘の具合が悪くなったとかで...」
私「盗み聞きの途中でほんと申し訳ありませんが、私は先に失礼させていただきます。いや、あなたともお話したかったんですけどね」
私「え？はい、ぜひぜひ、またの機会にお会いしましょう」
私「マスター、ごちそうさまでした」
