AspectJによる契約駆動開発 (準備＋蘊蓄編) - 檜山正幸のキマイラ飼育記 (はてなBlog)

そういうわけで（前のエントリーからの続きの気分）、なんかAspectJの練習をしたくなりました。メイヤー・ファンの僕としては、最初の課題に契約（contract）をやってみたい。"The AspectJ(TM) Programming Guide"の1.3節"Development Aspects"にも、"Pre- and Post-Conditions"、"Contract Enforcement"という例が出ているのだけど、もう少し系統的な契約記述法を探ってみましょう。

契約といえば、メイヤー先生に決まってんでしょ

契約概念について知りたいなら、迷わずメイヤー本『入門』の第7章「ソフトウェア構築への体系的アプローチ」（70ページもある）を読むべし。短い解説ならWeb上でも読めます→http://archive.eiffel.com/doc/manuals/technology/contract/。この論説で、"Design by Contract"に「(TM)」が付いていますけど、コレ、いまやEiffle Software社（メイヤー先生の会社；以前はInteractive Software Engineering社）のトレードマークなんですよ。最近ではDBCという言葉が有名になったけど、『入門』本では、"programming by contract"って言葉が使われています、僕はprogrammingのほうがシックリ来るな。

と、メイヤー先生の意見や見識について語り出すと、またキリがないので、一カ所だけ引用するにとどめます：

Eiffelで採り入れられた表明の記述方法は部分的でしかない。
…（うまくいかない例）…
このような場合には、インフォーマルな記述をコメントという形で事後条件に追加することしかできない。
完全な表明言語をEiffelに追加することは、理論的には満足できる結果を生むであろうが、完全に非現実的である。真の抽象データ型を記述できるほどに強力な形式的表明を実現するためには、集合や数列、関数、関係、そして限量記号（“すべての(for all)”や“存在する(there exists)”など）付きの一階述語を直接扱えるような表明言語が必要となる。しかし、このような概念を採り入れることは言語の性質と守備範囲を完全に変えるだろうし、言語の習得は一層難しくなるだろう -- 実現性や効率の問題はいうもでもない。

さすが、現実主義的ミニマリストのメイヤー先生だ、潔癖にならない妥協的態度がステキ。契約（論理式）で対象を完全に記述しようなんて気張ると挫折するに決まっている、ほどほどが大事！

※ 以下では「だ・である」調

ホーア式と契約

ホーア式（ホーア表明、ホーア制約）は、「事前条件P、実行文E、事後条件Q」の三つ組み（トリプル）で、通常は {P}E{Q}の形で書かれる。だけど僕は、P{E}Qの形を使っている。ブレイス（中括弧、波括弧）を使った理由はおそらく、（Pascalなどで）ブレイスがコメントだったからだろうけど、今じゃブレイスはブロックを意味する言語が多いから、P{E}Qのほうが自然に見えるので。

ところがですね、メイヤー本『招待』(9.4.4)によると、トニー・ホーア自身も最初はP{E}Qを使っていたらしいよ（トリビア）。アブラムスキー（Samson Abramsky）もP{E}Q方式を使っていたと思う。

さて、ホーア式の実行文を1つのメソッド呼び出しに限ると、P {f(x)} Q のような形になる。例えば、(x > 0) {f(x)} (result >= 15)；ここで、f(x)の戻り値は自動的に変数resultに代入されると仮定している。で、このホーア式の意味は「引数xの値が0より大きいなら、戻り値の値は15以上になる」だね。

ホーア式と契約は、概念も用語法もほとんど同じだけど、「契約は、簡略化したホーア式と同じ」ってわけではない。(x > 0) {f(x)} (result >= 15)の例で、引数xが-1の（つまり、事前条件が満たされない）とき、ホーア式としては真（問題なし）だが、契約としては偽（問題あり）となる。

もう少し正確にいうと、事前条件違反は、メソッドfの実装者に問題はないのだけど、利用者側に問題があると解釈される。本来のホーア式が、実装の正しさを判定することだけにフォーカスしているのに対して、契約は利用者の正しさも同時に考慮している点が違う。

もともとのホーア流解釈がimplicationalで、メイヤー流をconjunctional（またはrelational）といったりもするようだ。これは、実行文が空のときを考えて、P{}Qの論理的解釈が P⇒Q か P∧Q かによる違い。

契約駆動開発とそのツール

契約を適切に使って開発を進めることを契約駆動開発と呼んでおきましょう、とりあえず。テストファーストを強調したテスト駆動開発とか、最近少しだけ話題の振る舞い駆動開発と同類だね。契約駆動開発をやるには、契約のツールが必要。

メイヤー先生のEiffelは当然ながら契約をサポートしている。Eiffleのメソッド（ルーチンと呼ぶのだけど）は次の形式。



f(x: INTEGER): INTEGER is

  require 

    x > 0;

  do

   -- 定義の本体

  ensure

   Result > 15;

  end -- f

無理矢理Java風（つうか、C系統風）にすれば：



int f(int x) requires (x > 0) {

  // 定義の本体

} ensures (result > 15)

とでもなるか（resultへの代入は自動でされるとする）。

Java言語にEiffelと同様な契約機能を入れる試みはいくつかある。以前、iContractってツールがあったのだけど、今は……行方不明。2001年2月の時点では、iContract: Design by Contract in Javaなんて記事も書かれたのだけど、そこで紹介されている http://www.reliable-systems.com/tools/iContract/iContract.htm はアクセスできない。それどころか、What happened to Reliable Systems ( iContract ) & MetaMata? [September 3rd, 2004 by Angsuman Chakraborty]というブログによると：

I have been trying for the last few days to access Reliable Systems and yet being unable to access the site or find any alternative download location for iContract. The irony hasn't gone unnoticed.

似た名前のJContractってのもあるけど、こちらは商用（JTestを出しているベンダーの製品）。

もうひとつJML (Java Modeling Language)もありますぜ、だんな。が、どうも実際に使っている例は少ないみたい。あっ、そいういえばJMLに関して雑誌に書いたことがあった。載ってから時間もたったから原稿を公開しておこう→http://www.chimaira.org/docs/JavaAndJML.htm。

で、次回に続く。