コンピュータ可読な複数のメタデータが付随する複数の書類に対して処理を行うシステムであって、その動作仕様が各書類に対する操作の集合として与えられており、各操作における、それを適用可能なメタデータの範囲の条件である入力条件と、それの適用後のメタデータの変化である出力条件を保持しているシステムに対する、仕様検証方法であって、前記コンピュータの処理により、前記複数の書類を、各メタデータのとりうる値で示した抽象書類の集合として表現して、コンピュータ可読な形式で保持するステップと、前記コンピュータの処理により、前記抽象書類を、前記操作の入力条件に基づき複数の抽象書類に分割するステップと、前記コンピュータの処理により、前記操作の集合の少なくとも一部の操作を適用し、その出力条件に基づき新たな抽象書類を追加するステップと、前記コンピュータの処理により、前記抽象書類の集合に対して、前記メタデータが指定する範囲の重なりに従い前記抽象書類群を分割統合すると、前記コンピュータの処理により、所定の完了条件が満たされるまで前記操作の集合の少なくとも一部の操作を適用する処理を繰り返すステップと、前記完了条件が満たされた段階で操作が終了まで至らない抽象書類があるかどうか、前記コンピュータの処理によって検証するステップを有する、仕様検証方法。前記追加あるいは分割された抽象書類は、抽象書類をノード、操作をリンクとするグラフ構造を形成するように前記コンピュータ上で保持される、請求項1に記載の方法。前記完了条件が、前記操作の適用により前記抽象書類に変化が生じないことを検出することを含む、請求項1に記載の方法。前記操作の適用により前記抽象書類に変化が生じないことを検出することに応答して、前記検証するステップに移行するまでに、少なくとも複数回、前記操作を適用する処理を繰り返す、請求項3に記載の方法。前記動作仕様が、前記メタデータの特定の状態で記述される終了条件を含み、前記検証するステップが、前記終了条件を満たす前記抽象書類から、前記グラフ構造を逆順にたどって終了マークをつけるステップと、該たどった結果、終了マークがついていない前記抽象書類が見つかることに応答して、検証失敗と判定するステップを含む、請求項2に記載の方法。初期抽象書類から、前記終了マークがついていない前記抽象書類までのパスを、失敗例として提示するステップを含む、請求項5に記載の方法。コンピュータ可読な複数のメタデータが付随する複数の書類に対して処理を行うシステムであって、その動作仕様が各書類に対する操作の集合として与えられており、各操作における、それを適用可能なメタデータの範囲の条件である入力条件と、それの適用後のメタデータの変化である出力条件を保持しているシステムに対する、仕様検証プログラムであって、前記コンピュータに、前記複数の書類を、各メタデータのとりうる値で示した抽象書類の集合として表現して、コンピュータ可読な形式で保持するステップと、前記抽象書類を、前記操作の入力条件に基づき複数の抽象書類に分割するステップと、前記操作の集合の少なくとも一部の操作を適用し、その出力条件に基づき新たな抽象書類を追加するステップと、前記抽象書類の集合に対して、前記メタデータが指定する範囲の重なりに従い前記抽象書類群を分割統合するステップと、所定の完了条件が満たされるまで前記操作の集合の少なくとも一部の操作を適用する処理を繰り返すステップと、前記完了条件が満たされた段階で操作が終了まで至らない抽象書類があるかどうか、検証するステップを実行させる、仕様検証プログラム。前記追加あるいは分割された抽象書類は、抽象書類をノード、操作をリンクとするグラフ構造を形成するように前記コンピュータ上で保持される、請求項7に記載のプログラム。前記完了条件が、前記操作の適用により前記抽象書類に変化が生じないことを検出することを含む、請求項7に記載のプログラム。前記操作の適用により前記抽象書類に変化が生じないことを検出することに応答して、前記検証するステップに移行するまでに、少なくとも複数回、前記操作を適用する処理を繰り返す、請求項9に記載のプログラム。前記動作仕様が、前記メタデータの特定の状態で記述される終了条件を含み、前記検証するステップが、前記終了条件を満たす前記抽象書類から、前記グラフ構造を逆順にたどって終了マークをつけるステップと、該たどった結果、終了マークがついていない前記抽象書類が見つかることに応答して、検証失敗と判定するステップを含む、請求項8に記載のプログラム。初期抽象書類から、前記終了マークがついていない前記抽象書類までのパスを、失敗例として提示するステップを含む、請求項11に記載のプログラム。コンピュータ可読な複数のメタデータが付随する複数の書類に対して処理を行うシステムであって、記憶手段と、前記記憶手段に、動作仕様が各書類に対する操作の集合として与えられており、各操作における、それを適用可能なメタデータの範囲の条件である入力条件と、それの適用後のメタデータの変化である出力条件を保持している、仕様データと、前記複数の書類を、各メタデータのとりうる値で示した抽象書類の集合として表現して、コンピュータ可読な形式で前記記憶手段に保持する手段と、前記抽象書類を、前記操作の入力条件に基づき複数の抽象書類に分割する手段と、前記操作の集合の少なくとも一部の操作を適用し、その出力条件に基づき新たな抽象書類を追加する手段と、前記抽象書類の集合に対して、前記メタデータが指定する範囲の重なりに従い前記抽象書類群を分割統合する手段と、所定の完了条件が満たされるまで前記操作の集合の少なくとも一部の操作を適用する処理を繰り返す手段と、前記完了条件が満たされた段階で操作が終了まで至らない抽象書類があるかどうか、検証する手段を有する、仕様検証システム。前記追加あるいは分割された抽象書類は、抽象書類をノード、操作をリンクとするグラフ構造を形成するように前記コンピュータ上で保持される、請求項13に記載のシステム。前記完了条件が、前記操作の適用により前記抽象書類に変化が生じないことを検出することを含む、請求項13に記載のシステム。前記操作の適用により前記抽象書類に変化が生じないことを検出することに応答して、前記検証する手段を実行する前に、少なくとも複数回、前記操作を適用する処理を繰り返す、請求項15に記載のシステム。前記動作仕様が、前記メタデータの特定の状態で記述される終了条件を含み、前記検証する手段が、前記終了条件を満たす前記抽象書類から、前記グラフ構造を逆順にたどって終了マークをつける手段と、該たどった結果、終了マークがついていない前記抽象書類が見つかることに応答して、検証失敗と判定する手段を含む、請求項14に記載のシステム。初期抽象書類から、前記終了マークがついていない前記抽象書類までのパスを、失敗例として提示する手段を含む、請求項17に記載のシステム。従って、この発明の目的は、メタデータの組み合わせの複雑さを軽減して検証することを可能ならしめる技法を提供することにある。この発明の他の目的は、書類中心アーキテクチャにおいて、処理が進まなくなる書類があるかどうかを効果的に検証することを可能ならしめる技法を提供することにある。本発明は、上記課題を解決するためになされたものであり、本発明の基本的着想は、書類そのものを扱うのでなく、書類にメタデータを関連付けた抽象書類として管理することにある。本発明のシステムは、論理的な書類入れを用意し、書類入れに初期状態の複数の抽象書類を入れ、それに対して可能な処理操作を適用し、抽象書類の状態遷移図を作成する。そして、本発明のシステムは、生成された状態遷移図において、すべての抽象書類が終了状態に到達するかどうかを検証する。このとき好適には、本発明のシステムは具体的には、抽象書類に対して各処理の適用を繰り返す。そして入力条件に応じて抽象書類を分割し、出力された抽象書類を既存の抽象書類と統合する。より具体的に本発明の処理手順を記述すると、以下のとおりである。各処理を、どういう条件の時発動するかと処理後の各メタデータがどうなるかに着目して抽象化する。このとき、具体的にどんな処理をするかは気にしなくてよい。書類の初期状態としてありえるメタデータのバリエーションだけ書類入れに入れる。このとき、書類は抽象化されたもので、メタデータのとりうる範囲だけが記述されている。この抽象書類群に対し、で抽象化した各処理を順に適用し遷移図を作る。具体的には、以下のようにする。まず、処理の入力条件に沿って抽象書類群を分割する。抽象書類群に処理を適用し、処理の出力条件に沿った抽象書類を追加する。抽象書類のうち、メタデータに重なりがあるものを分割統合する。各処理終了条件も含むについてを繰り返し、変化がなくなったら終了する。出来上がった遷移図で、すべての抽象書類が終了状態に到達していれば検証成功である。このとき、終了条件に到達できない抽象書類があったら、その遷移を報告する。また、一回も使われなかった処理があったらそれも報告する。この発明によれば、書類中心アーキテクチャにおいて、書類をメタデータの値の範囲で抽象書類に分割した後、それに対して可能な処理を適用することにより、合理的な手続きで書類中心システムの設計仕様が正しいかどうかが検証可能となる。また、どのような処理手順でそれが発生するかを提示でき、さらに、使用されない処理を発見することも可能となる。以下、図面に基づき、この発明の実施例を説明する。特に断わらない限り、同一の参照番号は、図面を通して、同一の対象を指すものとする。尚、以下で説明するのは、本発明の一実施形態であり、この発明を、この実施例で説明する内容に限定する意図はないことを理解されたい。図1を参照すると、本発明の一実施例に係るシステム構成及び処理を実現するためのコンピュータハードウェアのブロック図が示されている。図1において、システムパス102には、CPU104と、主記憶RAM106と、ハードディスクドライブHDD108と、キーボード110と、マウス112と、ディスプレイ114が接続されている。CPU104は、好適には、32ビットまたは64ビットのアーキテクチャに基づくものであり、例えば、インテル社のPentium商標4、Core商標2Duo、Xeon商標、AMD社のAthlon商標などを使用することができる。主記憶106は、好適には、4GB以上の容量をもつものである。ハードディスクドライブ108は、好適には例えば、500GB以上の容量をもつものである。ハードディスクドライブ108には、個々に図示しないが、オペレーティングシステムが、予め格納されている。オペレーティングシステムは、Linux商標、マイクロソフト社のWindows商標7、WindowsXP商標、アップルコンピュータのMacOS商標などの、CPU104に適合する任意のものでよい。ハードディスクドライブ108にはさらに、図2に関連して後述するメインルーチン202、設計仕様ファイル204、メタデータクラス抽出ルーチン208、抽象書類分割ルーチン210、抽象書類追加ルーチン210、分割統合ルーチン214、分割ルーチン216、統合ルーチン218、検証ルーチン220が格納されている。これらの処理ルーチンは、C、C、C、Javaなどの既存のプログラミング言語処理系で作成することができ、オペレーティングシステムの働きで、これらのモジュールは適宜主記憶106にロードされて実行される。これらのモジュールの動作の詳細は、図2の機能ブロック図を参照して、より詳細に説明する。キーボード110及びマウス112は、所定のGUI画面図示しないを操作して、上述の処理ルーチンなどを起動したり、文字を打ち込んだりするために使用される。ディスプレイ114は、好適には、液晶ディスプレイであり、例えば、XGA1024×768の解像度、またはUXGA1600×1200の解像度などの任意の解像度のものを使用することができる。ディスプレイ114は、仕様の検証結果を表示するために使用される。図1のシステムは更に、バス102に接続された通信インターフェース116を介して、LAN、WANなどの外部ネットワークに接続されている。通信インターフェース116は、イーサネット商標などの仕組みにより、外部ネットワーク上にあるサーバやクライアントコンピュータなどのシステムとデータのやりとりを行う。書類中心アーキテクチャのシステムは、集中管理されるデータ記憶システムへのアクセスを行うが、互いには直接やりとりしない複数のコンピュータシステムからなるように規約の定められたソフトウェアアーキテクチャ基づくものであるが、この発明のシステムは、書類中心アーキテクチャの仕様を検証するためのシステムであるため、書類中心アーキテクチャのシステムである必要はない。すなわち、この発明のシステムは、パーソナルコンピュータ、ワークステーション、メインフレームなど任意の形態のコンピュータ装置上で実装可能である。また、図1では、ネットワーク接続された形態として示されているが、これには限定されず、スタンドアロンの形態でも実施可能である。また逆に、ネットワーク接続された複数のコンピュータ装置により並列分散処理する形でも実施可能である。図2は、本発明を実施するための論理構成を示す機能ブロック図である。図2において、コンピュータ可読な形式でハードディスクドライブ108に保存されている設計仕様のファイル204は、より具体的には、図3に示すように、初期書類の条件を示す情報302と、操作306a、306b、306k、および終了条件304を含む。図3には具体的に示さないが、一つの実施例では、書類の種類毎に設計書があり、その各々に対応してXMLスキーマが与えられる。メタデータもXMLスキーマによって記述される。抽象書類205a、205b、205mは、書類をメタデータの値の範囲で分割した論理的なオブジェクトであり、これらの抽象書類は、好適には、割り当てた主記憶106の領域である書類入れ206に配置される。なお、書類入れ206は、主記憶106の空き容量が十分でないなら、ハードディスクドライブ108に確保するようにしてもよい。図2に戻って、メインルーチン202は、好適にはディスプレイ114上にGUI図示しないを表示し、キーボード110やマウス112など操作によりユーザの処理を受付け、全体の処理を統合するルーチンであり、その処理の詳細は、図4のフローチャートを参照して後で説明する。メタデータクラス抽出ルーチン208は、仕様の操作からメタデータのクラスを抽出する処理を実行するルーチンであり、その処理の詳細は、図5のフローチャートを参照して後で説明する。抽象書類分割ルーチン210は、処理の入力条件に沿って抽象書類群を分割する処理を実行するルーチンであり、その処理の詳細は、図6のフローチャートを参照して後で説明する。抽象書類追加ルーチン212は、抽象書類群に処理を適用し、処理の出力条件に沿った抽象書類群を追加する処理を実行するルーチンであり、その処理の詳細は、図7のフローチャートを参照して後で説明する。分割統合ルーチン214は、抽象書類のうち、メタデータに重なりがあるものを分割統合する処理を実行するルーチンであり、その処理の詳細は、図8のフローチャートを参照して後で説明する。分割ルーチン216は、抽象書類分割ルーチン210及び分割統合ルーチン214に呼び出されて、抽象書類を分割する処理を実行するルーチンであり、その処理の詳細は、図9のフローチャートを参照して後で説明する。統合ルーチン218は、分割統合ルーチン214に呼び出されて、抽象書類を統合する処理を実行するルーチンであり、その処理の詳細は、図10のフローチャートを参照して後で説明する。検証ルーチン220は、検証処理を実行するルーチンであり、その処理の詳細は、図11のフローチャートを参照して後で説明する。次に図4を参照して、メインルーチン202が実行する全体のフローについて説明する。ステップ402で、メインルーチン202は、メタデータクラス抽出ルーチン208を呼び出して、仕様からメタデータのクラスを抽出する。ステップ404で、メインルーチン202は、初期状態として指定された書類を初期抽象書類として、書類入れ206に追加する。ここで書類入れ206とは、コンピュータシステムとしては、好適には主記憶に割り当てられたメモリ領域であり、そこにオブジェクトとしての書類が配置される。ステップ406で、メインルーチン202は、設計仕様204から処理操作306a、306b306k及び終了条件304のうちの1つを取り出す。ステップ408で、メインルーチン202は、抽象書類分割ルーチン210を呼び出して、ステップ406で取り出した処理の入力条件に沿って抽象書類群を分割する。このとき、分割された抽象書類は、元の抽象書類と置き換わり、元の抽象書類が持っていたリンクを保持する。このことは、図12乃至図20に関連して後述する例を参照することで、一層よく理解される。ステップ410で、メインルーチン202は、抽象書類群に処理操作を適用し、抽象書類追加ルーチン212を呼び出して、処理の出力結果に沿った抽象書類を追加する。この時、操作適用前の抽象書類と操作適用により追加された抽象書類はリンクで結ばれる。言い換えると、抽象書類群は、抽象書類をノード、操作をリンクとするグラフ構造を形成する。ステップ412で、メインルーチン202は、分割統合ルーチン214を呼び出して、書類入れ中のメタデータに重なりがある抽象書類を分割統合する。分割統合ルーチン214は適宜、分割ルーチン216と、統合ルーチン218を呼び出す。ステップ414で、メインルーチン202は、すべての処理および終了条件について行ったかどうか判断し、そうでなければステップ406に戻る。もしすべての処理について行ったと判断すると、メインルーチン202はステップ416に進み、前回このステップを行ったときから書類入れの中の抽象書類に変化があったかどうかを判断し、変化がなかった場合はステップ420の検証処理に進む。変化があった場合はステップ418に進み、一群の処理の適用を所定回数繰り返したかどうか判断する。所定回数繰り返していなければステップ406に戻り、所定回数繰り返した場合はステップ420の検証処理に進む。ステップ420でメインルーチン202は、検証ルーチン220を呼び出して、検証処理を行う。次に図5のフローチャートを参照して、仕様からメタデータのクラスを抽出するための、メタデータクラス抽出ルーチン208の処理について説明する。ステップ502では、メタデータクラス抽出ルーチン208は、仕様から処理を1つ取り出す。なお、ここでは終了条件も処理の一つとして考える。ステップ504では、メタデータクラス抽出ルーチン208は、その処理の入力条件として使われている属性をメタデータとして登録する。ステップ506では、メタデータクラス抽出ルーチン208は、その処理の出力条件として使われている属性をメタデータとして登録する。ステップ508では、メタデータクラス抽出ルーチン208は、全ての処理について行ったかどうか判断し、もしそうなら処理を終える。そうでないなら、ステップ502に戻る。次に図6のフローチャートを参照して、指定された処理の入力条件に従って抽象書類群を分割する、抽象書類分割ルーチン210の処理について説明する。抽象書類分割ルーチン210は、ステップ602で、書類入れから抽象書類を1つ取り出す。ステップ604で、抽象書類分割ルーチン210は、抽象書類に当該処理を適用済みかどうか判断し、もしそうならステップ610に移る。抽象書類に当該処理を適用済みでないと判断すると抽象書類分割ルーチン210は、ステップ606で、抽象書類の一部が当該処理の入力条件を満たしているかどうか判断し、そうでなければステップ610に移る。ステップ606で、抽象書類の一部が当該処理の入力条件を満たしていると判断すると、抽象書類分割ルーチン210は、ステップ608で入力条件を満たす部分を抽象書類から分割して、ステップ610に移る。なお、ステップ608の分割処理は、分割ルーチン216によって行われる。ステップ610で、抽象書類分割ルーチン210は、全ての抽象書類について行ったかどうか判断し、そうでなければステップ602に戻り、もしそうなら処理を終わる。次に図7のフローチャートを参照して、抽象書類群に指定された処理を適用し、処理の出力条件に沿った抽象書類を追加する、抽象書類追加ルーチン212の処理について説明する。抽象書類追加ルーチン212は、ステップ702で、書類入れから抽象書類を1つ取り出す。ステップ704で、抽象書類追加ルーチン212は、抽象書類に当該処理を適用済みかどうか判断し、もしそうならステップ710に移る。抽象書類に当該処理を適用済みでないと判断すると抽象書類追加ルーチン212は、ステップ706で、抽象書類が当該処理の入力条件を満たしているかどうか判断し、そうでなければステップ710に移る。なお、抽象書類分割ルーチン210により、抽象書類の一部のみが入力条件を満たしているという状態は起こらないことに留意されたい。抽象書類は全体が当該処理の入力条件を満たすか全体が当該処理の入力条件を満たさないかのいずれかである。ステップ706で、抽象書類の一部が当該処理の入力条件を満たしていると判断すると、抽象書類追加ルーチン212は、ステップ708で適用後の出力条件に合った抽象書類を書類入れに追加し、元の抽象書類から矢印でつなぐ。このとき、適用した処理の名前は矢印の属性として保持しておく。そして、ステップ710に移る。なお、抽象書類から、あるいは抽象書類への矢印については、図12~図20の具体例を参照して後で説明する。ステップ710で、抽象書類追加ルーチン212は、全ての抽象書類について行ったかどうか判断し、そうでなければステップ702に戻り、もしそうなら処理を終わる。次に図8のフローチャートを参照して、抽象書類のうち、メタデータに重なりがあるものを分割統合する処理を行う、分割統合ルーチン214の処理について説明する。分割統合ルーチン214は、ステップ802で、書類入れから抽象書類を1つ取り出す。ステップ804で、分割統合ルーチン214は、取り出した抽象書類に他の抽象書類とメタデータの条件の重なりがあるかどうか判断し、そうでないならステップ810に移る。取り出した抽象書類が他の抽象書類とメタデータの条件の重なりがあると判断すると、分割統合ルーチン214は、ステップ806で、分割ルーチン216を呼び出して、それぞれの抽象書類から、重なっている部分を分割して取り出す。次に分割統合ルーチン214は、ステップ808で、統合ルーチン218を呼び出して、重なっている部分を1つの抽象書類に統合し、ステップ810に進む。ステップ810で、分割統合ルーチン214は、全ての抽象書類について行ったかどうか判断し、そうでなければステップ802に戻り、もしそうなら処理を終わる。次に図9のフローチャートを参照して、分割ルーチン216の処理について説明する。ステップ902で、分割ルーチン216は、抽象書類から指定された部分、すなわち、ステップ804で重なりと認識された部分やステップ606で入力条件を満たしていると判断した部分を切り離し、2つの抽象書類に分割する。ステップ904では、分割ルーチン216は、分割前の抽象書類から出て行く矢印について、処理操作を再適用し、下流の抽象書類を分割する。ステップ906では、分割ルーチン216は、分割前の抽象書類に入ってくる矢印について、各書類の逆処理が行える場合はそれを行い、上流の抽象書類群を分割する。ステップ908では、分割ルーチン216は、新たに分割された抽象書類があるかどうか判断し、もしあればステップ904に戻り、なければ処理を終わる。次に図10のフローチャートを参照して、統合ルーチン218の処理について説明する。ステップ1002では、統合ルーチン218は、メタデータの範囲指定が同じである2つの抽象書類を1つにまとめる。ステップ1004では、統合ルーチン218は、統合後の抽象書類に入ってくる矢印、出て行く矢印について、統合前の両方の抽象書類のものを保持するように接続を行う。次に図11のフローチャートを参照して、検証ルーチン220の処理を説明する。ステップ1102では、検証ルーチン220は、終了条件を満たす抽象書類群から、矢印を逆向きにたどり、たどりつけるすべての抽象書類に終了可能のマークを付ける。矢印で結ばれた抽象書類は、グラフ構造を形成するので、この場合、深さ優先探索などの既知の一般的なグラフ訪問アルゴリズムを使用することができる。ステップ1102では、検証ルーチン220は、書類入れ中のすべての抽象書類に終了可能のマークがついたかどうか判断し、もしそうなら、検証成功1108として処理を終わる。もし書類入れ中の抽象書類で終了可能のマークがついていないものが存在すると判断すると、検証ルーチン220は、初期抽象書類から、マークがついていない抽象書類に至るパスを、失敗する例として、好適にはディスプレイ114上に提示し、検証失敗1110として処理を終わる。次に図12~図20を参照して、書類中心システムにおける、本発明の処理の具体例を説明する。ここで先ず、以下の前提を想定する。実際のメタデータは一般的に、これよりも複雑であるが、便宜上、簡単な例で説明することを理解されたい。書類にはAとBというメタデータがついている。初期書類:Aは0以上20以下の値で、Bは0処理X:Aが30未満の書類に対して処理を行い、結果としてAを40、BをAとする。処理Y:Aが10より大きく50未満の書類に対して処理を行い、結果としてAを100とする。処理Z:Aが40以上でBが10未満の書類に対して処理を行い、結果としてBを100とする。終了条件:AとBがともに100になった書類を処理終了とする。以上の前提において、この書類中心システムの正しさを検証するのが、この実施例のシステムの機能である。この実施例のシステムはまず、図12に示すように、初期状態の抽象書類を書類入れ206中に用意する。次に、この実施例のシステムは、図13に示すように、初期状態の抽象書類に処理Xを取り出して適用する。これにより、0≦A≦20B0というメタデータをもつ抽象書類から、A400≦B≦20というメタデータをもつ抽象書類が生成される。これは図4のフローチャートでは、ステップ406からステップ412までの処理に対応する。ただ、この段階では、ステップ408とステップ412では、分割や統合の要件は満たさないので、具体的な処理は行われない。次に、この実施例のシステムは、図14に示すように、処理Yを取り出し、ステップ408において、処理Yが適用可能な部分を分割する。そして図15に示すように、ステップ410において処理Yの結果の抽象書類を書類入れに追加する。次にこの実施例のシステムは、図15の抽象書類の状態において、図示するように、ステップ410で2つの抽象書類に重なりを見出して、重なっている部分を分割統合する。その結果、書類入れ中の抽象書類は、図16の状態になる。次に、この実施例のシステムは、処理Zを取り出し、ステップ408、410及び412を実行する。その結果の様子は図17に示すとおりである。次に、この実施例のシステムは、終了条件1回目を適用して、AとBがともに100になった書類を処理終了とする。その結果の様子は図18に示すとおりである。以上で、すべての処理と終了条件について1回目の適用が完了したので、ステップ416に進むが、前回初期状態から書類入れの抽象書類の状態に変化があったため、2回目の適用ステップを行うためステップ406に戻る。2回目の適用ステップでは、1回目と同様にまず処理Xを取り出し2回目、ステップ408、410及び412を実行するが、変化がない。そこで次に、この実施例のシステムは、処理Yを取り出し2回目、ステップ408、410及び412を実行する。その結果の様子は図19に示すとおりである。この後この実施例のシステムは、処理Zを適用2回目、終了条件を適用2回目、処理Xを適用3回目、処理Yを適用3回目と適用するが変化がないので、図4のステップ416が否定的になって検証処理ステップ420へと進む、できあがった状態遷移図図19に対するステップ420での検証処理の結果、図20及びに示す遷移パターンで、処理が行われない書類が生成されることがわかる。よって、この実施例のシステムは、仕様は正しくないという判定を下す。以上のように、特定の実施例に従い、本発明を説明してきたが、本発明は、特定のオペレーティングシステムやプラットフォームに限定されず、任意のコンピュータシステム上で実現可能であることを、この分野の当業者なら理解するであろう。