前置きは十分したぞ。で、息切れしてどうする?! あいだがあいてしまっちゃ いけません。ソフトウェア開発にまつわる話を開始しなくちゃ。
本屋を覗いてみたら、村上春樹編集長による『少年カフカ』って本が目に付 いた。外観は書籍と言うよりは雑誌、しかもマンガ雑誌風。タイトルも『少年〜』 なんて付けているくらいだから、マンガ的デザインを狙っているのだろうけど、 中身は字がいっぱい！
村上春樹さんの小説『海辺のカフカ』のホームページ（Webサイト）の内容を 印刷物にしたようなもの -- こんな本の作り方していいのか？ って、僕らも 似たような手口で本作ろうとしてるんだから、人のことは言えないわな。それ に村上さんが楽して本を1冊でっちあげたかっていうと、そうではないね。読 者からの膨大なメールに返事している。すっごい大変そう。
だいたいね、“某F社のSEクズレ”の山崎と“黒服と銀盆”で暮らし ていた檜山のコンビと、世界的大作家であらせられる村上春樹氏を比較しても の言っちゃいけない。いや、どうも失礼しました。思わず、『少年カフカ』買っ てしまいました。金950円（税別）なり。
で、やっと本論だ。
信頼性の高いソフトウェアを作りたい、とは誰でも思うことだ。「そうはいっ ても納期がねぇ」とか「うちのプログラマじゃ、あんまり期待できない」とか、 いろいろと言い訳はしたいだろうが、「信頼性なんてどうでもいい」と正面切っ て言える人はいないだろう。
ところで、信頼性ってなんだろうか？ 実務にも理論にも精通しているコンピュー タ・サイエンティストであるバートランド・メイヤーの定義を紹介しよう。彼は、 「信頼性」という言葉が曖昧であるとして、「正確さ(Correctness)」と「頑 丈さ(Robustness)」に分けている。「正確さ」とは、仕様によって定義された とおりに動作すること。「頑丈さ」とは、仕様によって定義されてない異常事 態においても合理的（つまり理不尽じゃない）動作をすることである。
「正確さ」は、まーいいとして、「頑丈さ」の定義は結局曖昧なままだ。仕様に よって定義されてないことも合理的に行う、とは言っても、“合理的である” ことの定義が存在しない。もし、「かくかくしかじかのように振る舞え」と決 めるなら、それは仕様の一部となるだろうから、仕様外の振る舞いを問題にし ている「頑丈さ」の議論ではなくなる。メイヤーも、もちろんこの本質的な （避けがたい）曖昧さは認識していて、現実的な配慮として「破壊的な行動を 起こさないように」といった指針を示すにとどめている。
そういう事情で、正確に議論できるのは「正確さ」のほうだ。そして、正確 な、正確なだけで必ずしも頑丈とは言えないソフトウェアを作ることでさえ、 実に気が遠くなるほどに難しい。実際に正確なソフトウェアが作れれば（頑丈 さの条件を忘れても）、それでも十分に、世間で言う「信頼性の高いソフトウェ ア」になりえると思う。だから以降の話では、正確さにフォーカスしよう。
メイヤーの「正確さ」の定義でも、仕様という概念が出てくる。仕様が正しさを判定す る基準だから、仕様がないとそもそも「正確さ」の議論ができない。だから仕 様は大事ですって -- って普通なるのだが、最近、「仕様」の評判はハナハダ かんばしくない。山崎がチラっと言及していたXP（eXtreme Programming）な んかだと、「仕様？ いまどきそんなもん書いてるの、遅れてるねぇ、ばかじゃ ないの」と言われかねない。
実際、古典的な意味での仕様 -- つまり、僕らの世代が四半世紀前に教わっ たような意味での仕様は、現在では重要性が薄れている。かつての仕様は、流 れ図で処理の流れが示してあり、UIを決める画面デザインのスケッチが並び、 遷移図で画面の順番と分岐が指示され、‥‥ その他諸々のことが自然言語で 記述されていた。図の描き方はいろいろな手法や流儀があったし、アルゴリズ ムの説明には疑似コードも使われていた。要するに、これさえ読めばシステム を作れる（はずの）処方箋なのだ。
古典的な意味での仕様と、それに基づく開発プロジェクトが、いかにして （ほぼ必然的に）破綻するか、という話は面白いのだけど、いまここで述べる のはやめよう。事実として、「システム作成の処方箋として仕様書」はうまく 機能しなかったことは指摘しておこう。
さてさて、仕様なんて役に立たないってことになると、せっかくはじめよう としていた「正確さ」の話ができないことになる。大丈夫、古き良き時代（い や、古き悪き時代）の仕様概念がもはや通用しないってことなんだから、“新 しいタイプの仕様”について考えればいい。もっと言えば、“新しいタイプの 仕様”を作り出してやろう、くらいのつもりで考えてみたらいい。とにかく僕 らの目的は、「正確な」ソフトウェアを作ることなんだから。
ここまで話すと、それほど古くさくはない「仕様策定の方法論」とか「形式 的な仕様記述言語」のことを思い起こす人がいるかもしれない。全然関係ないっ てわけではないが、あんまりその方向に話を進める気はない。机上の空論には したくないからね。具体的に使える道具と、その背景を示せたらいいな、と思っ ている。具体的な道具とは、JUnitやiContractのような（いずれもJavaベース の）既存のツール、あるいは比較的簡単に自作できそうなユーティリティのこ とだ。
だからといって、道具の使い方を指南しようとは思ってない -- そんな役回りに僕が適任と は言い難い。机上の空論じゃ困るのだが、実は僕は理屈が大好きだから、具体 的／実際的なツールと背後の理屈を結ぶ線を示せたらいいなと思っている。
じゃぁ、その理屈は何か？ それはね、「セオリーの理論」だ。えっ、なんじゃ そりゃ？ と思ったでしょう。セオリーはtheoryだから、「セオリーの理論」 は「理論の理論」となり、わけわからない。多少とも混乱を避けるために、 theoryを「理論」とは書かないでカタカナ書きの「セオリー」とする。そのカ タカナ書きのセオリーが、実は新しいタイプの仕様そのものなのだ。
先走ってもう少しだけ説明しておくと（いま、分かる必要は全然ないけど）、 セオリーは、Javaなどのインターフェースにアサーションを付け加えたものだ と思ってよい。よく勉強している人なら、ホーア（Hoare）論理をオブジェク ト指向に適合させる話だと思えば雰囲気がつかめるだろう。もっとよく勉強し ている人になら、セオリーが数理論理学／モデル理論に出てくるtheoryのこと だと言っても通じるかもしれない。えっ、通じない？ いいんですよ、先走っ ただけだから。
じゃ、続きはまた。