(57)【特許請求の範囲】
【請求項１】
不変条件生成装置であって、
プログラムコードが記憶される記憶部と、
前記不変条件を生成する処理を実行する処理部を備え、
前記処理は、
前記記憶部から前記プログラムコードを読み出す第１処理と、
多項式を構成するための１又は複数の部分式を生成する第２処理と、
前記不変条件を生成する第３処理と、
を含み、
前記第２処理は、
指定部分式を取得する取得処理と、
前記指定部分式に基づいて、前記多項式を構成するための１又は複数の前記部分式を生成する生成処理と、
を含み、
前記部分式は、前記プログラムコードに含まれるシンボルから構成可能な式であり、
前記生成処理は、前記プログラムコードの解析によって前記指定部分式との関連性が確認された１又は複数の関連部分式を、前記多項式を構成するための１又は複数の前記部分式として生成する
不変条件生成装置。
【請求項２】
前記プログラムコードに基づく前記解析は、
前記プログラムコードに含まれる前記シンボルの次元型解析によって、複数の前記シンボルそれぞれの次元型を求めること、
前記指定部分式の次元型を求めること、
を含み、
前記関連部分式は、前記シンボルから構成可能な部分式のうち、前記指定部分式の次元型と一致する次元型を有することが確認された部分式である
請求項１記載の不変条件生成装置。
【請求項３】
前記第２処理は、指定次数を取得することを更に含み
前記関連部分式は、前記指定次数以下の次数の部分式である
請求項２記載の不変条件生成装置。
【請求項４】
前記プログラムコードに基づく前記解析は、
前記指定部分式だけを要素として有する前記部分式の初期集合Ｂを生成すること、
前記指定部分式を変数ｑの初期値とすること、
φ（ｑ）が、前記集合Ｂに含まれる１又は複数の前記部分式の線形結合として表現される式になることが確認されるまで、後述の第１更新ステップ及び第２更新ステップを含む繰り返し処理を実行すること、
を含み、
前記関連部分式は、前記繰り返し処理が終了したときに、前記集合Ｂに含まれる１又は複数の部分式であり、
前記φ（ｑ）は、変数ｑが示す式を、前記プログラムコードに従って変化させる関数であり、前記プログラムコードに基づいて求められ、
第１更新ステップは、前記集合Ｂの要素に前記φ（ｑ）を加えるステップであり、
第２更新ステップは、前記φ（ｑ）を新たなｑとするステップである
請求項１記載の不変条件生成装置。
【請求項５】
請求項１〜４のいずれか１項に記載の不変条件生成装置としてコンピュータを機能させるためのコンピュータプログラム。
【請求項６】
不変条件を生成する処理を実行する処理部によって実行される方法であって、
記憶部からプログラムコードを読み出す第１処理を実行すること、
多項式を構成するための１又は複数の部分式を生成する第２処理を実行すること、
前記不変条件を生成する第３処理を実行すること、
を含み、
前記第２処理は、
指定部分式を取得する取得処理と、
前記指定部分式に基づいて、前記多項式を構成するための１又は複数の前記部分式を生成する生成処理と、
を含み、
前記部分式は、前記プログラムコードに含まれるシンボルから構成可能な式であり、
前記生成処理は、前記プログラムコードの解析によって前記指定部分式との関連性が確認された１又は複数の関連部分式を、前記多項式を構成するための１又は複数の前記部分式として生成する
方法。
【請求項７】
プログラムコードを作成すること、
請求項６に記載の前記記憶部が、作成されたプログラムコードを記憶すること、
請求項６に記載の方法によって、前記プログラムコードの不変条件を生成すること、
前記不変条件を用いて、前記プログラムコードの形式的検証を行うこと、
前記形式的検証の結果に基づいて前記プログラムコードを修正すること、
を含むプログラムコードの製造方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、不変条件生成装置等に関するものである。
【背景技術】
【０００２】
不変条件（Invariant）は、プログラムコード（以下、単に「コード」ということがある）の形式的検証（formal verification）に用いられる。形式的検証は、プログラムコードの正当性を数学的な形式的手法で証明することである。プログラムコードに含まれるある処理に対する不変条件は、その処理の実行前後において成立する条件として構成される。ｗｈｉｌｅ文のようなループ処理に対する不変条件は、ループ不変条件（Loop Invariant）と呼ばれる。ループ不変条件は、ループの開始時点で成立するとともに、ループを何回繰り返しても成立する条件として構成される。
【０００３】
不変条件を生成する従来の方法には、非特許文献１等に記載のテンプレート法（template-based method）がある。テンプレート法では、多項式ｐが、不変条件に関係する多項式のテンプレートとして生成される。多項式ｐは、検証対象のプログラムコードに含まれるシンボルと不定係数によって構成される。シンボルとは、プログラムに含まれる変数又は定数を示す文字又は記号である。そして、ｐ＝０が不変条件であるような制約が生成される。この制約を解析することで、不変条件が得られる。
【先行技術文献】
【非特許文献】
【０００４】
【非特許文献１】Sankaranarayanan, H. Sipma, and Z. Manna. Non-linear loop invariant generation using grobner bases. In N. D. Jones and X. Leroy, editors, Proceedings of the 31st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pages 318-329. ACM, 2004.
【非特許文献２】Kennedy. Dimension types. In D. Sannella, editor, ProgrammingLanguages and Systems - ESOP’94, 5th European Symposium on Programming, Edinburgh, U.K., April 11-13, 1994, Proceedings, volume 788 of Lecture Notes in Computer Science,pages 348-362. Springer, 1994.
【非特許文献３】Cachera, T. P. Jensen, A. Jobin, and F. Kirchner. Inference of polynomial invariants for imperative programs: A farewell to grobner bases. Sci. Comput. Program., 93:89-109, 2014.
【発明の概要】
【０００５】
テンプレート法では、プログラムコードに非線形の項（例えば、変数と変数の掛け算）が含まれると、不変条件の生成処理に膨大な時間を要することが多い。プログラムコードに非線形の項が含まれている場合、テンプレートとしての多項式の次数を高くしないと不変条件を発見できないことが多い。このため、テンプレートが大規模となる。
【０００６】
例えば、テンプレートとしての多項式の次数がｎであり、プログラムコードに含まれるシンボルの数が３であると、多項式に含まれる単項式の数のオーダは、Ｏ（ｎ３）となる。テンプレートが大きくなると、テンプレートを用いて生成される制約に含まれる単項式の数も多くなる。すなわち、制約が大規模になる。この結果、制約を解析するのに時間を要し、実用的な時間内に不変条件を生成できないこともある。
【０００７】
そこで、不変条件を生成するための新たな技術が望まれる。
【０００８】
本発明の一の態様は、不変条件生成装置である。不変条件生成装置は、プログラムコードが記憶される記憶部と、前記不変条件を生成する処理を実行する処理部を備える。前記処理は、前記記憶部から前記プログラムコードを読み出す第１処理と、多項式を構成するための１又は複数の部分式を生成する第２処理と、前記不変条件を生成する第３処理と、を含む。従来のテンプレート法の問題は、第２処理においてコード解析をすることによって解決される。本発明の他の態様は、不変条件生成装置としてコンピュータを機能させるためのコンピュータプログラムである。本発明の他の態様は、不変条件を生成する処理を実行する処理部によって実行される方法である。本発明の他の態様は、プログラムコード製造方法である。
【図面の簡単な説明】
【０００９】
【図１】検証装置の構成図である。
【図２】第２処理の第１例のフローチャートである。
【図３Ａ】第２処理の第２例のフローチャートである。
【図３Ｂ】第２処理の第２例の実行例を示す図である。
【図４】第３処理のフローチャートである。
【図５Ａ】第３処理の第１実行例を示す図である。
【図５Ｂ】第３処理の第１実行例を示す図である。
【図６Ａ】第３処理の第２実行例を示す図である。
【図６Ｂ】第３処理の第２実行例を示す図である。
【図７】プログラムコード製造方法のフローチャートである。
【発明を実施するための形態】
【００１０】
［１．実施形態の概要］
（１）実施形態に係る不変条件生成装置は、プログラムコードが記憶される記憶部と、前記不変条件を生成する処理を実行する処理部を備える。プログラムコードとは、例えば、プログラムのソースコードである。前記処理は、前記記憶部から前記プログラムコードを読み出す第１処理と、多項式を構成するための１又は複数の部分式を生成する第２処理と、前記不変条件を生成する第３処理と、を含む。
【００１１】
部分式は、典型的には、多項式に含まれる単項式である。単項式は、プログラムに含まれるシンボルの冪積と冪積に掛けられる係数によって構成されていてもよいし、係数を有さず冪積だけで構成されていてもよい。プログラムに含まれるシンボルは、例えば、変数又は定数である。部分式は、多項式に含まれる部分的な多項式であってもよい。なお、単項式は、項数が１である特殊な多項式の形式であると考えることができる。
【００１２】
前記第２処理は、指定部分式を取得する取得処理と、前記指定部分式に基づいて、前記多項式を構成するための１又は複数の前記部分式を生成する生成処理と、を含む。
【００１３】
前記部分式は、前記プログラムコードに含まれるシンボルから構成可能な式である。前記生成処理は、前記プログラムコードの解析によって前記指定部分式との関連性が確認された１又は複数の関連部分式を、前記多項式を構成するための１又は複数の前記部分式として生成する。
【００１４】
（２）前記プログラムコードに基づく前記解析は、前記プログラムコードに含まれる前記シンボルの次元型解析によって、複数の前記シンボルそれぞれの次元型を求めること、前記指定部分式の次元型を求めること、を含むことができる。前記関連部分式は、前記シンボルから構成可能な部分式のうち、前記指定部分式の次元型と一致する次元型を有することが確認された部分式であるのが好ましい。
【００１５】
（３）前記第２処理は、指定次数を取得することを更に含み、前記関連部分式は、前記指定次数以下の次数の部分式であるのが好ましい。
【００１６】
（４）前記プログラムコードに基づく前記解析は、前記指定部分式だけを要素として有する前記部分式の初期集合Ｂを生成すること、前記指定部分式を変数ｑの初期値とすること、φ（ｑ）が、前記集合Ｂに含まれる１又は複数の前記部分式の線形結合として表現される式になることが確認されるまで、後述の第１更新ステップ及び第２更新ステップを含む繰り返し処理を実行すること、を含むことができる。
【００１７】
前記関連部分式は、前記繰り返し処理が終了したときに、前記集合Ｂに含まれる１又は複数の部分式である。前記φ（ｑ）は、変数ｑが示す式を、前記プログラムコードに従って変化させる関数であり、前記プログラムコードに基づいて求められる。第１更新ステップは、前記集合Ｂの要素に前記φ（ｑ）を加えるステップである。第２更新ステップは、前記φ（ｑ）を新たなｑとするステップである。
【００１８】
（５）実施形態に係るコンピュータプログラムは、（１）項〜（４）項の請求項１記載のいずれか１項に記載の不変条件生成装置としてコンピュータを機能させる。
【００１９】
（６）実施形態に係る方法は、不変条件を生成する処理を実行する処理部によって実行される。方法は、記憶部からプログラムコードを読み出す第１処理を実行すること、多項式を構成するための１又は複数の部分式を生成する第２処理を実行すること、前記不変条件を生成する第３処理を実行すること、を含む。
【００２０】
前記第２処理は、指定部分式を取得する取得処理と、前記指定部分式に基づいて、前記多項式を構成するための１又は複数の前記部分式を生成する生成処理と、を含み、前記部分式は、前記プログラムコードに含まれるシンボルから構成可能な式である。前記生成処理は、前記プログラムコードの解析によって前記指定部分式との関連性が確認された１又は複数の関連部分式を、前記多項式を構成するための１又は複数の前記部分式として生成する。
【００２１】
（７）実施形態に係るプログラムコード製造方法は、プログラムコードを作成すること、前記記憶部が、作成されたプログラムコードを記憶すること、（６）項に記載の方法によって、前記プログラムコードの不変条件を生成すること、前記不変条件を用いて、前記プログラムコードの形式的検証を行うこと、前記形式的検証の結果に基づいて前記プログラムコードを修正すること、を含む。
【００２２】
［２．実施形態の詳細］
【００２３】
［２．１  プログラムコードの例］
以下ではプログラム検証の対象となるプログラムコードの例を説明する。これらのコードは、シンボル同士の積などの非線形表現を含む。
【００２４】
［２．１．１  ＡＣＣＥＬＲＥＳＩＳＴ］
【数１】
0006622098.tif 000002
【００２５】
ＡＣＣＥＬＲＥＳＩＳＴは、質量が１であり、一定の加速度ｇを持つ質量点の挙動をモデル化したものである。ＡＣＣＥＬＲＥＳＩＳＴは、シンボルｘ，ｖ，ｔ，ε，ｇ，ρを含む。ｘは質量点の位置である。ｖは、質量点の速度である。ｔは時間である。ｘ０は初期位置である。ｖ０は、初期速度である。ｇは加速度である。ρは質量点と空気との間の摩擦係数である。εは離散間隔である。
【００２６】
ｗｈｉｌｅ（＊）｛．．．｝は、繰り返し毎に実行を終了するか否かを非決定的に選択するループである。｛．．．｝の中身は、ループ本体である。例のループ本体においては、同時代入文が記載されている。同時代入文は、複数の変数を更新するものである。例では、同時代入により、変数ｘ，ｖ，ｔの値が更新される。
【００２７】
ｘの更新式ｘ：＝ｘ＋ｖεは、以下の微分方程式に基づく。
【数２】
0006622098.tif 000003
【００２８】
ｔの更新式ｔ：＝ｔ＋εは、以下の微分方程式に基づく。
【数３】
0006622098.tif 000004
【００２９】
ｖの更新式ｖ：＝ｖ−ｇε−ρｖεは、以下の微分方程式に基づく。−ρｖは、空気によって質量点に与えられる力である。
【数４】
0006622098.tif 000005
【００３０】
［２．１．２  ＳＵＭＰＯＷＥＲｋ，ｎ］
【数５】
0006622098.tif 000006
【００３１】
ＳＵＭＰＯＷＥＲｋ，ｎは、変数ｓに、以下の式の値をセットするプログラムコードである。ｍは、ループ繰り返しの回数である。ｋ，ｎは、任意の整数である。
【数６】
0006622098.tif 000007
【００３２】
［２．２  テンプレート法による不変条件の生成］
ループ不変条件を生成する従来の方法としては、非特許文献１等に記載のテンプレート法（template-based method）がある。テンプレート法は、最初に、ループ不変表明のテンプレートを指定する。例えば、テンプレート法に基づくアルゴリズムは、ＡＣＣＥＬＲＥＳＩＳＴのループ不変表明のテンプレートとして、次の２次多項式ｐ（ｘ，ｖ，ｔ，ε，ｇ，ρ）を生成する。
【数７】
0006622098.tif 000008
【００３３】
上記の多項式ｐ（ｘ，ｖ，ｔ，ε，ｇ，ρ）は、複数の単項式を有して構成されている。単項式は、ＡＣＣＥＬＲＥＳＩＳＴに含まれるシンボルｘ，ｖ，ｔ，ε，ｇ，ρからなる冪積（power products）と、冪積に掛けられた不定係数ａ１，．．．，ａ２８と、含む。
【００３４】
次に、テンプレート法に基づくアルゴリズムは、制約（constraint）を生成する。生成される制約は、ｐ（ｘ，ｖ，ｔ，ε，ｇ，ρ）＝０がループ不変条件であるような制約である。この制約を解析することで、ａ１，．．．，ａ２８を求める。制約を解析するには、以下の条件を計算すればよい。以下の条件は、ＡＣＣＥＬＲＥＳＩＳＴのループを１回繰り返しても、ｐ（ｘ，ｖ，ｔ，ε，ｇ，ρ）の値が変わらないことを示している。
【数８】
0006622098.tif 000009
【００３５】
上記の式で示される条件を計算することで、ａ２５＝ａ２４＝ａ２３＝ａ２２＝ａ２１＝ａ２０＝ａ１９＝ａ１８＝ａ１６＝ａ１５＝ａ１４＝ａ１０＝ａ９＝ａ８＝ａ４＝ａ２と、ａ３＝ａ１７と、が得られる。
【００３６】
得られた係数を、ｐ（ｘ，ｖ，ｔ，ε，ｇ，ρ）＝０に代入することで、以下の式がループ不変条件として得られる。以下の式において、ａ１，ａ５，ａ６，ａ７，ａ１１，ａ１２，ａ１３，ａ１７，ａ２６，ａ２７，ａ２８は、任意の定数である。
【数９】
0006622098.tif 000010
【００３７】
上記のループ不変条件が示す本質的な点は、ループ本体に記載された代入が繰り返されても、ｇｔ＋ｖが定数のままである、ということである。
【００３８】
テンプレート法に基づくアルゴリズムは、ＳＵＭＰＯＷＥＲｋ，１０のループ不変表明として、以下の式を得ることができる。
【数１０】
0006622098.tif 000011
【００３９】
しかし、ＳＵＭＰＯＷＥＲｋ，１０のループ不変表明を発見するには、次数が１１である多項式をテンプレートとして生成する必要がある。一般に、３変数を持つｎ次多項式は、Ｏ（ｎ３）もの単項式を持つことになる。単項式の数の増大は、制約を大規模にする。この結果、制約を解析するのに時間を要し、実用的な時間内に不変条件を生成できないこともある。
このように、単項式の数の増大は、高次多項式テンプレートを用いたテンプレート法の適用を困難にする。
【００４０】
また、テンプレート法では、テンプレートとなる多項式を用いた制約を明示的に生成するため、処理のための記憶領域が多く必要となり、処理時間も長くなり易い。
【００４１】
しかも、不変条件としては、ｐの値がコードの１回の実行でλ倍になる不変条件（以下、「λ−不変条件」という）が望ましいことがある。しかし、既存のテンプレート法では、コードを実行してもｐの値が変わらない不変条件しか生成できない。
【００４２】
例えば、ＡＣＣＥＬＲＥＳＩＳＴのための他の有用なループ不変条件として、以下の式がある。ｍは、ループ繰り返しの回数であり、ｔ／εに等しい。
【数１１】
0006622098.tif 000012
【００４３】
この不変条件は、ＡＣＣＥＬＲＥＳＩＳＴのループの１回の繰り返しで、（ｖ−ｇ／ρ）が、（１−ρε）倍になることを示している。すなわち、λ＝（１−ρε）である。したがって、この不変条件は、「（１−ρε）−不変条件」である。また、［数９］に示す不変条件は、ループの１回の繰り返しでｐが変わらない、つまり、ｐが１倍（λ=１）になる不変条件であるから、「１−不変条件」である。
【００４４】
［２．３  実施形態に係る不変条件の生成処理］
【００４５】
［２．３．１  検証装置］
図１は、プログラムコードの形式的検証のための検証装置１００を示している。検証装置１００は、処理部２００と、記憶部３００と、を備えたコンピュータを有して構成されている。処理部２００は、例えば、ＣＰＵを有して構成されている。記憶部３００は、処理部２００によって読み取られる情報が格納されている。記憶部３００に格納された情報は、検証用プログラム３１０を含む。記憶部３００に格納された情報は、検証対象のプログラムコード３３０も含む。
【００４６】
検証用プログラム３１０は、コンピュータを、検証装置１００として機能させるためのコンピュータプログラムである。処理部２００は、検証用プログラム３１０を実行することで、検証対象のプログラムコード３３０に対する形式的検証のための処理を行う。検証用プログラム３１０は、不変条件生成モジュール３２０を有している。不変条件生成モジュール３２０は、検証対象のプログラムコード３３０の形式的検証に用いる不変条件を生成する処理を実行する。したがって、検証装置１００は、不変条件生成装置としても機能する。検証用プログラム３１０は、生成した不変条件を用いて、検証対象のプログラムコード３３０の形式的検証を行う。
【００４７】
検証対象のプログラムコード３３０は、例えば、前述のＡＣＣＥＬＲＥＳＩＳＴ又はＳＵＭＰＯＷＥＲｋ，ｎである。以下の説明では、必要に応じて、前述のＡＣＣＥＬＲＥＳＩＳＴ又はＳＵＭＰＯＷＥＲｋ，ｎ以外のプログラムコードも説明に用いる。
【００４８】
［２．３．２  処理概要］
不変条件の生成処理３２０は、第１処理３２１と、第２処理３２２と、第３処理３２３と、を含む。第１処理３２１は、記憶部３００から検証対象のプログラムコード３３０を読み出す処理である。処理部２００は、読み出したコード３３０を用いて、不変条件を生成する。以下では、読み出したコード３３０に含まれるループ文（ｗｈｉｌｅ文）のための不変条件であるループ不変条件の生成について説明する。
【００４９】
第２処理３２２は、多項式を構成する部分式を生成する処理である。第２処理３２２は、従来のテンプレート法でいうと、テンプレートとなる多項式を構成する単項式又は単項式に含まれる冪積（power products）を生成する処理に対応する。従来のテンプレート法では、前述のように単項式の数が増大し易いが、実施形態に係る第２処理３２２では、多項式を構成する単項式（冪積）の数を削減することができる。
【００５０】
第３処理３２３は、生成した部分式に基づき、読み出したコード３３０に対する不変条件を生成する処理である。第３処理３２３は、従来のテンプレート法でいうと、テンプレートである多項式ｐ＝０がループ不変条件であるような制約を解いて、ループ不変条件を生成する処理に対応する。従来のテンプレート法では、λ=１である「１−不変条件」しか生成できなかったが、実施形態に係る第３処理３２３では、λ＝１以外のλ−不変条件を生成することができる。また、実施形態に係る第３処理３２３では、生成された部分式を用いるものの、テンプレートを明示的に生成する必要がないので、第３処理３２３の際に必要とする記憶容量が比較的少なくて済む。
【００５１】
［２．３．３  コード解析による部分式生成（第２処理）の第１例］
第２処理３２２は、指定部分式ｗが与えられると、指定部分式ｗに関連する複数の関連部分式を生成する処理である。図２は、第２処理３２２の第１例を示している。第２処理３２２の第１例は、ステップＳ１１からステップＳ１４までの処理を含む。図２には、ＡＣＣＥＬＲＥＳＩＳＴを例とした場合の、各ステップの処理結果を示している。
【００５２】
ステップＳ１１は、入力受付処理である。入力受付処理では、指定部分式ｗ及び指定次数ｎの入力をユーザから受け付ける。
【００５３】
指定部分式ｗは、関連部分式を発見するためのものである。指定部分式ｗは、読み出したコード３３０に含まれる１又は複数のシンボルからなる式である。指定部分式ｗは、典型的には、単項式（冪積）であるが、２以上の単項式を含む多項式であってもよい。指定部分式ｗの次数は、指定次数ｎ以下であるのが好ましい。コード３３０がＡＣＣＥＬＲＥＳＩＳＴである場合、例えば、単項式ｖが、指定部分式ｗとして入力される。
【００５４】
指定次数ｎは、関連部分式として生成される式の次数の制限である。指定次数ｎ以下の次数の式が、後述の関連部分式として生成される。ＡＣＣＥＬＲＥＳＩＳＴの場合、例えば、２が指定次数ｎとして入力される。
【００５５】
指定部分式ｗ及び／又は指定次数ｎの取得は、ユーザ入力による取得に代えて、装置１００自らが生成した指定部分式ｗ及び／又は指定次数ｎの取得であってもよい。例えば、装置１００は、コード３３０に含まれる１又は複数のシンボルを用いて、指定次数ｎ以下の次数となるシンボルの組み合わせをランダムに決定して、指定部分式ｗを得ても良い。また、装置１００は、指定次数ｎをランダムに決定してもよい。さらに、装置１００は、指定次数ｎを１から開始して部分式生成が成功しなければ、指定次数ｎを＋１としてもよい。
【００５６】
ステップＳ１２は、コード３３０に基づく解析によって、コード３３０に含まれるシンボルの次元型を求める処理（型環境Γの取得処理）である。第２処理３２２の第１例では、テンプレートを構成し得る部分式（単項式）の数を削減するため、「量の次元（quantity dimension）」という概念を利用する。量の次元は、物理学での概念であり、長さ、時間、速度などの物理量の型である。量の次元は、「物理次元」とも呼ばれる。量の次元は、物理量の基本型である基礎次元の積として表される。例えば、基礎次元としてＬとＴを考える。Ｌは、長さを示す基礎次元であり、Ｔは時間を示す基礎次元である。次元の積は、物理量がどのように計算して得られるかを示す。例えば、速度は、次元型ＬＴ−１を有する。速度は、距離を時間で割って得られるからである。加速度は、次元型ＬＴ−２を有する。加速度は、速度を時間で割って得られるからである。
【００５７】
ここで、ＡＣＣＥＬＲＥＳＩＳＴに含まれるシンボルは、ｘ，ｖ，ｔ，ε，ｇ，ρである。ＡＣＣＥＬＲＥＳＩＳＴのループ本体中のコマンド（代入文）である（ｘ、ｖ、ｔ）：＝（ｘ＋ｖε，ｖ−ｇε−ρｖε，ｔ＋ε）を解析すると、ＡＣＣＥＬＲＥＳＩＳＴにおいて、ｘの次元型はＬであり、ｖの次元型はＬＴ−１であり、ｔの次元型はＴであり、εの次元型はＴであり、ｇの次元型はＬＴ−２であり、ρの次元型はＴ−１であることが求まる。コード３３０に含まれるシンボルｘ，ｖ，ｔ，ε，ｇ，ρの次元型を示す情報を型環境Γという。
【００５８】
なお、コマンド中のｘ＋ｖεの次元型はＬであり、ｖ−ｇε−ρｖεの次元型はＬＴ−１であり、ｔ＋εの次元型はＴである。
【００５９】
物理学上の原則に基づくと、異なる次元型の量同士を加算することはできない。例えば、時間を長さに加算することはできないし、速度を長さに加算することもできない。この原則に基づくと、数７に示すテンプレート多項式ｐ（ｘ，ｖ，ｔ，ε，ｇ，ρ）は、物理的に無意味な量を表していることがわかる。すなわち、テンプレート多項式ｐ（ｘ，ｖ，ｔ，ε，ｇ，ρ）は、例えば、次元型がＴとなる単項式（ａ２ｔ，ａ５ε）と、次元型がＬＴ−１となる単項式（ａ３ｖ，ａ１７ｔｇ，ａ２６εｇ，ａ２５ｘρ）と、の和となっており、異なる次元型の量同士を加算している。したがって、次元型を考慮すれば、異なる次元型の量同士を加算するようなテンプレートが構築されるのを防止して、テンプレートのサイズを小さくすることができる。
【００６０】
コード３３０に含まれるシンボルの次元型の推論（型環境Γの取得）は、型推論アルゴリズムを用いた次元型解析によって行われる。型推論アルゴリズムは、コード３３０を解析して、コード３３０に含まれるシンボルの次元型を推論する。型推論アルゴリズムとしては、非特許文献２にて提案された次元型システム（dimension type system）を用いることができる。次元型システムは、関数型プログラミング言語のために提案され、現在では、プログラミング言語Ｆ＃に実装されている。
【００６１】
ステップＳ１３は、型環境Γに基づいて、指定部分式ｗの次元型を求める処理である。指定部分式ｗがｖである場合、指定部分式ｗの次元型は、ＬＴ−１となる。なお、指定部分式ｗが、例えば、ｖｔであれば、ｖ及びｔそれぞれの次元型ＬＴ−１，Ｔに基づいて、ｖｔの次元型は、Ｌとなる。
【００６２】
ステップＳ１４は、複数の関連部分式を生成する処理である。関連部分式とは、指定部分式ｗとの関連性が確認された部分式をいう。関連部分式は、テンプレートとなる多項式を構成することができる。テンプレートは、例えば、複数の関連部分式の線形結合として表される。関連部分式ｗは、典型的には、単項式（冪積）であるが、２以上の単項式を含む多項式であってもよい。
【００６３】
第１例では、指定部分式ｗとの関連性の確認を、指定部分式ｗの次元型を用いて行う。より具体的には、第１例で生成される関連部分式は、指定部分式ｗの次元型（ＬＴ−１）と一致する次元型を有することが確認された部分式である。関連部分式は、コード３３０に含まれるシンボルｘ，ｖ，ｔ，ε，ｇ，ρから構成可能な部分式（冪積）の中から、指定部分式ｗの次元型（ＬＴ−１）と一致する次元型を有する部分式（冪積）を選択することで得られる。関連部分式として生成される部分式の次数は、指定次数ｎ以下である。
【００６４】
シンボルｘ，ｖ，ｔ，ε，ｇ，ρから構成可能な部分式（冪積）であって、指定次数ｎ以下の部分式の集合は、｛ｔ，ｖ，ｘ，ε，ｇ，ρ，ｔ２，ｖ２，ｘ２，ε２，ｇ２，ρ２，ｔｖ，ｔｘ，ｔε，ｔｇ，ｔρ，ｖｘ，ｖε，ｖｇ，ｖρ，ｘε，ｘｇ，ｘρ、εｇ，ερ，ｇρ｝である。この集合の要素数は、指定次数ｎが大きくなると多くなる。したがって、指定次数ｎを大きくすると、多くの関連部分式を生成し易くなる。この集合の要素のうち、次元型がＬＴ−１となるのは、｛ｖ，ρｘ，ｇｔ，εｇ｝である。したがって、ステップ１４では、複数の関連部分式として、｛ｖ，ρｘ，ｇｔ，εｇ｝を生成する。関連部分式は、指定部分式を含んでも良い。
【００６５】
複数の関連部分式｛ｖ，ρｘ，ｇｔ，εｇ｝からテンプレート多項式を構成すると、テンプレート多項式は、ａ１ｖ＋ａ２ρｘ＋ａ３ｇｔ＋ａ４εｇとなる。ここで、ａ１，ａ２，ａ３，ａ４は、不定係数である。このテンプレート多項式は、［数７］に示すテンプレート多項式に比べて、単項式の数が少なく、不定係数の数も少ない。したがって、不変条件を求めるのが容易となる。
【００６６】
従来のテンプレート法に従うと、コード３３０に含まれる複数のシンボルが取り得る全ての組み合わせからなる多数の部分式（冪積）によって、テンプレート多項式が構成される（数７参照）。つまり、従来のテンプレート法では、テンプレート多項式の構成の際に、コード３３０における複数のシンボル間の関係を考慮することなく、コード３３０に含まれるシンボルから得られる冪積の単なる全列挙によって、テンプレート多項式が構成されている。このため、テンプレート多項式は、コード３３０における複数のシンボル間の関係に照らして、不適切な単項式まで含むことになり、規模が大きくなり易い。従来のテンプレート法では、不適切な単項式を含むテンプレート多項式を生成し、制約を解くことで、不適切な単項式（係数ａが０となる単項式）を見つけていた。この結果、大規模な制約を解く必要があり、演算時間が長くなり易かった。
【００６７】
これに対して、実施形態に係る第２処理３２２では、コード３３０の解析によって、指定部分式との関連が確認された関連部分式（関連単項式）を生成するため、不適切な単項式（指定部分式との関連性がない部分式）を排除することができる。
【００６８】
なお、本実施形態の第３処理３２３では、テンプレート多項式を明示的に作成する必要がない固有ベクトル法を用いる。したがって、生成された関連部分式｛ｖ，ρｘ，ｇｔ，εｇ｝は、テンプレート多項式に変換されることなく、生成された関連部分式｛ｖ，ρｘ，ｇｔ，εｇ｝自体が、第３処理３２３に与えられる。ただし、第３処理３２３では、テンプレート多項式を明示的に作成して、制約を解くことで不変条件を生成してもよい。
【００６９】
実施形態において、どのような手法で第３処理３２３を行うにしろ、第２処理３２２で生成された関連部分式の数が少ないため、第３処理３２３の処理負荷が軽減される。
【００７０】
なお、第２処理３２２において、指定次数ｎ以下では、指定部分式ｗ以外の関連部分式を発見できなかった場合、処理部２００が、自動的に、指定次数ｎを増加（例えば、＋１）させて、ステップＳ１４を再度実行してもよい。指定次数ｎを大きくすると、シンボルｘ，ｖ，ｔ，ε，ｇ，ρから構成可能な部分式（冪積）の数が増加するため、指定部分式ｗの次元型と一致する部分式が存在する可能性が高まる。なお、指定次数ｎの変更は、増加以外の変更であってもよく、例えば、指定次数ｎのランダムな変更であってもよい。
【００７１】
また、第２処理３２２において、指定部分式ｗ以外の関連部分式を発見できなかった場合、処理部２００が、自動的に、指定部分式を他の部分式に変更して、ステップＳ１３及びステップＳ１４を再度実行してもよい。
【００７２】
ここで、「量の次元」の概念に基づく部分式の数の削減は、ＡＣＣＥＬＲＥＳＩＳＴのように物理現象をモデル化したプログラムコードだけでなく、物理現象をモデル化していないプログラムコード、例えば、ＳＵＭＰＯＷＥＲｋ，ｎにも適用できる。例えば、ＳＵＭＰＯＷＥＲｋ，１０は、意味のある物理現象に対応していない。しかし、実施形態に係る第２処理３２２では、ＳＵＭＰＯＷＥＲｋ，１０に関し、指定部分式ｗとしてｋｓが与えられ、指定次数ｎとして１１が与えられると、関連部分式の集合として｛ｘ１１，ｘ１０ｋ，ｘ９ｋ２，ｘ７ｋ４，ｘ５ｋ６，ｘ３ｋ８，ｘｋ１０，ｋｓ｝を生成することができる。
【００７３】
なお、型環境Γとして、ｓは次元型Ｔ１０の量であり、ｋは次元型Ｔの量であり、ｘは次元型Ｔの量であることが求まる。ここで、Ｔは、基礎次元であるが、物理的な意味のある次元ではなく、仮想的な次元である。このように、次元型の概念は、非物理現象をモデル化したプログラムコードにも適用可能である。したがって、図２に示す第２処理３２２は、プログラムコードが何をモデル化しているかにかかわらず適用できる。
【００７４】
［２．３．４  コード解析による部分式生成（第２処理）の第２例］
第２処理３２２の第１例では、次元型の一致を、部分式の関連性の確認に用いていたが、第２処理３２２の第２例では、図３Ａに示すアルゴリズムによって、部分式の関連性の確認を行う。第２例においても、第１例と同様に、部分式の関連性の確認のために、コード３３０の解析を行う。
【００７５】
第２処理３２２の第２例は、ステップ２１からステップ２４までの処理を含む。図３Ｂは、ｗｈｉｌｅ（＊）｛（ｓ，ｃ）：＝（ｓ＋ｃε、ｃ−ｓε）｝のプログラムコードを例とした場合の、各ステップの処理結果を示している。
【００７６】
ステップＳ２１は、入力受付処理である。入力受付処理では、ステップＳ１１と同様に、指定部分式ｗの入力をユーザから受け付ける。ただし、ステップＳ２１では、指定次数を受け付ける必要はない。ここでは、例として、単項式ｓ２が、指定部分式ｗとして入力される。なお、指定部分式の取得は、装置１００が生成した指定部分式の取得であってもよい。
【００７７】
ステップＳ２２は、関数φ（ｑ）を取得する処理である。図３Ａに示すアルゴリズムでは、部分式の関連性の確認のために関数φ（ｑ）を用いる。ここで、ｑは、多項式を示す変数である。φは、ｑが示す式を、プログラムコードに従って変化させる関数である。ｑが示す多項式は、プログラムコードの実行によって値が更新されるシンボル（変数）ｓを含んでいる。したがって、ｑが示す多項式の値は、プログラムコードであるループ文（ｗｈｉｌｅ文）１回の実行によって変化する。φは、プログラムコードであるループ文（ｗｈｉｌｅ文）１回の実行により変化した値を示す多項式を生成する。例えば、ｗｈｉｌｅ（＊）｛（ｓ，ｃ）：＝（ｓ＋ｃε、ｃ−ｓε）｝の場合、ｗｈｉｌｅ文１回の実行によって、ｓ：＝ｓ＋ｃεの代入及びｃ：＝ｃ−ｓεの代入が生じ、多項式ｑ＝ｓ２の値は、（ｓ＋ｃε）２＝ｓ２＋２εｓｃ＋ε２ｃ２に変化する。したがって、φ（ｓ２）は、ｓ２＋２εｓｃ＋ε２ｃ２を生成する。
【００７８】
ステップＳ２２では、プログラムコードｗｈｉｌｅ（＊）｛（ｓ，ｃ）：＝（ｓ＋ｃε、ｃ−ｓε）｝を解析し、関数φ（ｑ）を作成するための情報として、ｓ：＝ｓ＋ｃε及びｃ：＝ｃ−ｓεを取得する。関数φ（ｑ）を作成するための情報は、一般に、プログラムコード中において、シンボル（変数）の値を更新するコマンド（例えば、代入文）が相当する。ここでは、取得した情報ｓ：＝ｓ＋ｃε及びｃ：＝ｃ−ｓεに基づき、関数φ（ｑ）は、ｑに含まれるｓをｓ＋ｃεに写像し、ｑに含まれるｃをｃ−ｓεに写像する関数として生成される。
【００７９】
ステップＳ２３では、図３ＡのステップＳ２３のボックス中に示すステップ１からステップ６の処理が実行される。図３Ｂに示すように、ステップ１では、指定部分式ｗ＝ｓ２だけを要素として有する初期集合Ｂが生成される。集合Ｂは、部分式を要素として持つ集合である。ステップ２では、指定部分式ｓ２が変数ｑの初期値として設定される。
【００８０】
ステップ３は、ｗｈｉｌｅループの繰り返し条件判定である。ステップ４，５は、ｗｈｉｌｅループ本体であり、ステップ６は、ｗｈｉｌｅループの終わりを示す。ｗｈｉｌｅループの繰り返し条件判定に含まれる＜Ｂ＞は、集合Ｂに含まれる部分式の線形結合となる式の集合を示す。ｗｈｉｌｅループの繰り返し条件判定は、ステップ３に示すように、φ（ｑ）が、集合Ｂに含まれる部分式の線形結合となる式の集合に含まれていないことである。φ（ｑ）が、集合Ｂに含まれる部分式の線形結合となる式の集合に含まれていれば、ｗｈｉｌｅループは終了する。
【００８１】
φ（ｑ）が、集合Ｂに含まれる部分式の線形結合となる式の集合に含まれているか否かの判定は、例えば、φ（ｑ）を、集合Ｂに含まれる部分式の線形結合となる式で表現するための線形結合係数が存在するか否かの判定によって行われる。例えば、ｗｈｉｌｅループ１回目の繰り返し条件判定（ステップ３）において、φ（ｑ）＝ｓ２＋２εｓｃ＋ε２ｃ２であり、Ｂ＝｛ｓ２｝である。したがって、図３Ｂに示すように、ｓ２＋２εｓｃ＋ε２ｃ２＝ａｓ２を満たす係数ａが存在するか否かが判定される。そのような係数ａは、存在しないから、ｗｈｉｌｅループの繰り返し条件を満たす。したがって、繰り返しは終了せず、ｗｈｉｌｅループ本体であるステップ４，５が実行される。
【００８２】
ステップ４は、集合Ｂの更新ステップ（第１更新ステップ）である。図３Ｂに示すように、ステップ４では、集合Ｂの要素にφ（ｑ）が加えられる。ｗｈｉｌｅループ１回目のステップ４において、Ｂ＝｛ｓ２，ｓ２＋２εｓｃ＋ε２ｃ２｝となる。
【００８３】
ステップ５は、変数ｑの更新ステップ（第２更新ステップ）である。ステップ５では、φ（ｑ）が新たなｑとなる。ｗｈｉｌｅループ１回目のステップ５において、ｑ＝ｓ２＋２εｓｃ＋ε２ｃ２となる。
【００８４】
ｗｈｉｌｅループ２回目の繰り返し条件判定（ステップ３）において、φ（ｑ）＝（１−２ε２＋ε４）ｓ２＋（４ε−４ε３）ｓｃ＋４ε２ｃ２であり、Ｂ＝｛ｓ２，ｓ２＋２εｓｃ＋ε２ｃ２｝である。したがって、（１−２ε２＋ε４）ｓ２＋（４ε―４ε３）ｓｃ＋４ε２ｃ２＝ａｓ２＋ｂ（ｓ２＋２εｓｃ＋ε２ｃ２）を満たす係数ａ，ｂが存在するか否かが判定される。そのような係数ａ，ｂは、存在しないから、ｗｈｉｌｅループの繰り返し条件を満たす。
【００８５】
ｗｈｉｌｅループ２回目のステップ４において、Ｂ＝｛ｓ２，ｓ２＋２εｓｃ＋ε２ｃ２，（１−２ε２＋ε４）ｓ２＋（４ε―４ε３）ｓｃ＋４ε２ｃ２｝となる。
【００８６】
ｗｈｉｌｅループ２回目のステップ５において、ｑ＝（１−２ε２＋ε４）ｓ２＋（４ε−４ε３）ｓｃ＋ε２ｃ２となる。
【００８７】
ｗｈｉｌｅループ３回目の繰り返し条件判定（ステップ３）において、φ（ｑ）は、（１−６ε２＋９ε４）ｓ２＋（６ε−２０ε３＋６ε５）ｓｃ＋（９ε２−６ε４＋ε６）ｃ２であり、Ｂ＝｛ｓ２，ｓ２＋２εｓｃ＋ε２ｃ２，（１−２ε２＋ε４）ｓ２＋（４ε―４ε３）ｓｃ＋４ε２ｃ２｝である。したがって、（１−６ε２＋９ε４）ｓ２＋（６ε−２０ε３＋６ε５）ｓｃ＋（９ε２−６ε４＋ε６）ｃ２＝ａｓ２＋ｂ（ｓ２＋２εｓｃ＋ε２ｃ２）＋ｄ｛（１−２ε２＋ε４）ｓ２＋（４ε―４ε３）ｓｃ＋４ε２ｃ２｝を満たす係数ａ，ｂ，ｄが存在するか否かが判定される。
【００８８】
ａ＝１＋３ε２＋３ε４＋ε６，ｂ＝−３−２ε２＋ε４，ｄ＝３−ε２とした場合、上記の式を満たす。つまり、φ（ｑ）が、集合Ｂに含まれる１又は複数の部分式の線形結合として表現される式になることが確認されたことになる。したがって、ｗｈｉｌｅループの繰り返し条件は満たされなくなり、ｗｈｉｌｅループは終了する。
【００８９】
ステップＳ２４では、ｗｈｉｌｅループを終了した時点での集合Ｂ＝｛ｓ２，ｓ２＋２εｓｃ＋ε２ｃ２，（１−２ε２＋ε４）ｓ２＋（４ε―４ε３）ｓｃ＋４ε２ｃ２｝が、指定部分式ｗに関連することが確認された関連部分式の集合として出力される。
【００９０】
第２処理３２２の第２例においても、コード３３０の解析によって、指定部分式ｗとの関連が確認された関連部分式（関連多項式）を生成するため、不適切な部分式（指定部分式との関連性がない部分式）を排除することができる。
【００９１】
なお、第２処理３２２の第２例において、ステップＳ２３中のｗｈｉｌｅループが所定時間内に終了しない場合、すなわち、関連部分式を発見できなかったものとみなして、ｗｈｉｌｅループを強制終了する。この場合、指定部分式を他の部分式に変更して、ステップＳ２２からステップＳ２４を再度実行すればよい。
【００９２】
［２．３．５  固有ベクトル法による不変条件生成（第３処理）］
第３処理３２３は、第２処理３２２で生成された関連部分式から、不変条件を生成する処理である。なお、第３処理３２３において不変条件を生成するのに用いられる部分式は、第２処理３２２で生成された関連部分式に限られず、従来のテンプレート法において生成されるテンプレート多項式を構成する複数の単項式（冪積）であってもよい。
【００９３】
さて、プログラムコードが実行されることによる複数の関連部分式それぞれの変換を表す変換行列ＭＴを考えた場合、その変換行列ＭＴの転置である表現行列（representation matrix）Ｍは、固有値と固有ベクトルとを持つ。なお、Ｔは、転置を示す。本発明者らは、表現行列Ｍの固有値と固有ベクトルとが不変条件を与えることを見出した。したがって、不変条件の生成は、表現行列の固有値と固有ベクトルを求めるという簡易な処理によって行うことができる。なお、表現行列の固有値と固有ベクトルを求めることで、不変条件を生成することを、「固有ベクトル法」というものとする。
【００９４】
図４は、固有ベクトル法による不変条件生成（第３処理３２３）を示している。第３処理３２３は、ステップ３１からステップＳ３３までの処理を含む。図５Ａ，５Ｂは、ＡＣＣＥＬＲＥＳＩＳＴを例とした場合の処理結果を示している。図５Ａ，５Ｂでは、複数の関連部分式として、第２処理３２２の第１例に示すように、｛ｖ，ρｘ，ｇｔ，εｇ｝が生成されているものとする。
【００９５】
ステップＳ３１は、表現行列Ｍと、余りベクトルｑと、を生成する処理（行列生成処理；余りベクトル生成処理）である。
【００９６】
表現行列Ｍは、プログラムコードが実行されることによる複数の関連部分式それぞれの変換を表す変換行列ＭＴの転置行列として生成される。余り行列ｑは、複数の関連部分式それぞれの変換が、変換行列ＭＴだけでは表現できない場合に生成される。余り行列ｑは、図５Ａ，５Ｂの例では生成されないが、図６Ａ，６Ｂの例では生成される。
【００９７】
ＡＣＣＥＬＲＥＳＩＳＴの場合、ステップＳ３１では、まず、図５Ａに示す変換行列ＭＴが生成される。変換行列ＭＴは、ＡＣＣＥＬＲＥＳＩＳＴのｗｈｉｌｅループ１回の実行による、複数の関連部分式それぞれの変換を表す行列として生成される。関連部分式が｛ｖ，ρｘ，ｇｔ，εｇ｝である場合、（ｘ，ｖ，ｔ）＝（ｘ＋ｖε，ｖ−ｇε−ρｖε）の実行により、関連部分式ｇｔはｇ（ｔ＋ε）に変換され、関連部分式ｇεはｇεに変換され、ｖはｖ−ｇε−ρｖεに変換され、ρｘはρ（ｘ＋ｖε）に変換される。これらの変換関係より、図５Ａに示す変換行列ＭＴが得られる。関連部分式の変換は、変換行列ＭＴだけで表現することができるので、前述のように余りベクトルｑは生成されない。
【００９８】
図５Ａに示す変換行列ＭＴの転置により、図５Ａに示す表現行列Ｍが生成される。
【００９９】
ステップＳ３２は、表現行列Ｍの固有値と固有ベクトルとを求める処理（演算処理）である。表現行列Ｍの固有値と固有ベクトルとは既知の手法によって算出される。図５Ａに示す表現行列Ｍは、２つの固有値を持つ。一つ目の固有値は１である。二つ目の固有値は（１−ρε）である。図５Ａに示すように、固有値１に対応する固有ベクトルは（−１，０，１，１）Ｔ及び（０，１，０，０）Ｔであり、固有値（１−ρε）に対応する固有ベクトルは（０，−１／ερ，１，０）Ｔである。
【０１００】
ステップＳ３３は、固有値λとその固有値λに対応する固有ベクトルとの組み合わせから、λ−不変条件を生成する処理（不変条件生成処理）である。λ−不変条件は、前述のように、ループの１回の繰り返しで値がλ倍になる不変条件である。固有値と固有ベクトルとの組が、一つの不変条件に対応する。したがって、固有値と固有ベクトルとの組が複数ある場合には、組ごとに不変条件を生成する処理が行われる。
【０１０１】
固有値１に対応する固有ベクトル（−１，０，１，１）Ｔ及び（０，１，０，０）は、１−不変条件として、ａ（−ｇｔ＋ｖ＋ρｘ）＋ｂ（ｇε）を与える。複数の関連部分式｛ｇｔ，ｇε，ｖ，ρｘ｝をベクトル（ｇｔ，ｇε，ｖ，ρｘ）Ｔとして扱うと、固有ベクトルとベクトル（ｇｔ，ｇε，ｖ，ρｘ）Ｔとの内積が、１−不変条件となる。１−不変条件は、前述のように、ループの１回の繰り返しで値が変化しない不変条件である
【０１０２】
ここで、一つの固有値に対して、複数の独立な固有ベクトルが存在する場合には、複数の独立な固有ベクトルの線形結合を不変条件の生成に用いればよい。例えば、固有値”１”に対応する固有ベクトルが（−１，０，１，１）Ｔ及び（０，１，０，０）Ｔである場合、それらの線形結合は、（−ａ，ｂ，ａ，ｂ）Ｔである。ここで、ａ，ｂは、任意の係数である。固有ベクトルの線形結合（−ａ，ｂ，ａ，ｂ）Ｔとベクトル（ｇｔ，ｇε，ｖ，ρｘ）Ｔとの内積は、ａ（−ｇｔ＋ｖ＋ρε）＋ｂ（ｇε）である。したがって、ステップＳ３３では、ａ（−ｇｔ＋ｖ＋ρε）＋ｂ（ｇε）が、ＡＣＣＥＬＲＥＳＩＳＴの１−不変条件として生成される。
【０１０３】
固有値（１−ρε）に対応する固有ベクトルは（０，−１／ερ，１，０）Ｔは、（１−ρε）−不変条件として、ｃ（−ｇ／ρ＋ｖ）を与える。固有ベクトル（０，−１／ερ，１，０）Ｔと、ベクトル（ｇｔ，ｇε，ｖ，ρｘ）Ｔと、の内積は、ｃ（−ｇ／ρ＋ｖ）である。ここで、ｃは、任意の係数である。したがって、ステップＳ３３では、ｃ（−ｇ／ρ＋ｖ）が、ＡＣＣＥＬＲＥＳＩＳＴの（１−ρε）−不変条件として生成される。
【０１０４】
図６Ａ，６Ｂは、別のプログラムコードｗｈｉｌｅ（＊）｛（ｘ，ｙ，ｚ）：＝（ｘ２，ｙ＋ｘ２，ｚ−ｘ２）｝についての第３処理３２３の処理例を示している。ここでは、複数の関連部分式として｛ｚ，ｙ，ｘ２｝が生成されているものとする。
【０１０５】
ステップＳ３１では、まず、図６Ａに示す変換行列ＭＴが生成される。変換行列ＭＴは、プログラムコードｗｈｉｌｅ（＊）｛（ｘ，ｙ，ｚ）：＝（ｘ２，ｙ＋ｘ２，ｚ−ｘ２）｝のｗｈｉｌｅループ１回の実行による、複数の関連部分式それぞれの変換を表す行列として生成される。関連部分式が｛ｚ，ｙ，ｘ２｝である場合、（ｘ，ｙ，ｚ）：＝（ｘ２，ｙ＋ｘ２，ｚ−ｘ２）の実行により、関連部分式ｘはｚ−ｘ２に変換され、関連部分式ｙはｙ＋ｘ２に変換され、ｘ２はｘ４に変換される。これらの変換関係より、図６Ａに示す変換行列ＭＴ及び余りベクトルｑが生成される。ここでは、関連部分式の変換は、変換行列ＭＴだけは表現することができないので、関連部分式の変換を完全に表現するための余りベクトルｑが生成される。
【０１０６】
図６Ａに示す変換行列ＭＴの転置により、図６Ａに示す表現行列Ｍが生成される。
【０１０７】
ステップＳ３２では、図６Ａに示す表現行列Ｍの固有値として１が求められ、固有値１に対応する２つの固有ベクトル（１，１，０）Ｔ及び（−１，０，１）Ｔが求められる。
【０１０８】
ステップＳ３３では、まず、固有値１に対応する２つの固有ベクトル（１，１，０）Ｔ及び（−１，０，１）Ｔの線形結合が求められる。２つの固有ベクトルの線形結合は、図６Ｂに示すように、（Ｃ１−Ｃ２，Ｃ１，Ｃ２）Ｔである。ここで、Ｃ１，Ｃ２は、任意の係数である。
【０１０９】
本発明者らは、余りベクトルｑが存在する場合であっても、固有ベクトル（複数の固有ベクトルの線形結合を含む）と余りベクトルｑとの内積が０になる条件が満たされれば、固有値λと固有ベクトル（複数の固有ベクトルの線形結合を含む）とが、λ−不変条件を与えることを見出した。
【０１１０】
そこで、余りベクトルｑが生成されている場合には、ステップ３３では、固有ベクトル（複数の固有ベクトルの線形結合を含む）と余りベクトルｑとの内積が０になる条件を求める。複数の固有ベクトルの線形結合（Ｃ１−Ｃ２，Ｃ１，Ｃ２）Ｔと余りベクトル（０，０，ｘ４）との内積は、図６Ｂに示すように、Ｃ２ｘ４である。Ｃ２ｘ４＝０となる条件は、Ｃ２＝０である。Ｃ２＝０という条件を満たす固有ベクトルの線形結合は、図６Ｂに示すように、（Ｃ１，Ｃ１，０）Ｔである。Ｃ２＝０という条件を満たす固有ベクトルの線形結合（Ｃ１，Ｃ１，０）Ｔと関連部分式ベクトル（ｚ，ｙ，ｘ２）Ｔとの内積は、Ｃ１（ｚ＋ｙ）である。したがって、ステップＳ３３では、Ｃ１（ｚ＋ｙ）が、プログラムコードｗｈｉｌｅ（＊）｛（ｘ，ｙ，ｚ）：＝（ｘ２，ｙ＋ｘ２，ｚ−ｘ２）｝の１−不変条件として生成される。
【０１１１】
以上のように、実施形態の第３処理３２３では、固有ベクトルを求めるなどの簡単な処理で、不変条件を生成することができる。
【０１１２】
［２．４  実験結果］
以下の表１は、さまざまなプログラムコードの不変条件を生成した実験結果を示している。表１，２は、実施形態の不変条件生成モジュール３２０によって、不変条件を生成した結果を示している。なお、第２処理３２２として、図２に示す第１例を用い、第３処理３２３としては、固有ベクトル法を用いた。
【表１】
0006622098.tif 000013
【表２】
0006622098.tif 000014
【０１１３】
表１，２において、「名称」は、検証対象のプログラムコードの名称を示す。表１において「プログラム」は、検証対象のプログラムコードのループ本体（ｗｈｉｌｅ（＊）｛｝の中身）を示している。
【０１１４】
表１，２において、「ｗ」は、指定部分式を示し、ｎは指定次数を示している。表１において、「λ」は、実施形態に係る処理によって生成された固有値を示し、「Generated invariants」は、実施形態に係る処理によって生成されたλ−不変条件を示している。
【０１１５】
表２において、「単項式の数の比」は、単項式の数に関し、実施例における数と比較例における数との比を示している。実施例における数は、実施形態の第２処理３２２の第１例によって関連部分式として生成された単項式の数であり、比較例における数は、従来のテンプレート法によって生成されたテンプレート多項式に含まれる単項式（冪積）の数である。表２において、「演算時間（実施例）」は、実施形態において不変条件生成に要した演算時間であり、「演算時間（比較例）」は、比較例において不変条件生成に要した演算時間であり、単位はいずれも「秒」である。
【０１１６】
表２の「単項式の数の比」が示すように、実施形態に係る処理（実施例）では、大部分のケースにおいて、比較例に比べて単項式の数を削減できている。表２の「演算時間（実施例）」及び「演算時間（比較例）」が示すように、大部分のケースにおいて、比較例に比べて、不変条件生成に要する演算時間を短縮できている。なお、"MARKUS"及び指定部分式がｓである場合の"TRIG"においては、比較例の方が演算時間が短くなっている。これは、実施例においては第２処理３２２にある程度の時間を要するため、比較例において生成される単項式数が少ないと、比較例の方が演算時間が短くなるからである。
【０１１７】
表１の「λ」及び「Generated invariants」が示すように、実施形態の第２処理３２２によって生成された不変条件は、固有値λが１でないλ−不変条件を含んでいる。
【０１１８】
【表３】
0006622098.tif 000015
【０１１９】
表３は、実施形態の不変条件生成モジュール３２０による不変条件生成の演算時間が、短縮されていることを示す実験結果である。表３において、「実験結果１」は、第２処理３２２として第１例を用い、第３処理３２３として固有ベクトル法を用いた場合の不変条件生成の演算時間を示す。「実験結果２」は、第２処理３２２（単項式の生成）は従来のテンプレート法で行い、第３処理３２２は固有ベクトル法を用いた場合の不変条件生成の演算時間を示す。「実験結果３」は、非特許文献１記載の従来のテンプレート法を用いた場合の不変条件生成の演算時間を示す。「実験結果４」は、非特許文献３記載のアルゴリズムを用いた場合の不変条件生成の演算時間を示す。
【０１２０】
表３は、ＳＵＭＰＯＷＥＲ１，ｎ（上段）、ＳＵＭＰＯＷＥＲｋ，ｎ（下段）それぞれについての演算時間を示している。演算時間の単位は「秒」であり、表３に示す演算時間は、５回の実行の平均である。Ｔ／Ｏは、タイムアウトを示す。演算時間が６００秒を超えるとタイムアウトとした。ＳＵＭＰＯＷＥＲｋ，ｎにおいて、ｋは任意の値である。表３は、ＳＵＭＰＯＷＥＲ１，ｎ及びＳＵＭＰＯＷＥＲｋ，ｎにおけるｎを１から１２８にした場合の演算時間を示している。ｎが大きくなると、生成されるλ−不変条件の次数も大きくなる。
【０１２１】
実験結果１によれば、ｎが大きくなっても、タイムアウトせずに、λ−不変条件を生成できていることがわかる。実験結果１と実験結果２とを比較すると、単項式の数が削減されない実験結果２に比べて、実験結果１の演算時間が短くなっている。したがって、実施形態の第２処理３２２（次元型解析）による効果が確認できる。また、実験結果３，４に比べて、実験結果２の演算時間が短くなっている。したがって、実施形態の第３処理３２３（固有ベクトル法）による効果が確認できる。
【０１２２】
［２．５  プログラムコード製造方法］
図７は、実施形態に係る検証装置１００を用いたプログラムコード製造工程を示している。プログラムコード製造工程は、ステップＳ４１からステップＳ４６を含んでいる。
【０１２３】
ステップＳ４１は、プログラムコード（初期コード；検証対象のプログラムコード）を作成するステップである。プログラムコードは、例えば、プログラマーによって作成及び修正される。ステップＳ４２は、検証対象のプログラムコードを、検証装置１００の記憶部３００が、検証対象のプログラムコードを記憶するステップである。ステップ４３は、検証装置１００の不変条件生成モジュール３２０が、検証対象のプログラムコードの不変条件を生成するステップである。ステップＳ４４は、検証装置１００が、生成された不変条件と、記憶部３００に記憶されたプログラムコードと、を用いて、そのプログラムコードの形式的検証を行うステップである。ステップＳ４５においては、検証の結果の判定、すなわち、プログラムコードが不変条件を満たしていたか否かが判定される。ステップＳ４６は、検証の結果に基づいて、プログラムコードを修正するステップである。プログラムコードの検証・修正は、必要に応じて何度か繰り返される。
【０１２４】
プログラムコードの検証・修正を経て、最終的に、不変条件を満たしていると判定されたプログラムコードは、仕様等に照らして、正しいことが証明されたものとなる。したがって、より高品質のプログラムコードが得られる。
【０１２５】
プログラムコードの製造工程について、以下のプログラムコードを例として説明する。
【数１２】
0006622098.tif 000016
【０１２６】
このプログラムコードは、変数sumとiの値を0に初期化し、iが自然数n0に等しくなるまでsumの値にiを加え、iを1増加させるという動作を繰り返す。プログラムコードの末尾のassert(2*sum==n0*(n0+1))は、プログラムが停止したならば、その時点で等式2* sum== n0* (n0+1)が成り立っていなければならないというプログラムの仕様を表す。
【０１２７】
このプログラムについて、実施形態に係る検証装置１００を用いて、プログラムコードのバグを修正する方法を示す。検証装置１００は、このプログラムコード中のｗｈｉｌｅループについて、ループ不変条件として、2*sum==i*(i-1)を生成することができる。
【０１２８】
ループが実行されるための条件はi≠n0なので、ループを抜けた時点では、この否定i == n0が成り立っているはずである。したがって、
【数１３】
0006622098.tif 000017
という条件が、任意のi、sum、非負のn0について成り立てば、このプログラムコードは仕様を満たす。この条件を、以下で条件Ｃと呼ぶことにする。
【０１２９】
しかしながらsum=0,i=1,n0 =1であるときに条件Ｃは満たされない。これは、n0=1であるときに、ループを抜けたときのsumとiの値がそれぞれ0,1であると、仕様が満たされないことを示している。実際に、n0=1であるときの各変数の値を考えると、sumとiの値はプログラム開始時点でそれぞれ0,0であり、ループを一回実行した時点で0,1であり、その後ループを抜けるため、このプログラムコードは仕様を満たしていない。
【０１３０】
n0=1のときに仕様を満たすためにはsumの値がプログラム終了時に1でなければならない。このあるべきsumの値と上記の状態遷移とを比較すると、仕様が満たされるためにはもう一回ループが実行されなければならないことが分かる。もう一回ループが実行されるためには、ループが実行されるための条件をi != n0からi != n0+1に変更しなければならないことが分かる。こうして、修正を加えられた以下のプログラムコードが得られる。
【数１４】
0006622098.tif 000018
【０１３１】
修正されたプログラムコードが、仕様を満たすための条件Ｃ’を条件Ｃを得たのと同様に求める。すなわち、
【数１５】
0006622098.tif 000019
という条件Ｃ’が、任意のsum,iと非負のn0について成り立てば、この修正プログラムコードは仕様を満たす。この条件は実際に成り立っているため、修正プログラムは仕様を満たす。
【符号の説明】
【０１３２】
１００  不変条件生成装置
２００  処理部
３００  記憶部
３１０  検証用プログラム
３２０  不変条件生成モジュール
３２１  第１処理
３２２  第２処理
３２３  第３処理
３３０  検証対象のプログラムコード
【図１】
0006622098.tif 000020
【図２】
0006622098.tif 000021
【図３Ａ】
0006622098.tif 000022
【図３Ｂ】
0006622098.tif 000023
【図４】
0006622098.tif 000024
【図５Ａ】
0006622098.tif 000025
【図５Ｂ】
0006622098.tif 000026
【図６Ａ】
0006622098.tif 000027
【図６Ｂ】
0006622098.tif 000028
【図７】
0006622098.tif 000029