二度書く - 教えて！アロイ人！

プログラムを二度書くことの必要性

データエントリーでのベリファイ

　まだ大学生だった頃、データ入力のアルバイトをしていたのですが、その作業内容は「エントレックス」という機械に、二人の人がペアで同じデータを入力し、その両方を比較するというものでした。当時から「絶対に間違っていてはいけない伝票のような情報を入力する際は、互いに影響を与え合わない二者で同じ作業を平行して行い、結果を突き合わせる、ということは普通に行われていました。
　ところが、ソフトウェアの製造に関してはこういったことは僕の知る限り行われていません。仕様書が書かれ、それを見ながらプログラムを作って、仕様書を見ながらテストをして（同じ人が！）、という具合に進んでいきます。これらの作業が、並行して行われているということはありません。そんな提案をしたら、「コストのこと考えろ」と言われるに決まっています。まぁ確かにそれはないでしょう。

仕様書作成は「内包的」なプログラミング作業

　仕様を作成するという作業は「プログラムがどうあるべきか」を事細かに、特定の言語で書く作業です。細かく書けばそれだけ仕様書としての完成度は上がります。しかしよく考えると、「プログラムがどうあるべきかを特定の言語で書く」というのはプログラミングと同じ作業で、「特定の言語」の違いこそあれ、等価な作業と言えなくもありません。
　それならば、いっそのこと「仕様書を書く」という作業自体を一種のプログラミングと考えても無理はなさそうです。仕様を考えることは、外から内側に追い込むようにプログラムを定義していくことです。プログラムが満たすべき条件、性質を満たすものはどういうものか、ということを厳格に記述するということは、「内包的（外側から内側に包み込んでいくような・・・）」な側面で捉えたプログラミングそのものです。

従来のプログラミングは「外延的」なプログラミング作業

　対して、いわゆる「プログラミング」という作業は、プログラムの中身を一つ一つ列挙していくような作業です。小さいところから始めて、外に外に結晶が成長していくように作られるプログラムです。

そしてベリファイ

　こうして違う言語で同じプログラムを二度書き、その結果を突き合わせる、ということは、データエントリーでのベリファイ作業に通じるものがあります。あるべきプログラムを二つのプログラムで外側と内側から追い込んでいき、その結果が一致することを確認することが、正しい仕様とプログラムのありかただと思うのです。幸い、仕様書はプログラムとして書かれていますから、あらゆるパターンで実行して動きを検証することができます。時間的に許される限りにおいて、多くのパターンで二つのプログラムを動かし、同じであることを検証できるのです。これが（単体）テスト作業になります。

新しい開発スタイルへ

　XPというものが提唱されて久しいですが、その先を見て、以下のような開発スタイルを提唱してみたいと思います。

1. 基本設計までは、いわゆるSEがこれまでと同じように行う
2. その後、機能設計とプログラミングに相当する作業は、同時並行で二人の人間が行う。その際、機能設計はAlloyで、プログラミングは従来の手続き型言語で行う。作業中、二人は「何を作るか」について毎日密に連絡を取り合ってもかまわないが「どう作るか」については触れない（その必要はないはず）。
3. 両方のプログラミングが完成したら、Alloyで、起こりえる事象のパターンの入力条件と出力条件（そのスジの言葉では事前条件と事後条件）を時間の許す範囲で（XMLなどに）出力し、それをテストツールにかけてプログラムの実行結果と比較する。
4. 結果が異なる場合、どちらが間違っているかを人間が検証する。Alloy側が間違っていた場合はモデルを修正し、プログラムが間違っていた場合はプログラムを修正し、再度テストを流す。
5. 両者が一致した時点で単体テスト完了とする。
6. Alloyのソースと、そこからもう少し分かりやすい図を作成して機能設計ドキュメントとする。

　このようにして、プログラムの内包的な定義と外延的な定義が一致するようなところを目指すのです。

現実と理想

　とはいえ、実際にAlloyを使って、例えば300人月規模のプログラムの定義が書けるのか、といわれると、まだ夢物語の感はぬぐえません。しかしそれでも、このようなアプローチを取っている手法の中では、Alloyはかなり現実的な方向に振られている方です。まずこのあたりから初めて形式手法にある程度みんなが馴染んでくれば、それなりに世の中も変わってくるのではないかというのが今の僕の心境です。

（文責：片山 功士　　　2011/11/14）

今日： - 人
昨日： - 人
トータル： - 人