検証対象プログラムの処理内容を解析し、前記検証対象プログラムの言語仕様のうちの検証対象の仕様である検証対象仕様を満たすか否かを判定するための検証式を生成する検証式生成手段と、前記生成した検証式を含む検証コードを生成する検証コード生成手段と、前記検証コード生成手段が生成した少なくとも2つの検証コードについて、1つの検証コードに合成可能か否かを判定し、合成可能である場合には、1つの検証コードに合成する検証コード合成手段と、前記合成可能な少なくとも2つの検証コードについては、前記検証コード合成手段が合成した検証コードを用いて検証対象仕様を満たすか否かを判定する検証実行手段と、を備えていることを特徴とするプログラム検証装置。前記検証実行手段は、前記検証コード合成手段が合成した検証コード、及び、前記検証コード生成手段が生成し、前記検証コード合成手段が合成しなかった検証コードをそれぞれ実行して、各検証コードについて、対応する検証対象仕様を満たすか否かを判定する、ことを特徴とする請求項1に記載のプログラム検証装置。前記検証式生成手段は、前記検証対象プログラムの処理内容を解析して、前記検証対象仕様に対応する処理部分を判定し、該判定した処理部分それぞれについて、該処理部分に対応する検証対象仕様の前記検証式および該処理部分に対応する関数を示すデータを含む検証データを生成し、前記検証コード生成手段は、前記判定した処理部分それぞれについて前記検証コードを生成し、前記検証コード合成手段は、前記検証コード生成手段が生成した少なくとも2つの検証コードについて、前記検証データに基づき対応する関数を判定し、同一の関数に対応する少なくとも2つの検証コードについて、1つの検証コードに合成可能か否かを判定する、ことを特徴とする請求項1又は2に記載のプログラム検証装置。前記検証実行手段が実行した検証コードが対応する検証対象仕様を満たさない場合、前記実行した検証コードに対応する第1の関数に、前記第1の関数だけでは値が不定となる変数が存在するか否かを判定し、値が不定となる変数が存在する場合、前記第1の関数を呼び出す第2の関数を特定して、再度、前記検証対象プログラムの検証を、前記プログラム検証装置に実行させる制御手段を、備えており、前記検証コード生成手段は、再度の前記検証対象プログラムの検証時、前記第2の関数を、前記第1の関数の前記検証対象仕様に対応する処理部分の検証コードを生成する際に参照する、ことを特徴とする請求項3に記載のプログラム検証装置。前記検証コード合成手段は、前記検証コード生成手段が生成した少なくとも2つの検証コードで使用されている変数が包含関係にある場合、前記少なくとも2つの検証コードを合成可能と判定することを特徴とする請求項3又は4に記載のプログラム検証装置。前記検証コード合成手段は、前記少なくとも2つの検証コードで使用されている変数が同一であり、前記少なくとも2つの検証コードの前記検証式を除いた部分が同一である場合、前記少なくとも2つの検証コードの前記検証式を合成して1つの検証式にすることを特徴とする請求項5に記載のプログラム検証装置。前記検証コード合成手段は、前記少なくとも2つの検証コードの内の第1の検証コードで使用されている検証式及び変数を除いた部分が、もう一方の第2の検証コードで使用されている検証式及び変数を除いた部分を包含する場合、前記第2の検証コードで使用されている検証式を、前記第1の検証コードに挿入することにより検証コードの合成を行うことを特徴とする請求項5に記載のプログラム検証装置。請求項1から7のいずれか1項に記載のプログラム検証装置としてコンピュータを機能させるプログラム。しかしながら、特許文献1に記載の方法においては、分割により検証実行回数が増加し検証時間が長くなってしまう。したがって、状態数が多くなることを防ぎつつ、検証時間を短縮化することが求められている。本発明は、検証時間を短縮化できるプログラム検証装置及びプログラムを提供するものである。本発明によるプログラム検証装置は、検証対象プログラムの処理内容を解析し、前記検証対象プログラムの言語仕様のうちの検証対象の仕様である検証対象仕様を満たすか否かを判定するための検証式を生成する検証式生成手段と、生成した検証式を含む検証コードを生成する検証コード生成手段と、検証コード生成手段が生成した少なくとも2つの検証コードについて、1つの検証コードに合成可能か否かを判定し、合成可能である場合には、1つの検証コードに合成する検証コード合成手段と、合成可能な少なくとも2つの検証コードについては、検証コード合成手段が合成した検証コードを用いて検証対象仕様を満たすか否かを判定する検証実行手段と、を備えていることを特徴とする。検証式に対応する検証コードを生成し、合成可能であるものについては複数の検証コードを1つの検証コードに合成することで、プログラム検証に要する時間を短縮化することができる。第一実施形態図1は、一実施形態におけるプログラム検証装置201のハードウェア構成を示す図である。例えば、ハードディスクといった外部記憶装置204には、検証対象プログラムと、検証装置用プログラムが保存されている。中央処理装置202は、検証装置用プログラムを主記憶装置203にロードして実行することで、以下に説明する様なプログラム検証装置201が実現される。つまり、プログラム検証装置201は、コンピュータを以下に説明するプログラム検証装置201として機能させるプログラムにより実現することができる。プログラム検証装置201は、検証対象プログラムの言語仕様のうちの検証対象の仕様である検証対象仕様を、検証対象プログラムが満足しているか否かの検証を行う。なお、入出力装置205は、例えば、ディスプレイ等の表示装置や、キーボードやマウスなどの入力装置を含み、プログラム検証装置201に対するユーザの指示等の入力処理や、検証結果のユーザへの表示等の出力処理を行う。以下、検証対象プログラムがC言語で記述されており、検証対象仕様が、配列外へのメモリアクセスは行ってはならない以後、配列外参照と呼ぶ。と、0による割り算を実行してはならない以後、DIV0と呼ぶ。である場合を例にして説明を行う。なお、プログラム検証装置201が実行する検証コードはSPINで記述されているものとする。図2は、本実施形態によるプログラム検証装置201の機能ブロック図である。検証式生成部303は、検証対象プログラム309の処理内容を解析し、検証対象仕様を満たすか否かを判定するための検証式を生成して検証データ310として出力する。図3に、本実施形態の説明に使用する検証対象プログラム309を示す。なお、図3はC言語で記述されたソースコードを、図3bは、図3aのソースコードを、静的単一代入形式SSAといった、3番地コードに変換したものを示している。なお、ソースコードから3番地コードへの変換は公知の種々の方法を利用することができる。例えば、検証式生成部303は、図3に示すソースコードを、まず、図3bに示す3番地コードに変換する。検証式生成部303は、その後、ソースコード及び3番地コードに基づき、検証対象仕様に対応する処理部分を判定し、各処理部分それぞれについて検証式を生成する。具体的には、図3に示す検証対象プログラムから以下の内容を把握することできる。図3bの関数test1のline1において、prmを添え字にして、配列varにアクセスする。第3bの関数test1のline3において、D.1185による割り算を実行する。なお、line2よりD.1185はprm1に等しい。prmはtest1の引数であり、関数test1のline1~line3の間で変更されない。図3aから配列varの要素数は3である。上記内容から、関数test1に関し、配列外参照に対応する処理部分は、line1であり、line1の配列varへのアクセスにおいて、prmが0以上3未満であることを検証すれば良いことが分かる。つまり、line1の処理部分に対する配列外参照の検証式は、0<=prmprm<3となる。同様に、DIV0に対応する処理部分はline3であり、line3におけるD.1185=prm1が0以外であることを検証すれば良いことが分かる。つまり、DIV0に対する検証式は、prm1=0となる。従って、検証式生成部303は、図6aに示す検証データ310を出力する。図6において、検証IDフィールドは、検証式の識別子を示し、関数名フィールドは検証対象の関数名を示し、行番号フィールドは、検証対象仕様に対応する処理部分であり、図3bの三番地コードの行番号で示している。また、検証式フィールドは、検証対象仕様に対応する検証式を示し、コード生成フィールドは、検証コードを既に生成したか否かを示している。この時点において検証コードは生成されていないため、コード生成フィールドにはnoが設定されている。さらに、コードNoフィールドは、検証コードを生成した場合においてその番号を示し、検証結果フィールドは、検証式が検証対象仕様を満足しているか否かを示す。図2に戻り、検証コード生成部304は、図6aに示す検証データ310及び図3に示す検証対象プログラムから、検証対象仕様である配列外参照とDIV0それぞれを検証するための検証コード311を生成する。各検証コード311の生成には、公知のコードスライス法を利用できる。つまり、検証対象プログラムの依存関係を調べ、検証対象仕様に関連する値に影響する検証対象プログラムのコードのみを残し、それ以外の部分を消去して検証式を埋め込むことにより、検証コード生成部304は検証コード311を生成する。図4は、図6aの検証ID1の検証式に対応する検証コード311であり、図4は、図6aの検証ID2の検証式に対応する検証コード311である。図4aに示す様に、検証ID1に対応する検証コード311は、図3bの関数test1の当該検証式に関連するline1のprm値に影響するコードのみを残すことで生成されている。また、検証コード生成部304は、検証コードを生成したことにより、図6に示す様に、検証データのコード生成フィールドをyesに設定し、コードNoフィールドに対応する番号を設定する。続いて、検証コード合成部305は、各関数について、検証コードの合成処理を行う。合成処理の詳細については、後述するが、図4a及びbに示す2つの検証コードが使用する変数は同じであるため、合成可能である。検証コード合成部305が出力する合成後の検証コード312を図4cに示す。なお、図4cでは、各assert文を順に記述しているが、0=prm10<=prmprm<3の様に、一つの検証式としても良い。また、検証コード合成部305は、検証コードを生成したことにより、図6に示す様に、コードNoフィールドに対応する番号を設定する。次に、変換部306は、検証コード311又は312を、プログラム検証装置がサポートするモデル検証用の言語に対応する検証コード313に変換する。より詳しくは、検証コード合成部305により合成された検証式については合成後の検証コード312を、合成されなかった検証式については検証コード311を、それぞれ、検証コード313に変換する。図5は、モデル検証用の言語がSPINである場合における図4cの検証コード312の変換後の状態を示している。図5に示す検証コード313により、検証領域を関数内に限定した検証を行う事が可能となる。検証実行部307は、検証コード313を読み込んで検証式を満たすか否かを判定し、判定結果を検証データ310の検証結果フィールドに設定する。ここで、検証対象仕様を満たしていないNG場合、制御部308は、スコープ外変数の存在を判定する。つまり、対象としている関数単体では、その値が不定となる変数の存在を判定する。図3に示す検証対象プログラムの関数test1及びbに示す検証コード311の生成には、公知のコードスライス法を利用できる。続いて、S3において、検証コード合成部305は、各関数についての検証コード311の合成処理を行う。図8は検証コード合成部305による合成処理のフロー図である。なお、図8の処理は各関数について実行する。S11において、検証コード合成部305は、検証データ310から、同じ関数内の2つの検証コード311を処理対象として選択する。例えば、図6に示す検証データ310においては、検証ID1及び2で特定される2つの検証コード311を処理対象として選択する。S12において、検証コード合成部305は、各検証コード311の変数が包含関係にあるか否かを判定する。包含関係とは、一方の検証コード311の変数の総てが、他方の検証コード311においても変数として使用されている状態を意味する。なお、変数の異同は、名前及び型が同じ場合に変数が同じであると判定する。包含関係になければ、検証コード合成部305は、選択した2つの検証コード311の合成は不可と判定して処理を終了する。一方、包含関係にあれば、検証コード合成部305は、S13において、各検証コード311の変数が同じであり、かつ、検証式以外のコード部分が同一であるかを判定する。変数が同じであり、かつ、検証式以外のコード部分が同一である場合、検証コード合成部305は、S14において、検証式の合成を行うことで、合成した検証コード312を生成する。一方、変数又は検証式以外のコード部分が同一ではない場合、検証コード合成部305は、S15において、単に、選択した検証コード311の合成を行う。例えば、図4a及びbに示す検証コード311で使用されている変数prmは、その名前及び型整数:intが同じであるので、同一である。また、検証式、つまり、assert文以下のコード部分は同一より詳しくは、assert文のみであるであるため、S13の処理はYesである。なお、S13の判定はオプションであり、S12の判定がYesであれば、検証コード311は合成可能である。検証コード合成部305は、ある関数に対して3つ以上の検証コード311が有る場合、例えば、S11においてそのすべてを選択し、S12~S15の処理で合成可能な組を判定して合成後の検証コード312を生成することができる。あるいは、1つの注目する検証コード311に対して、他の1つの検証コード311を選択して図8の処理を繰り返して3つ以上の検証コードを合成することもできる。この場合、先の処理で注目する検証コード311を合成して、合成後の検証コード312を生成した場合、続く図8のS11では、合成後の検証コード312と、次の検証コード311を選択する。一方、先の処理で注目する検証コード311が合成不可であれば、続く図8のS11では、この注目する検証コード311と、次の検証コード311を選択して処理を行うことになる。いずれにしても、各関数内において、検証コードの合成を行う。図7に戻り、S4において、変換部306は、検証コード311及び/又は312を、利用するモデル検証プログラム言語に従う検証コード313に変換し、検証実行部307が検証コード313を読み込んで、検証対象仕様を満足しているか否かを判定する。S5において、制御部308は、判定結果がどちらであるかを判定し、結果をOKであれば処理を終了する。一方、判定結果がNGであれば、S6において、スコープ外変数が存在するかを判定する。スコープ外変数が存在しない場合、制御部308は、処理を終了させるが、スコープ外変数が存在する場合、S7において検証コードの生成の対象とする検証範囲を拡大して、S1からの処理を実行する。なお、検証コードの生成の対象とする検証範囲を拡大するとは、既に説明した様に、判定結果がNGとなった関数と関連する他の関数を含めて、この互いに関連する複数の関数に対してS1からS7の処理を実行することを意味する。つまり、2回目以降の繰り返しにおいて、検証コード生成部304は、検証範囲に含まれる複数の関数を考慮してコードスライスを実行することになる。以上、本実施形態においては、関数内で検証コードの合成を行った後に、まず、検証を行う。その後、検証結果がNGである場合、その範囲を増大させながら繰り返し検証を行うことで状態数を増加させることなく、確実にプログラム検証を行うことを可能にする。例えば、図2に示す検証対象プログラムにおいて、従来の様に、関数内における合成を行わないものとすると、4回の検証を行う必要がある。これに対して、本実施形態においては、関数内の検証コード311を合成することで、2回の検証のみで検証結果を取得できる。この様に、本実施形態による構成により検証時間を短縮することができる。なお、検証に用いる変数は合成前後で変化しないため、合成する事によって状態数の増加を引き起こす可能性は少ない。第二実施形態第一実施形態においては、図8のS12及びS13の判定は共にYesであった。以下、S12の判定はYesであるが、S13の判定がNoである場合について説明する。図9は、検証対象プログラム309のソースコードを、図10は、図9のソースコードに対応する3番地コードを示している。図9及び図10の検証対象プログラム309から以下の内容を把握することできる。図10の関数test2のline2において、prmを添え字にして、配列varにアクセスする。図10の関数test2のline12において、prmを添え字にして、配列var2にアクセスする。prmはtest2の引数であり、関数test2のline1~line12の間で変更されない。図9から配列var及びvar2の要素数は3である。上記内容から、関数test2に関し、配列外参照に対しては、line2及び12における配列var及びvar2へのアクセスにおいて、prmが0以上3未満であることを検証すれば良いことが分かる。従って、検証式生成部303は、図13aに示す検証データ310を出力する。検証コード生成部304は、図13aに示す検証データ310から、検証ID1の検証式に対しては、図11aに示す検証コード311を、検証ID2の検証式に対しては、図11bに示す検証コード311を生成する。また、検証コード311を生成したことにより、図13に示す様に、検証データのコード生成フィールドをyesに設定し、コードNoフィールドに対応する番号を設定する。続いて、検証コード合成部305は、各関数について、検証コードの合成処理を行う。図11a及び図11bの検証コード311で使用する変数名は共にprmであり、その型は共に整数であるため、図8のS12はYesとなる。しかしながら、図11aの検証式を除いたコード部分、つまり、line1-2以外の部分と、図11bの検証式を除いたコード部分、つまり、line2-10以外の部分は異なる。したがって、図8のS13はNoとなる。しかしながら、図11bの検証コード第1の検証コードの検証式以外のコード部分は、図11aの検証コード第2の検証コードの検証式以外のコード部分を包含している。つまり、line1-1、1-3~1-6は、line2-1、2-2、2-3、2-4、2-11に対応する。したがって、検証コード合成部305は、図11aのline1-2の検証式であるassert分を、単に、図11bのline1-2に対応する、line2-1と2-2の間に挿入することで、図11cに示す検証コード312へと合成する。また、検証コード合成部305は、合成した検証コード312を生成したことにより、図13に示す様に、コードNoフィールドに対応する番号を設定する。以下、変換部306は、検証コード312を、プログラム検証装置がサポートするモデル検証用の言語に対応する検証コード313に変換する。図12は、モデル検証用の言語がSPINである場合における図11cの検証コード312の変換後の状態を示している。図9及び10に示す検証対象プログラムの関数test2において、prmはスコープ外変数であるため、検証実行部307は、図12aの検証コード313についてはNGと判定する。したがって、制御部308は、検証範囲を広げて、再度、上述した処理を実行する様に、図2の各部を制御する。図10に示す様に、関数test2Aのline5でtest2関数の呼び出しが行われているため、2回目の実行において、関数test2Aを検証範囲に加える。図12bに関数test2Aを検証範囲に加えた場合の検証コード313を示す。図12bの検証コード313については、検証対象仕様を満たしているOKため、検証実行部307は、図13dに示す様に検証結果フィールドにOKを設定する。第三実施形態続いて、配列の添え字や割り算の分母が定数ではなく変数である場合について説明する。図14は、検証対象プログラム309のソースコードを、図14は、図14のソースコードに対応する3番地コードを示している。図14及びbの検証対象プログラム309から以下の内容を把握することできる。図14bの関数test3のline5においてD.1128による割り算を実行する。図14bの関数test3のline6においてsymを添え字にして、配列varにアクセスする。図14aからvarの配列要素数は3である。上記内容から、関数test3に関し、DIV0に対しては、line5におけるD.1128が0でないこと、配列外参照に対しては、line6における配列varへのアクセスにおいて、symが0以上3未満であることを検証すれば良いことが分かる。従って、検証式生成部303は、図17aに示す検証データ310を出力する。検証コード生成部304は、図17aに示す検証データ310から、検証ID1の検証式に対しては、図15aに示す検証コード311を、検証ID2の検証式に対しては、図15bに示す検証コード311を生成する。また、検証コード311を生成したことにより、図17に示す様に、検証データのコード生成フィールドをyesに設定し、コードNoフィールドに対応する番号を設定する。続いて、検証コード合成部305は、各関数について、検証コードの合成処理を行う。図15aの検証コード312で使用する変数はD.1228及びiであり、図15aの検証コード312で使用する変数はD.1228、i及びsymであり包含関係にある。よって、図8のS12はYesとなる。しかしながら、図15aの変数及び検証式を除いたコード部分、つまり、line1-5以外の部分と、図15bの検証式以外のコード部分、つまり、line2-6以外の部分は異なる。したがって、図8のS12はNoとなる。この場合、検証コード合成部305は、図8のS15において合成処理を行い、図16に示す合成した検証コード312を生成する。なお、第二実施形態と同様に図15bの検証コードの検証式、つまり、line2-6以外の部分は、図15aの検証コードの検証式、つまり、line1-5以外の部分を包含するものである。よって、合成処理は、図15aの検証コードのline1-5の検証式を、図15bの検証コードの対応する位置、つまり、line2-4と2-5の間に挿入することにより行われる。また、合成した検証コード312を生成したことにより、図17に示す様に、コードNoフィールドに対応する番号を設定する。以下、変換部306は、検証コード312を、プログラム検証装置がサポートするモデル検証用の言語に対応する検証コード313に変換する。図16は、モデル検証用の言語がSPINである場合における図16aの検証コード312の変換後の状態を示している。検証実行部307は、図16bの検証コード313についてはOKと判定し、図17dに示す様に検証結果フィールドにOKを設定する。以上、検証式に対応する検証コードを生成し、合成可能であるものについては複数の検証コードを1つの検証コードに合成することで、プログラム検証に要する時間を短縮化することができる。また、同じ関数内の検証コードに対して合成可能であるか否かを判定することで、簡易に判定して検証コードを合成することができる。なお、検証コードがスコープ外変数を有する場合、この検証コードに対応する関数を呼び出す関数を含める形で、検証コードを生成して、再度検証を行うことでプログラムの検証を行う。これにより、状態数の急激な増加を抑えつつ、プログラムの検証を行うことができる。、なお、検証コードの合成は、2つの検証コードの対応する関数が同一であり、かつ、少なくとも2つの検証コードで使用されている変数が包含関係にある場合に合成可能であると判定する。なお、変数が同一であり、2つの検証コードの検証式を除いた部分が同一である場合、2つの検証コードの検証式を合成して1つの検証式にすることができる。また、一方の検証コードの検証式及び変数を除いた部分が、他方の検証コードの検証式及び変数を除いた部分を包含する場合、他方の検証コードの検証式を、一方の検証コードに挿入することにより検証コードの合成を行うことができる。この様に、検証コードの合成処理は、簡易であり、検証すべき状態数を効果的に減少させることができる。