しかし、この元のドキュメントめっちゃわかりにくいなあ。訳もひどいがそもそもの文章があまりにわかりにくい。あまり国語(書いた人にとっては英語か)を学んでないと見た。文章が構造化されておらず、話がとびまくり。内容の説明とその内容の実現方式がどう難しかったが、ごっちゃに書かれている。 ちゃんと書け。
以前は,「JPFはJavaのバイトコードに対するな明示的状態ソフトウェアモデルチェッカ*1」と答えていた.しかし,現在,JPFは,まるでアーミーナイフのように,あらゆる種類の実行環境の検証が可能なソフトウェアであるといえる. あなたが形式手法を良く知らないのなら,JPFは以下の処理をするものであると考えるとよい.JPFは,対象のプログラムを一度(通常のVMはもちろん一度だけしか実行しません)だけでなく,理論的に可能なすべての入力によって実行を繰り返すことにより,実行経路上で潜在的に生じえるデッドロックや補足されない例外のような違反がないかどうかをチェックする.もし,このような違反を発見した場合,JPFは,どのような実行によってこの違反に達したのかという,実行経路を示す.またJPFは,問題にたどり着くすべての実行ステップにおける情報を保持しており、この点で,JPFは通常のデバガと異なる.
JPFはどのような種類の不具合を見つけることができるのであろうか?JPFをただインストールしただけの状態でも,JPFはデッドロックと補足されない例外(たとえば NullPointerExceptions?やAssertionErrors?)を発見することができる.さらに,あなたが自分自身でプロパティクラスやリスナエクステンションを実装すれば,他の特性(たとえば,リソースの競合など)のチェックもできるようになるのである. では,JPFが対象にできるプログラムはどのようなものであろうか? JPFのVMは,プラットフォーム依存のネイティブコードを実行することはできない.よって,一般論で言えば,JPFはネイティブメソッドの呼び出しをしないJavaプログラムのみを対象にすることができる.この制約は,テスト対象のアプリケーションにおいて,どのような標準ライブラリを利用することができるかに関しての制約となる.ネイティブコードを呼び出すライブラリを利用できるようにするために,JPDは,Model Java Interface(MJI)を用意している.しかし,現時点ではjava.awtやjava.netは対応しておらず,java.ioの一部に対応しているのみである. もう一つの制約として,アプリケーションの大きさがある.JPDが実行状態を保持するため,なんら状態の抽象化をしない場合,おおよそ〜10kloc程度(もちろんコードの中身によるが)のアプリケーションでないと効率的にチェックができない. 標準ライブラリの利用制限とプログラムコードの大きさの制限から,JPFは,主に完全な手続き的プログラムで記述されたモデルであるようなアプリケーションに利用されている.JPFは,特にJavaプログラムのコンカレンシーの検証に利用される.つまり,スケジュールされた連続処理の網羅的な探査のために使われる.
なぜJPFは普通のテストでは不可能なことができるのであろうか?それは、JPFが「非決定性」を扱うことができるからである。一方、テストドライバーは、たとえば、処理の実行順序などの非決定性を制御できない。というのも、その制御は、実行環境(VM)が制御するからである。また、ランダムな入力データのような非決定性も、提供するAPIを用いたユーザの実装によって簡単に実現可能である。非決定性をシミュレートすることは単にすべての非決定的な選択をシステマティックに実現するだけではない。バックトラッキングと状態の一致判定が可能になるということである。
理論的に、明示的状態モデル検証はきわめて厳密なやり方である。なぜならすべての選択を探索するからであり、ソフトウェアに何らかの問題があれば必ず発見できる。残念ながら、ソフトウェアのモデル検証は、この厳密性のために10kloc程度の小さなプログラムに対してのみ適応が可能である。なぜなら、複雑なプログラムになると、状態数はコンピュータが計算できる限界を上回ってしまうからである。この問題は状態爆発として知られており、原子的な処理から構成される複数のプロセスがどのような実行順序をとりうるかを考えるとわかりやすい。
JPFは状態爆発に起因するスケーラビリティの問題を3つの方法で解決している。一つ目は検索戦略を選択できるようにしていること、二つ目は、状態数の削減、3つ目は状態保持のための必要なメモリ量の削減である。
今まで示したJPFの特徴からわかるように、JPFはもはやクラシカルなモデル検証ではないことは明らかである。JPFを動的でランタイム指向の検証目的として実行システムのフレームワークとして考える人もいるであろう。JPFは、ある種のアプリケーションやある種の特性に特化して採用することにより、ソフトウェアモデル検証のシステマティックなスケーラビリティの問題を克服しようとしている。であるから、将来的な開発を駆動する設計方針は拡張性である。ここでは、二つの拡張の機構を示す。一つ目は検索/VMLリスナ、二つ目はModel Java Interface(MJI)である。