ソフトウェアのソースコードを、異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換するソースコード変換装置で実行されるソースコード変換方法であって、前記変換ルールは、前記ソースコードを特定のプログラミング言語に依存しない形式である中間形式で表現されたソフトウェアへ変換する第1変換ルールと、前記変換された中間形式で表現されたソフトウェアを抽象化する第2変換ルールと、前記抽象化された中間形式で表現されたソフトウェアを前記検査コードに変換する第3変換ルールと、を含み、前記方法は、前記ソースコードを入力するステップと、少なくとも一つの前記第1変換ルールの入力を受け付けるステップと、少なくとも一つの前記第2変換ルールの入力を受け付けるステップと、少なくとも一つの前記第3変換ルールの入力を受け付けるステップと、前記入力された第1変換ルールを用いて、前記ソースコードを前記中間形式で表現されたソフトウェアへ変換し、前記変換された箇所を第1逆変換ルールに記憶するステップと、前記入力された第2変換ルールを用いて、前記変換された中間形式で表現されたソフトウェアを抽象化し、前記抽象化された箇所を第2逆変換ルールに記憶するステップと、前記入力された第3変換ルールを用いて、前記抽象化された中間形式で表現されたソフトウェアを前記検査コードへ変換するステップと、前記第2逆変換ルールを用いて、前記抽象化された中間形式で表現されたソフトウェアを前記抽象化される前の中間形式で表現されたソフトウェアに変換するステップと、前記第1逆変換ルールを用いて、前記抽象化される前の中間形式で表現されたソフトウェアをソースコードである抽象化ソースコードに変換するステップと、を含むことを特徴とするソースコード変換方法。請求項1に記載のソースコード変換方法であって、前記変換された中間形式で表現されたソフトウェアを抽象化した場合、前記抽象化された箇所と、当該抽象化に用いられた第2変換ルールと、を前記第2逆変換ルールに記憶し、前記方法は、前記抽象化ソースコードを出力するステップを含み、前記抽象化ソースコードを出力するステップでは、前記第2逆変換ルールを用いて、前記抽象化された箇所と当該箇所の抽象化に用いられた第2変換ルールとの関係を出力することを特徴とするソースコード変換方法。請求項2に記載のソースコード変換方法であって、前記抽象化ソースコードを出力するステップでは、前記抽象化ソースコードを含み、前記抽象化に用いられた第2変換ルールを適用するか否かの選択操作を受け付け可能な画面を出力し、前記方法は、前記抽象化に用いられた第2変換ルールを適用するか否かの選択を受け付けるステップと、前記抽象化に用いられた第2変換ルールを適用する旨の選択を受け付けた場合、当該第2変換ルールを、前記中間形式で表現されたソフトウェアの抽象化に用いるように設定するステップと、前記抽象化に用いられた第2変換ルールを適用しない旨の選択を受け付けた場合、当該第2変換ルールを、前記中間形式で表現されたソフトウェアの抽象化に用いないように設定するステップと、を含むことを特徴とするソースコード変換方法。プロセッサ及び記憶領域を備えるソースコード変換装置に、ソフトウェアのソースコードを、前記異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換する処理を実行させるソースコード変換プログラムであって、前記変換ルールは、前記ソースコードを特定のプログラミング言語に依存しない形式である中間形式で表現されたソフトウェアへ変換する第1変換ルールと、前記変換された中間形式で表現されたソフトウェアを抽象化する第2変換ルールと、前記抽象化された中間形式で表現されたソフトウェアを前記検査コードに変換する第3変換ルールと、を含み、前記処理は、前記ソースコードを入力するステップと、少なくとも一つの前記第1変換ルールの入力を受け付けるステップと、少なくとも一つの前記第2変換ルールの入力を受け付けるステップと、少なくとも一つの前記第3変換ルールの入力を受け付けるステップと、前記入力された第1変換ルールを用いて、前記ソースコードを前記中間形式で表現されたソフトウェアへ変換し、前記変換された箇所を第1逆変換ルールに記憶するステップと、前記入力された第2変換ルールを用いて、前記変換された中間形式で表現されたソフトウェアを抽象化し、前記抽象化された箇所を第2逆変換ルールに記憶するステップと、前記入力された第3変換ルールを用いて、前記抽象化された中間形式で表現されたソフトウェアを前記検査コードへ変換するステップと、前記第2逆変換ルールを用いて、前記抽象化された中間形式で表現されたソフトウェアを前記抽象化される前の中間形式で表現されたソフトウェアに変換するステップと、前記第1逆変換ルールを用いて、前記抽象化される前の中間形式で表現されたソフトウェアをソースコードである抽象化ソースコードに変換するステップと、を含むことを特徴とするソースコード変換プログラム。請求項4に記載のソースコード変換プログラムであって、前記変換された中間形式で表現されたソフトウェアを抽象化した場合、前記抽象化された箇所と、当該抽象化に用いられた第2変換ルールと、を前記第2逆変換ルールに記憶し、前記処理は、前記抽象化ソースコードを出力するステップを含み、前記抽象化ソースコードを出力するステップでは、前記第2逆変換ルールを用いて、前記抽象化された箇所と当該箇所の抽象化に用いられた第2変換ルールとの関係を出力することを特徴とするソースコード変換プログラム。請求項5に記載のソースコード変換プログラムであって、前記抽象化ソースコードを出力するステップでは、前記抽象化ソースコードを含み、前記抽象化に用いられた第2変換ルールを適用するか否かの選択操作を受け付け可能な画面を出力し、前記処理は、前記抽象化に用いられた第2変換ルールを適用するか否かの選択を受け付けるステップと、前記抽象化に用いられた第2変換ルールを適用する旨の選択を受け付けた場合、当該第2変換ルールを、前記中間形式で表現されたソフトウェアの抽象化に用いるように設定するステップと、前記抽象化に用いられた第2変換ルールを適用しない旨の選択を受け付けた場合、当該第2変換ルールを、前記中間形式で表現されたソフトウェアの抽象化に用いないように設定するステップと、を含むことを特徴とするソースコード変換プログラム。ソフトウェアが果たす責任が重大化していることに伴って、ソフトウェアに高い信頼性が要求される。また、ソフトウェアの規模及び複雑さが増大していることに伴って、ソフトウェアを目視によるレビュー及びソフトウェアの手作業によるテストには限界がある。モデル検査技術による信頼性を確保するためには、ソフトウェアの仕様、設計、及び実装を適切に抽象化することによって、ソフトウェアが曖昧さなく解釈されるように形式的に記述できること、並びに、ソフトウェアが特定の性質を満たしているかどうかを、自動的及び網羅的に検査できることが必要である。また、検査結果が、抽象化前のソフトウェアの仕様、設計、及び実装のどの部分に関するものであるかを対応付けし、検査結果がソフトウェアに反映される必要がある。しかし、特許文献1に開示される方法には、以下の1~4の課題が存在する。1ソフトウェアの抽象化の水準の変更が困難であること2ソフトウェアの設計変更への追従コストが高いこと3異なるモデルチェッカを用いてソフトウェアを検査する場合のコストが高いこと4利用者によって選択された抽象化水準によるモデルの検査結果と抽象化前のソフトウェアと対応づける場合のコストが高いこと上記1~4の課題について詳細に説明する。上記1の課題について説明する。特許文献1に開示される方法では、ソースプログラムの改訂等、新しいタイプの命令がソースコード内に導入された場合のみに翻訳マップが変更される。このため、利用者が抽象化の水準を変更する方法は、利用者が変換前の検査対象のソースコードに修正を加える方法と、変換後の特定モデルチェッカの入力言語で書かれた検査コードに修正を加える方法と、環境モデルに修正を加える方法とに限定される。いずれの方法においても、利用者が大きな手間を費やすことになる。上記2の課題について説明する。特許文献1に開示される方法では、使用するライブラリの変更などの設計変更が生じた場合、翻訳マップ及び環境モデルを修正しなければならない。しかし、ソースコードと当該ソースコードの変換先である検査コードとを対応付けるマップ要素によって翻訳マップが構成されていること、及び環境モデルが特定モデルチェッカの入力言語で記述されていることに起因して、利用者が設計変更に追従するように整合性を保ちながら修正することは困難である。上記3の課題について説明する。特許文献1に開示される方法では、異なるモデルチェッカを用いてソースコードを検査するためには、翻訳マップ及び環境モデルを修正しなければならない。しかし、ソースコードと当該ソースコードの変換先である前記検査コードとを対応付けるマップ要素によって翻訳マップが構成されていること、及び、環境モデルが特定モデルチェッカの入力言語で記述されていることに起因して、利用者は、翻訳マップ及び環境モデルのすべてを修正しなければならず、大きなコストを要する。上記4課題について説明する。特許文献1に開示される方法では、利用者によって選択された水準でソースコードが抽象化されて、抽象化されたソースコードに対してモデル検査が実行される。このため、利用者によって選択された水準に従って抽象化されたソースコードレベルのエラートレースと、ソースコードとを対応付けなければならない。しかし、ソースコードが利用者によって選択された基準で抽象化されているため、エラートレースには存在するが、ソースコードには存在しない箇所、及び前記ソースコードには存在するが、前記エラートレースには存在しない箇所の少なくとも一方が存在することになり、利用者はエラートレースとソースコードとを対応付けなければならず、利用者が大きな手間を費やすことになる。また、複雑なシステムの検査では、状態爆発が容易に発生し、検査を完了することができない場合がある。このような場合において、何も検査できない状態よりも、検査水準を若干落としてでも、検査できることを利用者が望む場合がある。また、繰り返し文の実行時のみに発生する特定の不具合がある場合、この繰り返し文を除去することによって、特定の不具合の検出はできなくなるものの、大幅に状態数を削減できる。これらが理由となって、検査水準と状態数とのトレードオフを、利用者側で管理したいというニーズがある。本発明は、従来の技術の課題を踏まえ、抽象化の水準等に柔軟に対応でき、かつ、抽象化水準に従ったソースコードレベルでのエラートレースと抽象化前のソースコードとを対応付けることができるソースコード変換方法及びソースコード変換プログラムを提供することを目的とする。本発明の代表的な一例を示せば、ソフトウェアのソースコードを、異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換するソースコード変換装置で実行されるソースコード変換方法であって、前記変換ルールは、前記ソースコードを特定のプログラミング言語に依存しない形式である中間形式へ変換する第1変換ルールと、前記変換された中間形式を抽象化する第2変換ルールと、前記抽象化された中間形式を前記検査コードに変換する第3変換ルールと、を含み、前記方法は、前記ソースコードを入力するステップと、少なくとも一つの前記第1変換ルールの入力を受け付けるステップと、少なくとも一つの前記第2変換ルールの入力を受け付けるステップと、少なくとも一つの前記第3変換ルールの入力を受け付けるステップと、前記入力された第1変換ルールを用いて、前記ソースコードを前記中間形式へ変換し、前記変換された箇所を逆変換ルールに記憶するステップと、前記入力された第2変換ルールを用いて、前記変換された中間形式を抽象化し、前記抽象化された箇所を前記逆変換ルールに記憶するステップと、前記入力された第3変換ルールを用いて、前記抽象化された中間形式を前記検査コードへ変換するステップと、前記変換された中間形式を抽象化するステップで記憶された前記逆変換ルールを用いて、前記抽象化された中間形式を前記抽象化される前の中間形式に変換するステップと、前記ソースコードを前記中間形式に変換するステップで記憶された前記逆変換ルールを用いて、前記抽象化される前の中間形式をソースコードである抽象化ソースコードに変換するステップと、を含むことを特徴とする。本願において開示される発明のうち代表的なものによって得られる効果を簡潔に説明すれば、下記の通りである。すなわち、抽象化の水準等に柔軟に対応でき、かつ、抽象化水準に従ったソースコードレベルでのエラートレースと抽象化前のソースコードとを対応付けることができるソースコード変換方法及びソースコード変換プログラムを提供できる。本発明では、異なる複数の変換ルールを用いて検査対象のソースコードをモデルチェッカの入力言語で記述された検査コードへ変換する。前記異なる複数の変換ルールは、検査対象のソースコードをモデルチェッカの入力言語で記述された検査コードへ変換し、抽象化する一連の処理を細粒度に分割したものであり、複数の変換ルールを組み合わせて用いることにより、前記ソースコードから前記検査コードへの変換が実現される。本発明において、検査対象のソースコードを検査コードへ変換する一連の処理を、抽象化の処理も含めて、細粒度に分割し、分割されたそれぞれを、変換ルールと呼ぶ。本発明により実現されるソースコード変換装置は、ソースコードを検査コードへ変換する場合、異なる複数の変換ルールが、利用者によって、選択され、又は入力されるためのインタフェースを所有する。前記変換ルールは、事前にソースコード変換装置内部に蓄積された複数の変換ルールの中からの選択と、利用者の記述と、のいずれかの手段により入力される。また、本発明において、変換ルールは、ソースコードを、前記ソースコードの記述言語に依存しない、汎化されたプログラム情報をもつ形式汎化モデルへ変換する実装-汎化変換ルールと、汎化モデルを抽象化する抽象化変換ルールと、汎化モデルをモデルチェッカの記述言語へ変換する汎化-検査変換ルールに分類される。換言すると、異なる複数の変換ルールは、ソースコードを特定のプログラミング言語に依存しない形式である中間形式へ変換する第1変換ルールと、前記中間形式に対して抽象化処理を行う第2変換ルールと、前記中間形式から前記検査コードに変換する第3変換ルールとに分類される。ソースコードから検査コードへの変換は、ソースコードを、実装-汎化変換ルールにより、汎化モデルへ変換するステップと、前記汎化モデルを、抽象化変換ルールにより抽象化するステップと、前記汎化モデルを、汎化-検査変換ルールにより、検査コードへ変換するステップと、の3つのステップを続けて行うことで実現される。換言すると、ソースコードから検査コードへの変換は、前記第1、第2、第3の変換ルールを各々1つ以上入力するステップと、前記第1変換ルールを用いて、ソフトウェアのソースコードを、前記中間形式へ変換するステップと、前記第2変換ルールを用いて、前記中間形式で表現されたソフトウェアを抽象化するステップと、前記第3変換ルールを用いて、前記中間形式を検証ツールの入力言語で記述された検証用コードに変換するステップの3つのステップを続けて行うことで実現される。また、本発明において、検査対象のソースコードを、検査コードへ変換する一連の処理にて、内部的に保持される情報モデルは、その形式をメタモデルにより定義される。前記モデルは、検査対象のソースコードに対応する情報をもつ実装モデルと、前述の汎化モデルと、モデルチェッカの記述言語に対応する情報をもつ検査モデルと、に分類される。実装モデルは、そのメタモデルであるメタ実装モデルにより定義され、汎化モデルは、そのメタモデルであるメタ汎化モデルにより定義され、検査モデルは、そのメタモデルであるメタ検査モデルにより定義される。前述のそれぞれのメタモデルは、データ構造の定義と、データに含まれる要素間の制約に関する情報とを保有する。また、本発明は、ソースコードを中間形式へ変換するステップでは、変換した箇所を逆変換ルールに記憶し、中間形式を抽象化するステップでは、抽象化した箇所を逆変換ルールに記憶し、変換された中間形式を抽象化するステップで記憶された逆変換ルールを用いて、抽象化された中間形式を抽象化される前の中間形式に変換するステップと、ソースコードを中間形式に変換するステップで記憶された逆変換ルールを用いて、抽象化される前の中間形式をソースコードである抽象化ソースコードに変換するステップと、を含む。以下、図面を参照して本発明の実施形態について詳しく説明する。まず、図1、図2を参照しながら本発明の基本概念を説明する。本発明では、図1に示すように、ソースコード0001に対して、ソースコード変換装置1000において、複数の変換ルール0002を組み合わせた変換処理を行うことにより、既存モデル検査装置に適合した検査コード0005へ変換する。すなわち、a変換を細粒度に分割し、複数の変換ルール0002の組み合わせとしてパッケージ化することで、柔軟な変換を実現する。b利用者検査者は、検査対象のソースコード0001を入力し、対象のソースコードと検査水準に応じた変換ルール0002を選択して、所望の検査コード0005を得る。本発明における、変換ルールの例を挙げると次の通りである。a単純な構文変換C言語の条件分岐を、検査コードの条件分岐に変換C言語の繰り返し文for文while文...を、検査コードの繰り返しに変換b外部環境のモデル化データ読込みを、ランダム入力へ置き換えc抽象化繰り返しの除去条件の簡略化図2により、本発明のソースコード変換処理における変換ルールの入力インタフェースについて、説明する。本発明によれば、細粒度に分割された複数の変換ルール0002を入力するインタフェースを所有するので、利用者による抽象化の変更は、複数の異なる変換ルール0002を選択入力する操作によって容易に実現される。すなわち、利用者による抽象化の水準の変更は、ドメイン情報、検査したい性質、及び検査水準の情報抽象化による性質への影響に応じて、利用者が複数の異なる変換ルール0002を選択して呼び出し、ソースコード変換装置1000へ入力する操作によって容易に実現される。本発明によれば、異なる複数の変換ルール0002を用いて検査対象のソースコード0001をモデルチェッカの入力言語で記述された検査コード0005へ変換する手順を含んでいる。前記異なる複数の変換ルールは、実装-汎化変換ルールと、抽象化変換ルールと、汎化-検査変換ルールとに分類され、これらの変換ルールを用いた変換は段階的に実行される。検査対象のソースコードの設計変更に追従する際には、変更に関連する変換ルールのみを変更すればよく、変更が最小限にとどめられる。加えて、実装モデルと、汎化モデルと、検査モデルとをそれぞれメタモデルで定義し、制約を加えることにより、変換ルールによる変換結果が不正でないことを検証可能となる。これによって、本実施形態では、検査対象のソースコードを検査コードへ抽象化しながら変換する一連の処理は、細粒度の変換ルールを組み合わせることで実現されるが、このような一連の処理の実現方法によって生じる変換ルールの検証コストの増大を防ぐことができる。また、異なる検査ツールにて検査するために、前記検査ツールの形式で出力する際には、メタ検査モデルと、汎化-検査変換ルールのみを作成すればよく、作成部分が最小限にとどめられる。第1の実施例次に、本発明の第1の実施例になるソースコード変換装置及び変換処理方法を、図3Aから図8Bを参照しながら説明する。図3Aは、第一の実施例となるソースコード変換装置を含むソースコード変換システムの構成例を示す図である。本発明の実施形態に適用されるソースコード変換装置1000は、検査対象のソースコード0001を検査コード0005に変換する装置であり、入力部1100と、変換処理部1200と、出力部1300と、記憶部1400と、制御部1500とを備える。2000はモデル検査ツール、3000は検査結果を示す。入力部1100は、ソースコード0001及び変換ルール0002の入力を受け付ける。記憶部1400には、変換ルール0002、メタモデル0003、及び書出しルール0004が格納される。メタモデル0003は、変換処理部1200によるソースコード001を検査コード0005へ変換する一連の処理で内部的に保持されるモデルの形式を定義するためのデータである。変換処理部1200は、検査対象のソースコード0001を変換ルール0002に基づいて検査コード0005に変換する。出力部1300は書出しルール0004に基づいて検査コード0005を出力する。制御部1500は、ソースコード変換装置1000の全体の処理を制御するための各種処理を実行するプロセッサである。なお、入力部1100、変換処理部1200、及び出力部1300は、記憶部1400に記憶される図示しない各部の各機能を実現するプログラムをプロセッサが実行することによって実現される。また、各機能を実現するプログラム、テーブル、ファイル等の情報は、不揮発性半導体メモリ、ハードディスクドライブ、SSDSolidStateDrive等の記憶デバイス、または、ICカード、SDカード、DVD等の計算機読み取り可能な非一時的データ記憶媒体に格納することができる。図3Bに、ソースコード変換装置1000の構成例を示す。入力部1100は、ソースコード入力部1101、及び変換ルール入力部1102を有する。変換処理部1200は、モデル構築部1201、実装-汎化モデル変換部1202、抽象化モデル変換部1203、及び、汎化-検査モデル変換部1204を有する。出力部1300は、検査コード書出し部1301を有する。記憶部1400は、変換ルールデータベース1401、メタモデルデータベース1402、及び、書出しルールデータベース1403を有する。ソースコード変換装置1000は、例えば、1台のコンピュータ、又は、ネットワークを介して接続された複数のコンピュータ上で動作するプログラムとして実施される。ソースコード0001と変換ルール集合0002とは、例えば、コンピュータ上の記憶装置から読込む方法と、コンピュータに接続された入力デバイスにより直接入力される方法等の方法により入力される。また、検査コード0005は、例えば、コンピュータ上の記憶装置に書出す方法と、コンピュータのディスプレイ装置に表示する方法により出力される。入力部1100は、ユーザによって入力されるデータを受付け、入力されたデータを変換処理部1200へ供給する処理を行う。入力部1100は、ソースコード0001に関する情報と、細粒度に分割された複数の変換ルール、すなわち変換ルール集合0002に関する情報とを受付け、変換処理部1200へ供給する。ある実施形態においては、入力部1100は、ユーザによる、変換処理部の駆動や制御、出力部の駆動や制御、に関する指示を受け付けてもよい。変換処理部1200には、入力部1100から、ソースコード0001の情報と、ソースコード0001に適用すべき変換ルール集合0002の情報とが供給される。また、変換処理部1200は、ソースコード0001を、変換ルール集合0002によって変換する処理を行い、変換結果の情報を、出力部1300に供給する。ある実施形態においては、入力部1100から供給される変換ルール集合0002に関する情報は、記憶部1400に格納された変換ルール0002を指し示す識別情報のみが含まれていて、変換ルール集合0002の実体を、前記識別情報を用いて記憶部1400から取り出し、変換に用いてもよい。図6を用いて、変換処理部1200及び出力部1300の詳細ついて説明する。変換処理部1200は、モデル構築部1201と、実装-汎化モデル変換部1202と、抽象化モデル変換部1203と、汎化-検査モデル変換部1204とを有する。本実施例において、変換処理部1200は、メタモデル0003図3A参照と、変換ルール0002を用いたモデル変換により、ソースコード情報1001を、検査モデル1008へ変換する。メタ実装モデル1002と、メタ汎化モデル1003と、メタ検査モデル1004とは、例えば、非特許文献2に記載のMOFにて記述される。また、例えば、非特許文献3に記載されているQVTにて、実装-汎化変換ルール1005と、抽象化変換ルール1006と、汎化-検査変換ルール1007とを記述し、モデルの変換を行う。前記変換は、既に例示した方法の他のモデル変換方法でもよく、また、複数の方法を混在させてもよい。また、ある実施例においては、実装-汎化モデル変換部1202と、抽象化モデル変換部1203と、汎化-検査モデル変換部1204とをそれぞれ独立させず、同一の部位によって行われてもよい。さらに、実装モデル1205と、汎化モデル1206と、検査モデル1008と、のそれぞれのメタモデルとして、メタ実装モデル1002と、メタ汎化モデル1003と、メタ検査モデル1004とを個別に用意せず、単一のメタモデルによって、実装モデル1205と、汎化モデル1206と、検査モデル1008とを定義してもよい。また、ある実施例においては、メタ実装モデル1002と、メタ汎化モデル1003と、メタ検査モデル1004と、は、複数の方式によって、それぞれ実装モデル1205、汎化モデル1206、検査モデル1008、の形式や制約を定義してもよい。例えば、それぞれのメタモデルは、前記MOFによる定義のほかに、非特許文献4に記載されているOCLにて記載された制約条件を含み、モデルの変換を行った際に、制約条件を満たしているかどうかの検証を行う方法があり得る。モデル構築部1201は、ソースコード入力部1101からソースコード情報1001を受け取り、実装モデル1205へ変換する。実装モデル1205の形式は、そのメタモデルであるメタ実装モデル1002によって定義される。実装モデル1205は、本発明の効果を最大限に得るためには、ソースコード情報1001と相互に変換するのに必要十分な情報を持つことが望ましいが、ある実施例では、検査コードを出力するという目的を逸しない程度にて、情報の省略や、追加があってもかまわない。ある実施例においては、モデル構築部1201は、ソースコード入力部1101と不可分な様態で実装され、ソースコード情報1001が生じない形態で処理が進んでもよい。実装-汎化モデル変換部1202は、実装-汎化変換ルール1005と、メタ実装モデル1002と、メタ汎化モデル1003とを用いて、実装モデル1205を汎化モデル1206へ変換する。汎化モデル1206は、複数のプログラミング言語における構造及び処理を表現可能なデータ構造をもつ。例えば、汎化モデル1206中では、ソースコード0001におけるIf文とSwitch文とを区別せず、選択的実行文として表現する。ある実施形態においては、実装モデル1205を、汎化モデル1206へ変換する際、実装-汎化変換ルール1005のみを用いることもあり得る。また、ある実施形態において、実装-汎化変換ルール1005が、複数の変換ルールを含む場合には、複数の変換ルールを統合して一つの変換ルールとし、実装モデル1205から汎化モデル1206への変換に利用する方法があり得る。また、ある実施形態において、実装-汎化変換ルール1005が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、実装モデル1205から汎化モデル1206への変換を行う手順があり得る。抽象化モデル変換部1203は、抽象化変換ルール1006と、メタ汎化モデル1003とを用いて、汎化モデル1206を抽象化する。抽象化の例としては、選択文における条件式を、恒真、もしくは恒偽、又は非決定的な選択で置き換える方法があり得る。ある実施例においては、汎化モデル1206を抽象化する際、抽象化変換ルール1006のみを用いることもあり得る。また、ある実施例において、抽象化変換ルール1006が、複数の変換ルールを含む場合には、複数の変換ルールを統合して一つの変換ルールとし、汎化モデル1206の抽象化に用いる方法があり得る。また、ある実施例において、抽象化変換ルール1006が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、汎化モデル1206の変換を行う手順があり得る。汎化-検査モデル変換部1204は、汎化-検査変換ルール1007と、メタ汎化モデル1003と、メタ検査モデル1004とを用いて、汎化モデル1206を、検査モデル1008へ変換する。例えば、検査コード0005がPromela形式である場合、汎化モデルにおいて選択的実行文として表現された要素は、検査モデルにおいてはIf文として表現される。ある実施形態においては、汎化モデル1206を、検査モデル1008へ変換する際、汎化-検査変換ルール1007のみを用いることもあり得る。また、ある実施形態において、汎化-検査変換ルール1007が、複数の変換ルールを含む場合には、複数の変換ルールを統合して1つの変換ルールとし、汎化モデル1206から検査モデル1008への変換に利用する方法があり得る。また、ある実施形態において、汎化-検査変換ルール1007が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、汎化モデル1206から検査モデル1008への変換を行う手順があり得る。出力部1300は、変換処理部1200より供給された、変換結果の情報を用いて、検査コード0005を出力する。ある実施例においては、検査コード0005の出力に際して、例えばモデルチェッカの記述言語の文法情報などの情報を記憶部1400から供給されてもよい。検査コード書出し部1301は、メタ検査モデル1004と、記憶部1400の書出しルールデータベース1403から取得した検査コード書出しルール1009とを用いて、検査モデル1008を検査コード0005へ変換する。例えば、非特許文献5に記載される方法にて、検査コード書出しルール1009を記述し、検査モデル1008から、検査コード0005への変換を行う。ある実施例においては、これに限らず、検査モデル1008を、検査に利用するモデルチェッカの記述形式へ変換する任意の方法でもよい。検査コード0005は、例えば、モデルチェッカとしてSPINを用いる場合には、SPINの入力言語である、Promela言語によって記述される。記憶部1400において、変換ルールデータベース1401、メタモデルデータベース1402、及び書出しルールデータベース1403のそれぞれは、例えば、関係データベース、又は、階層型データベースなどの、コンピュータ上にて実現される任意のデータ格納方式で実現される。変換ルールデータベース1401と、メタモデルデータベース1402と、書出しルールデータベース1403と、は互いに同一の方式で実現されている必要性は無く、互いに異なる方式で実現されていてもよい。また、変換ルールデータベース1401と、メタモデルデータベース1402と、書出しルールデータベース1403と、のそれぞれは、単一の方式で実現されている必要性は無く、例えば、保有すべき情報の一部を関係データベースに格納し、保有すべき情報の一部を、発明を実現するコンピュータプログラム中に組込むなど、それぞれ異なる方式の組合せで実現されていてもよい。記憶部1400は、入力部1100と、変換処理部1200と、出力部1300とが、それぞれの処理を行うのに必要な情報を供給する。例えば、記憶部1400は、変換ルールに関する情報と、メタモデルに関する情報と、モデルチェッカの記述言語の文法に関する情報とを格納する。変換ルールデータベース1401は、既に述べたとおり、変換ルールを、メタデータとともに保有する。前記メタデータは、変換ルールを選択するためのものであり、実装-汎化変換ルール1005と、抽象化変換ルール1006と、汎化-検査変換ルール1007の、それぞれ異なる情報を持つ方法があり得る。実装-汎化変換ルール1005のメタデータは、例えば、変換元ソースコードの記述言語の種類があり得る。抽象化変換ルール1006のメタデータは、例えば、抽象化を分かりやすく端的に表現した名前、簡単な説明、データの抽象化、処理の抽象化などの抽象化の種別、自然語例えばアルファベット又は数値で表現された抽象化による状態数削減効果、自然語例えばアルファベット又は数値で表現された抽象化による性質への影響、及び抽象化の適用できるソフトウェアのドメイン、があり得る。汎化-検査変換ルール1007のメタデータは、例えば、検査に使用するモデルチェッカを指し示す名前があり得る。以降、図4ないし図6を参照しながら入力部1100、変換処理部1200、出力部1300、記憶部1400、及び制御部1500の詳細を説明する。まず、本実施例におけるソースコード変換手順の一例を、図4及び図6を参照しながら説明する。本実施例におけるソースコード変換手順は、ソースコード入力ステップS101と、変換ルール入力ステップS102と、変換ルール適用ステップS103と、検査コード出力ステップS104と、を含む。このソースコード変換手順は、制御部1500が主体となって実行される。まず、ソースコード入力ステップS101において、ソースコード入力部1101によって、ソースコード0001がソースコード変換装置1000に読み込まれ、ソースコード情報1001へ変換される。ソースコード入力部1101は、利用者から入力された検査対象のソースコード0001を受け付け、ソースコード情報1001へ変換する。ソースコード0001は、例えば、JISX30101993に公開されるプログラミング言語Cにより記述される。ソースコード情報1001は、具体的には、例えば抽象構文木の形式で保持される。ソースコード情報1001の形式は、抽象構文木に限らず、構造や論理などソースコード0001の検査に要する情報を保持する、任意の形式でもよい。ソースコード入力ステップS101に続き、変換ルール入力ステップS102において、変換ルール入力部1102によって、細粒度に分割された複数の変換ルールである変換ルール集合0002がソースコード変換装置1000に読み込まれる。この変換ルール入力ステップS102では、変換前のモデルの要素と変換後のモデル要素との対応関係、及び変換によって変換前のモデルの要素に加えられる操作の少なくとも一方が定義される。変換ルール集合0002をソースコード変換装置1000に読み込む処理は、利用者による一度の操作で行われる必要性は無く、繰り返し操作により行われてもよい。また、ソースコード入力ステップS101、及び変換ルール入力ステップS102は、必ずしもこの順番で完了する必要性は無く、ソースコード入力部1101によりソースコード情報1001が生成される前にソースコード0001が入力され、かつ、変換ルール入力部1102が変換ルール入力処理のためにソースコード情報1001を要求する前にソースコード0001が入力されていればよい。したがって、ソースコード入力ステップS101の処理と、変換ルール入力ステップS102の処理とが混在する順番で処理が進んでもよい。例えば、ソースコード入力部1101がソースコード0001を受け付け、続いて、変換ルール入力部1102が、変換ルール集合0002を受け付け、続いて、ソースコード入力部1101が、ソースコード0001をソースコード情報1001へ変換する、手順があり得る。変換ルール入力部1102は、利用者から入力された変換ルール集合0002を受け付ける。利用者から変換ルール集合0002を受け付ける方法は、例えば、次に示す方法があり得る。一つめの変換ルール入力方法の例として、変換ルール入力部1102は、変換ルール集合0002の一部として、利用者が手作業で直接入力した変換ルールを受け取る。二つめの変換ルール入力方法の例として、図5Aに示すように、変換ルール集合0002の少なくとも一部は、利用者が記述した変換ルール記述0010により入力してもよい。また、入力部1100が、記憶部1400から変換ルールの一覧0015を取得し、取得した変換ルールの一覧0015を利用者に一覧などの形式で提示し、前記提示された一覧から変換ルールを利用者が選択することによって、変換ルール集合0002の入力を受け付けてもよい。すなわち、利用者が、変換ルールの入力に前置して、変換ルールの検索条件0011を入力部1100の変換ルール入力部1102に入力記述し、続いて、変換ルール入力部1102が、前記検索条件に合致する変換ルールを、記憶部1400が有する変換ルールデータベース1401から取得し変換ルール一覧0015として前記利用者に提示する。続いて、前記利用者が、提示された前記変換ルール一覧0015に含まれる一つ以上の変換ルールを選択する。この利用者によって選択された一つ以上の変換ルールを、変換ルール入力部1102が、変換ルール集合0002の一部として受け付ける。三つめの変換ルール入力方法の例として、まず、利用者が、変換ルールの入力に前置して、変換ルールの検索条件0011を変換ルール入力部1102に入力し、続いて、変換ルール入力部1102が、前記検索条件に合致する変換ルールを、変換ルールデータベース1401から取得して、変換ルール集合0002の一部として受け付けてもよい。四つめの変換ルール入力方法の例として、図5Bに示すように、入力されたソースコード0001から、変換ルール入力部1102が、変換ルールの検索条件0012を抽出、生成し、さらに、前記検索条件に合致する変換ルールを、変換ルールデータベース1401から取得し、変換ルール集合0002の一部として受け付ける。二つめの変換ルール入力方法の例と、三つめの変換ルール入力方法の例と、四つめの変換ルール入力方法の例における、変換ルール検索条件の因子としては、例えば、後述する、変換ルールデータベース1401において、変換ルールのメタデータとして格納される情報があり得る。また、五つめの変換ルール入力方法の例として、変換ルール入力部1102は、何らかの方法で入力された変換ルールを加工することにより、変換ルールを受け付ける。前記加工方法の例としては、変換ルールデータベース1401には、ソースコード0001中の変数名などをパラメタ化した状態で変換ルールを保持しておき、例えば利用者の明示的な入力による方法などにより、ソースコード0001の情報にてパラメタを埋めたものを、変換ルール集合0002に含める方法があり得る。五つめの変換ルール入力方法の例において、加工元の変換ルールの入力方法としては、既に述べた一つめの変換ルール入力方法の例など、入力された変換ルールを加工せずに用いる場合と同様の方法があり得る。変換ルール入力部1102が、変換ルール集合0002を受け付ける方法は、これらの変換ルール入力方法に限らず、変換処理部1200で用いる変換ルールの集合を受け付ける任意の方法でよく、また、これらの変換ルール入力方法の一つ以上の組合せにより変換ルール集合0002を受け付けてもよい。変換ルール入力ステップS102に続き、変換ルール適用ステップS103において、モデル構築部1201がソースコード情報1001を実装モデル1205へ変換し、続いて、実装-汎化モデル変換部1202が実装モデル1205を汎化モデル1206へ変換しS1031、続いて、抽象化モデル変換部1203が汎化モデル1206を抽象化しS1032、続いて、汎化-検査モデル変換部1204が汎化モデル1206を検査モデル1008へ変換するS1033。変換ルール入力ステップS102と、変換ルール適用ステップS103とは、必ずしもこの順番で処理が完了する必要性は無く、実装-汎化モデル変換部1202の処理までに実装-汎化変換ルール1005が入力され、かつ、抽象化モデル変換部1203の処理までに抽象化変換ルール1006が入力され、かつ、汎化-検査モデル変換部の処理までに汎化-検査変換ルール1007が入力されていればよい。変換ルール適用ステップS103に続き、検査コード出力ステップS104において、検査コード書出し部1301により、検査モデル1008が、検査コード0005として書き出される。検査コード0005の書出し先の指定は、必ずしも変換ルール適用ステップS103の後である必要性は無く、検査コード0005の書出しよりも先であればよい。例えば検査コード0005の書出し先の指定がソースコード入力ステップS101と平行して行われる手順があり得る。次に、図7、図8A、図8Bを用いて、変換の手順をより詳細に説明する。図7に示すように、本発明では、モデル変換技術を利用し、段階的に変換するために、次のような処理を行う。1ソースコード0001をこれとほぼ等価な実装モデル1205へ変換2実装モデルを特定のプログラミング言語に依存しない形式にて構造及び論理などのプログラム情報を表現する汎化モデル1206へ変換すなわち、異なる複数の第1変換ルール1005-1~1005-nの少なくとも一つを用いて、実装モデル1205を特定のプログラミング言語に依存しない形式である中間形式の汎化モデル1206へ変換する。図7の例では、第1変換ルールとして、if文→条件分岐、switch文→条件分岐、while文→繰り返し、及びfor文→繰り返しの少なくとも四つの異なる変換ルールが選択されている。3汎化モデル1206に対して、抽象化のための変換を実施すなわち、異なる複数の第2変換ルール1006-1~1006-nの少なくとも一つを用いて、前記中間形式の汎化モデル1206に対して抽象化処理を行う。図7の例では、第2変換ルールとして、データ読み込み→ランダム入力、及びデータの抽象化の少なくとも二つの異なる変換ルールが選択されている。4汎化モデル1206を、検査モデル1008に変換し、コード生成出力すなわち、異なる複数の第3変換ルール1007-1~1007-nの少なくとも一つを用いて、前記中間形式の汎化モデル1206から検査コードの生成に要する情報を有する検査モデル1008に変換する。図7の例では、第3変換ルールとして、第1変換ルールに対応した条件分岐→if文、及び繰り返し→do文の少なくとも二つの異なる変換ルールが選択されている。また、実装モデル1205、汎化モデル1206、検査モデル1008は、それぞれ構文を定義するメタモデルによりデータ構造及び意味論が定義される。このように、実装モデル1205から汎化モデル1206への変換に際しては、例えば、変換対象ソースコードの記述言語の文法が、繰り返し処理の記法としてfor文及びwhile文を含む場合、使用者がfor文を繰り返しへ変換するルールと、While文を繰り返しへ変換するルールとを、既に述べた変換ルール入力方法を用いて、第1変換ルールとして選択する。汎化モデル1206の抽象化の変換に際しては、使用者が検査水準抽象化の度合いを決定し、決定した検査水準を達成する変換ルールとして、例えば、外部データの読込みに関する命令及び一連の処理をランダムな入力へ変換するルールと、特定のデータ型をより抽象度の高い型へ変換するルールとを、既に述べた変換ルール入力方法を用いて、第2変換ルール1006として選択する。さらに、汎化モデル1206から検査モデル1008への変換に当たっては、例えば、モデルチェッカの入力言語の文法が、繰り返し処理の記法としてdo文をもつとき、使用者が繰り返しをdo文へ変換するルールを、既に述べた変換ルール入力方法を用いて、第3変換ルール1007として選択する。変換ルールは、複数のソフトウェアにまたがって適用可能な汎用的なルールなど、繰り返し利用可能なものがデータベース化される。データベースに格納された変換ルールは、使用者による検索及びルール選択の判断材料として用いられるメタ情報として、ドメイン情報や検査水準抽象化による検査への影響の情報を有する。また、変換ルールの選択方法としては、次のようなものがある。1汎用的なルール:常に選択2特定のライブラリに依存したルール:使用ライブラリ、及び検査対象のドメインを入力することで、まとめて選択3抽象化に対応したルール:検査したい性質検査水準を入力して得た変換ルール一覧から、利用者が選択して入力、利用者自身が記述して入力、又は検査したい性質などから、自動生成。図8A、図8Bに、それぞれモデルの抽象化の一例を示す。モデルの抽象化により、状態数を削減することができる。しかし、抽象化によりモデルの性質に影響を与えることがある。例えば、検出された欠陥反例が、もとのシステムに存在しない、もとのシステムに存在する欠陥を発見できない、等である。一方で、性質に影響を与えない健全な抽象化は、状態数削減効果が小さい傾向がある。本実施例によれば、細粒度に分割された複数の変換ルールを入力するインタフェースを所有することによって、利用者による抽象化の水準の変更は、変換ルールを入力する操作によって容易に実現される。すなわち、複数の細粒度の変換ルールを利用者が入力インタフェースにより選択できるため、図8A、図8Bに示す抽象化の水準を、状況に応じて利用者が容易に選定又は変更することが可能となる。ソースコード変換法は、複数の変換ルールを用いて検査対象のソースコードをモデルチェッカの入力言語で記述された検査コードへ変換する手順を有し、前記変換ルールは、実装-汎化変換ルールと、抽象化変換ルールと、汎化-検査変換ルールと、に分類され、変換が段階的に行われる。これによって、検査対象のソースコードの設計変更に追従する際には、複数の変換ルールの中の変更に関連する変換ルールのみを変更すればよく、変更が最小限にとどめられる。加えて、実装モデルと、汎化モデルと、検査モデルとをそれぞれメタモデルで定義し、制約を加えることにより、変換ルールによる変換結果が不正でないことを検証可能となる。これによって、変換ルールの検証コストの増大を防ぐことが出来る。また、モデルの変換ルールをデータベースに蓄積し、蓄積した変換ルールを再利用することによって、検査対象ソースコードの設計変更や、別ソフトウェアへの応用に、低コストで対応可能になる。第2の実施例次に、第2の実施例になるソース変換装置及びソースコード変換方法について図9~図11を用いて説明する。本実施例では、抽象化された汎化モデルをソースコードに逆変換することによって、検査対象のソースコードの抽象化された箇所を出力するステップを有する。図9は、第2の実施例になるソースコード変換装置を含むソースコード変換システムの構成例を示す図である。図9のうち、第1の実施例の図3Aに示すソースコード変換システムと同じ構成は同じ符号を付与し、説明を省略する。本実施例のソースコード変換装置1000は、入力部1100、制御部1500、出力部1300、記憶部1400、及び変換処理部4100を備える。変換処理部4100は、検査対象のソースコード0001を検査コード0005に変換する点では、第1の実施例の変換処理部1200と同じであるが、ソースコード0001を検査コード0005に変換する一連の処理で抽象化された汎化モデルをソースコードに逆変換したソースコードである抽象化ソースコード4101を出力する点で、第1の実施例の変換処理部1200と異なる。図10は、第2の実施例のソースコード変換装置の構成例を示す。図10のうち、第1の実施例の図3Bに示すソースコード変換装置と同じ構成は、同じ符号を付与し、説明を省略する。入力部1100は、第1の実施例と同じく、ソースコード入力部1101及び変換ルール入力部1102を備える。変換処理部4100は、モデル構築部4201、実装-汎化モデル変換部4202、抽象化モデル変換部4203、汎化-検査モデル変換部4204、汎化-実装モデル変換部4205、及びコード生成部4206を備える。出力部1300は、検査コード書出し部1301、及び抽象化ソースコード出力部4220を備える。記憶部1400は、変換ルールデータベース1401、メタモデルデータベース1402、及び書出しルールデータベース1403の他に、逆変換ルールデータベース4210を備える。以下、変換処理部4100について詳細に説明する。モデル構築部4201は、ソースコード入力部1101からソースコード0001を受け取り、受け取ったソースコード0001を実装モデルへ変換する。また、モデル構築部4201は、変換箇所をソースコード-実装モデル変換対応表として逆変換ルールデータベース4210に登録する。実装-汎化モデル変換部4202は、変換ルールデータベース1401から実装-汎化変換ルールを取り出し、メタモデルデータベース4221からメタ実装モデル及びメタ汎化モデルを取り出す。そして、実装-汎化モデル変換部4202は、取り出された実装-汎化ルール、メタ実装モデル、及びメタ汎化モデルを用いて、実装モデルを汎化モデルへ変換する。また、実装-汎化モデル変換部4202は、変換箇所を実装-汎化モデル変換対応表として逆変換ルールデータベース4210に登録する。抽象化モデル変換部4203は、変換ルールデータベース1401から抽象化変換ルールを取り出し、メタモデルデータベース1402からメタ汎化モデルを取り出す。そして、抽象化モデル変換部4203は、取り出された抽象化変換ルール及びメタ汎化モデルを用いて、汎化モデルを抽象化する。また、抽象化モデル変換部4203は、抽象化された箇所を抽象化変換対応表として逆変換ルールデータベース4210に登録する。汎化-検査モデル変換部4204は、変換ルールデータベース1401から汎化-検査変換ルールを取り出し、メタモデルデータベース1402からメタ汎化モデル及びメタ検査モデルを取り出す。そして、汎化-検査モデル変換部4204は、取り出された汎化-検査変換ルール、メタ汎化モデル及びメタ検査モデルを用いて、汎化モデルを検査モデルへ変換する。汎化-実装モデル変換部4205は、抽象化モデル変換部4203が抽象化処理を終了すると、逆変換ルールデータベース4210から抽象化変換対応表を取り出す。そして、汎化-実装モデル変換部4205は、取り出された抽象化変換対応表を用いて、抽象化された汎化モデルを抽象化される前の汎化モデルに変換する。次に、汎化-実装モデル変換部4205は、逆変換ルールデータベース4210から実装-汎化変換対応表を取り出す。そして、汎化-実装モデル変換部4205は、取り出された実装-汎化変換対応表示を用いて、抽象化される前の汎化モデルを実装モデルに変換する。コード生成部4208は、汎化-実装モデル変換部4205によって抽象化される前の汎化モデルが実装モデルに変換されると、逆変換ルールデータベース4210からソースコード-実装変換対応表を取り出す。そして、コード生成部4208は、取り出されたソースコード-実装変換対応表を用いて、実装モデルを抽象化ソースコード4101に変換し、抽象化ソースコード4101を抽象化ソースコード出力部4220に出力する。抽象化ソースコード出力部4220は、コード生成部4206から入力された抽象化ソースコード4101をシステム外部に出力する。例えば、ソースコード出力部4210は、抽象化ソースコード4101を外部記憶媒体へ保存したり、抽象化ソースコード4101を表示装置であるディスプレイに表示したりする。これによって、利用者が、対象ソースコードと、検査水準抽象化の度合いに応じて、変換ルールを選択することで、検査可能な検査コードに変換し、前記検査コードと同じ抽象化の水準の抽象化ソースコードを出力することが可能となり、利用者によって選択された抽象化水準によるモデルの検査結果と抽象化前のソフトウェアとの対応付けの課題が解決される。次に、本実施例の具体例について図11を用いて説明する。まず、本具体例で検査対象となるソースコード0001について説明する。検査対象となるソースコード0001では、a、b、及びcの値が定義される。具体的には、aには0が代入され、bには、iが5より大きい場合0が代入され、これ以外の場合1が代入され、cにはcの値をインクリメントした値が代入される。このソースコード0001がモデル構築部4201によって図示しない実装モデルに変換され、この実装モデルが実装-汎化モデル変換部4202によって汎化モデルに変換される。実装-汎化モデル変換部4202は、実装モデルを汎化モデルに変換する場合にソースコード0001中のif文を条件分岐に変換する。そして、抽象化モデル変換部4203は、汎化モデルの条件分岐の分岐先を固定化することによって、汎化モデルを抽象化する。具体的には、bに代入される値が0に固定化されるため、図11に示すように、汎化モデルの2行目、4行目、及び5行目が削除される。次に、汎化-検査モデル変換部4204は、抽象化モデル変換部4203によって抽象化された汎化モデルを検査コード0005に変換する。なお、図11に示すように、検査コード0005では、抽象化によってbに代入される値は0で固定されている。汎化-検査モデル変換部4204によって変換された検査コード0005がモデル検査ツール2000によって検査され、検査結果3000が生成される。また、抽象化モデル変換部4203が汎化モデルを抽象化すると、汎化-実装モデル変換部4205は、逆変換ルールデータベース4210を用いて、抽象化された汎化モデルを実装モデルに逆変換する。次に、コード生成部4206は、逆変換ルールデータベース4210を用いて、逆変換された実装モデルを抽象化ソースコード4101に変換する。抽象化ソースコード4101は、抽象化モデル変換部4203によって抽象化された箇所が利用者に把握可能な形態で出力される。図11に示す抽象化ソースコード4101は、抽象化モデル変換部4203によって抽象化された箇所が点線で囲まれた形態で出力される。なお、抽象化された箇所が利用者に把握可能な形態で出力されるためには、抽象化された汎化モデルを抽象化される前の汎化モデルに変換した箇所を汎化-実装モデル変換部4205がコード生成部4206に抽象化された箇所として通知し、コード生成部4206が当該箇所を抽象化ソースコード4101に変換する場合に、当該箇所を利用者に把握可能な形態で出力する必要がある。以上によって、抽象化された汎化モデルが、抽象化された箇所を抽象化される前の状態に戻した抽象化ソースコード4101に変換されるため、利用者は、検査結果と抽象化ソースコード4101とを対応付けやすくなる。さらに、抽象化された箇所を利用者に把握可能にして抽象化ソースコード4101が出力されることによって、抽象化された箇所は検査結果に対応しないので、利用者は、検査結果と抽象化ソースコード4101とをさらに対応付けやすくなる。第3の実施例次に、第3の実施例になるソース変換装置及びソースコード変換方法について図12及び図13を用いて説明する。本実施例では、検査対象のソースコードの抽象化された箇所と当該抽象化に用いた抽象化変換ルールとを出力するステップを有する。図12は、第3の実施例のソースコード変換装置の構成例を示す。図12のうち、第2の実施例の図10に示すソースコード変換装置と同じ構成は、同じ符号を付与し、説明を省略する。第3の実施例のソースコード変換装置に備わる変換処理部4100は、ルール適用情報付加部4301を備える点で、第2の実施例のソースコード変換装置に備わる変換処理部4100と異なる。また、第3の実施例の抽象化モデル変換部4203は、汎化モデルを抽象化した場合に、抽象化した箇所と抽象化に用いた抽象化変換ルールを特定可能な識別子とを抽象化変換対応表として逆変換ルールデータベース4210に登録する。ルール適用情報付加部4301は、抽象化モデル変換部4203によって汎化モデルが抽象化された場合、逆変換ルールデータベース4210から抽象化変換対応表を取り出す。そして、ルール適用情報付加部4301は、取り出された抽象化変換対応表に登録された抽象化に用いた抽象化変換ルールの識別子を、汎化モデルの抽象化された箇所に付加して、当該汎化モデルを汎化-実装モデル変換部4205に渡す。汎化-実装モデル変換部4205は、抽象化された汎化モデルを実装モデルに変換する場合に、実装モデルのうち、抽象化された箇所に対応する箇所に抽象化に用いた抽象化変換ルールの識別子を付加する。コード生成部4206は、実装モデルの抽象化変換ルールの識別子が付加された箇所を抽象化ソースコード4101に変換する場合、当該抽象化変換ルールの識別子を当該箇所のソースコードのコメントとして記述する。本実施例の具体例について図13を用いて説明する。図13に示す具体例は、図11に示す第2の実施例の具体例と、抽象化ソースコード4101が異なる。本実施例の抽象化ソースコード4101では、抽象化された箇所と同じ行に、コメントとして当該箇所の抽象化に用いた抽象化変換ルールが記述される。図13に示す抽象化ソースコード4101では、抽象化された箇所と当該箇所の抽象化に用いた抽象化変換ルールが記述された部分は点線によって囲まれ、どこが抽象化された箇所なのか利用者に把握可能にしている。すなわち、本実施例の抽象化ソースコード4101は、抽象化モデル変換部4203によって抽象化された箇所と当該箇所の抽象化に用いた抽象化変換ルールとの関係を利用者に把握可能な形態で出力される。なお、図13では、一つの抽象化変換ルールを用いてすべての箇所が抽象化されているが、抽象化された箇所が異なる抽象化変換ルールを用いて抽象化されていてもよいことは言うまでもない。以上によって、抽象化ソースコード4101は、抽象化された箇所と当該箇所の抽象化に用いた抽象化変換ルールとの関係が利用者に把握可能な形態で出力される。このため、利用者が検査結果を検討した結果、抽象化変換ルールを変更する必要がある場合、どの抽象化変換ルールを変更すればよいかが把握しやすくなる。さらに、第3の実施例の抽象化ソースコード4101を含む表示画面において、コメントで記述された抽象化に用いた抽象化変換ルールを抽象化モデル変換部4203で適用するか否かの利用者からの選択操作を受け付け可能な領域を設けてもよい。ソースコード変換装置1000は、抽象化ソースコード4101の表示画面を介して抽象化変換ルールを適用する旨の選択を受け付けた場合、選択を受け付けた抽象化変換ルールを抽象化モデル変換部4203で抽象化に用いるように設定する。一方、ソースコード変換装置1000は、抽象化ソースコード4101の表示画面を介して抽象化変換ルールを適用しない旨の選択を受け付けた場合、選択を受け付けた抽象化変換ルールを抽象化モデル変換部4203で抽象化に用いないように設定する。これによって、利用者は、抽象化された箇所と当該箇所の抽象化に用いられた抽象化変換ルールとの関係及び検査結果を把握しながら、抽象化変換ルールを抽象化に用いるか否かの決定を容易にすることができる。第4の実施例図14によって、本発明の第4の実施例のソースコード変換装置及び変換処理方法を説明する。この実施例においては、図33に示す検査コード出力ステップS104に続き、変換ルール入力ステップS102へ進むことで、既に入力されたソースコード0001を、繰り返し、異なる変換ルール集合0002を用いて、変換する手順をとってもよい。また、ある実施形態においては、検査コード出力ステップS104に続き、変換ルール入力ステップS102へ進み、既に入力された変換ルール集合0002の全てまたは一部と、新たに変換ルール入力ステップS102で入力された変換ルール集合0002をあわせて、変換ルール集合0002として用いてもよい。本実施例によれば、細粒度に分割された複数の変換ルールを入力するインタフェースを所有し、入力されたソースコードと、変換に用いた変換ルール集合を保存し、前記ソースコードを前記変換ルール集合の一部を入れ替えて変換できることによって、異なる抽象度の複数の検査コードを生成する場合などの、同一のソースコードを繰り返し変換する手間を削減できる。第5の実施例図15によって、本発明の第5の実施例のソースコード変換装置及び変換処理方法を説明する。本実施例では、ソースコードから検査コードを得る過程において生成される実装モデルと、汎化モデルと、検査モデルとを制約条件に基づいて検証するステップを有する。図15を用いて、変換の妥当性の検証手順を詳細に説明する。特定の変換ルールが、その変換に際して対象モデルについての前提条件をもつ場合、変換対象のモデルにおいて、前記特定の変換ルールの前提条件が、他の変換ルールの適用によって満たされなくなることがあり得る。このように前提条件が満たされないときに前記特定の変換ルールによってモデル変換を実施すると、変換結果のモデルが不正な状態になり得る。また、単に変換ルールに誤りが含まれるときも、変換結果のモデルが不正な状態になり得る。本実施例では、ソフトウェアのソースコード0001を入力するステップと、ソースコード情報1001を有する実装モデル1205を特定のプログラミング言語に依存しない形式である中間形式汎化モデル1206へ変換する第1変換ルールを入力するステップと、中間形式に対して抽象化処理を行う第2変換ルールを入力するステップと、中間形式から検査コードの情報をもつ検査モデル1008に変換する第3変換ルールを入力するステップと、ソフトウェアのソースコード0001を解析して実装モデル1205へ変換するステップと、前記第1変換ルールを用いてソフトウェアのソースコード0001を前記中間形式の汎化モデル1206へ変換するステップと、第2変換ルールを用いて、前記中間形式で表現されたソフトウェアを抽象化するステップと、第3変換ルールを用いて、前記中間形式を検査モデル1008に変換するステップと、検査モデル1008を用いて検証ツールの入力言語で記述された検査コード0005を生成するステップと、前記各段階のモデルを各々第1の制約条件0300、第2の制約条件0301、及び第3の制約条件0302に基づいて検証する充足性検証ステップと、を有する。前記各段階のモデルの、各々第1の制約条件0300、第2の制約条件0301、及び第3の制約条件0302に基づく充足性検証は、例えば、非特許文献2に開示されるMOFでメタモデルを記述することによって、又は非特許文献4に開示されるOCLによりメタモデルにより定義されるモデルに対する制約条件を記述することによって、実現される。本実施例によれば、メタモデル及び制約条件を用いることで、変換ルール同士の衝突や変換ルールの不具合による変換の妥当性を保証できる。このモデル変換では、メタモデルによって定義された形式のモデルが生成される。また、制約条件を追加し、生成されたモデルの妥当性を制約条件0300~00302で充足性検証することができる。以上、本発明者によりなされた発明を実施形態に基づき具体的に説明したが、本発明は上述した実施形態に限定されるものではなく、その要旨を逸脱しない範囲で種々変更可能であることは言うまでもない。