JavaとJML

この記事は「JavaWorld」誌の「私が感動したJavaソースコード」というコーナーに掲載されたエッセイの原稿です。雑誌掲載後かなり時間がたったので公開します（掲載記事とは若干の違いがあります）。記事内のURLのなかには、現在ではアクセス不可能であったり、移転したものがあるかもしれません。

キレイに書かれたコードを見ると“感心”します。ですが、それはどうも “感動”とは違うような気がします。例えば、Perlの作者であるラリー・ウォールが（Perlより前に）書いたニュースリーダー「rn」のC言語ソースコードはかなりトンデモナイものです。感心しません。が、そのえぐさは感動ものでした。

CやC++では、言語処理系やOSに関する知識に基づきトリッキーなワザを使ったヤバいコードをよく見かけました。一方、Javaはというと、プラットフォームに依存しない行儀がよいコードを書きやすいプログラミング言語です。言い換えれば、邪悪なコードが書きにくいように工夫されています。ですから、ギョッとするようなすさまじいコードにお目にかかることは少なくなってしまったようです。もちろん、これは良い傾向なのでして、アクロバティックなプログラミングを推奨する気はありません。

そうです、Javaは、計算科学やソフトウェア工学から見ても優等生プログラミング言語なのです。腕力や悪戯でいきがっている不良言語とは違います（まー、不良のほうがステキってのもあったりしますけど…）。であるなら、ギョッとするほどに正統派、すさまじくも品行方正なJavaコードはないものでしょうか？

それがあるんですよ、実は。だいぶ古い話になりますが、1999年から2000年ごろ、Vector_annotated.javaというソースコードがインターネット上に公開されていました（残念ながら今は見あたりません）。これは、究極の品行方正コードで、お行儀のよさもここまでくれば感動ものです。いったいどういうものかって？このソースコードは、Sunが提供しているVectorクラスのコードそのものです。「なるほど、標準ライブラリのコードならお手本になるくらいにキレイだろう」って、いやっ、そうじゃありません。

問題は、オリジナルのライブラリコードに追加されたコメントです。そのコメントは、オランダのバート・ジャコブス（ http://www.cs.ru.nl/~bart/）を中心とするグループにより付加されたもので、単なるコメントではなくて、JML （Java Modeling Language; http://www.jmlspecs.org/）という仕様記述言語による制約条件なのです（LIST1）。

LIST1: JMLコメント付きのJavaソースコード

/*@
  @ normal_behavior
  @  requires: (\forall (int i) 0 <= i && i < elementCount
  @                             ==> elementData[i] != null);
  @  ensures: true;
  @ also
  @ exceptional_behavior
  @  requires: elementCount > 0 &&
  @            !(\forall (int i) 0 <= i && i < elementCount
  @                              ==> elementData[i] != null);
  @  signals: (NullPointerException) true;
  @*/
public final synchronized String toString() {
 // ...
}

ジャコブスのグループは、JMLコメント付きのJavaソースコードを、ある種のコンパイラ（JMLコンパイラとは別物）と手作業で一群の論理式に変換して、定理証明系PVS（http://pvs.csl.sri.com/）を使った検証までしています。このような仕様記述と検証が現に可能であるという点がJavaの優れた特性を示しているといえるでしょう。

詳細は、 http://www.cs.ru.nl/research/reports/info/CSI-R0007.htmlから入手できる、"A Case Study in Class Library Verification: Java's Vector Class"という論文に記述されています。また、JMLについては、 "Disign by Contract with JML" ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmldbc.pdfという、DBC（契約による設計）の観点から書かれた新しい（2005年の）解説があります。

ジャコブス達のように、定理証明系による静的検証はJMLやPVSの極端にヘビーな使い方で、それゆえに感動をおぼえるのですが、仕様記述／検証ツールが一般化すれば、当たり前のことになるのしょうか。そうなることを私は期待してますが、道は遠いかもしれません。