TOP > 国内特許検索 > 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 > 明細書

明細書 :不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法

発行国 日本国特許庁(JP)
公報種別 公開特許公報(A)
公開番号 特開2017-138679 (P2017-138679A)
公開日 平成29年8月10日(2017.8.10)
発明の名称または考案の名称 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法
国際特許分類 G06F  11/36        (2006.01)
FI G06F 9/06 620M
請求項の数または発明の数 6
出願形態 OL
全頁数 23
出願番号 特願2016-017441 (P2016-017441)
出願日 平成28年2月1日(2016.2.1)
発明者または考案者 【氏名】末永 幸平
【氏名】樹下 稔
【氏名】小島 健介
出願人 【識別番号】504132272
【氏名又は名称】国立大学法人京都大学
個別代理人の代理人 【識別番号】110000280、【氏名又は名称】特許業務法人サンクレスト国際特許事務所
審査請求 未請求
テーマコード 5B376
Fターム 5B376BC69
要約 【課題】不変条件を生成するための新たな技術を提供する。
【解決手段】不変条件生成装置100は、プログラムコードが記憶される記憶部300と、不変条件を生成する処理を実行する処理部200を備える。処理部200は、不変条件を生成する第3処理を実行する。第3処理は、プログラムコードが実行されることによる1又は複数の部分式それぞれの変換を表す変換行列の転置である表現行列を生成する行列生成処理と、表現行列の固有値と固有ベクトルを求める演算処理と、固有値及び固有ベクトルの組と、1又は複数の部分式と、に基づいて、不変条件を生成する不変条件生成処理と、を含む。
【選択図】図1
特許請求の範囲 【請求項1】
不変条件生成装置であって、
プログラムコードが記憶される記憶部と、
前記不変条件を生成する処理を実行する処理部を備え、
前記処理は、
前記記憶部から前記プログラムコードを読み出す第1処理と、
多項式を構成するための1又は複数の部分式を生成する第2処理と、
前記不変条件を生成する第3処理と、
を含み、
前記第3処理は、
前記プログラムコードが実行されることによる1又は複数の前記部分式それぞれの変換を表す変換行列の転置である表現行列を生成する行列生成処理と、
前記表現行列の固有値と固有ベクトルを求める演算処理と、
前記固有値及び前記固有ベクトルの組と、1又は複数の前記部分式と、に基づいて、前記不変条件を生成する不変条件生成処理と、
を含む
不変条件生成装置。
【請求項2】
前記表現行列の一つの固有値に対して複数の独立な固有ベクトルが存在する場合には、
前記不変条件生成処理は、複数の固有ベクトルの線形結合を、前記不変条件の生成に用いる
請求項1記載の不変条件生成装置。
【請求項3】
1又は複数の前記部分式それぞれの前記変換が、前記変換行列だけでなく余りベクトルによっても表される場合には、
前記不変条件生成処理は、前記固有ベクトルと前記余りベクトルとの内積が0になる条件の下で前記不変条件を生成する
請求項1又は2記載の不変条件生成装置。
【請求項4】
請求項1~3のいずれか1項に記載の不変条件生成装置としてコンピュータを機能させるためのコンピュータプログラム。
【請求項5】
不変条件を生成する処理を実行する処理部によって実行される方法であって、
記憶部からプログラムコードを読み出す第1処理を実行すること、
多項式を構成するための1又は複数の部分式を生成する第2処理を実行すること、
前記不変条件を生成する第3処理を実行すること、
を含み、
前記第3処理は、
前記プログラムコードが実行されることによる1又は複数の前記部分式それぞれの変換を表す変換行列の転置である表現行列を生成する行列生成処理と、
前記表現行列の固有値と固有ベクトルを求める演算処理と、
前記固有値及び前記固有ベクトルの組と、1又は複数の前記部分式と、に基づいて、前記ループ不変条件を生成する不変条件生成処理と、
を含む
方法。
【請求項6】
プログラムコードを作成すること、
請求項5に記載の前記記憶部が、作成されたプログラムコードを記憶すること、
請求項5に記載の方法によって、前記プログラムコードの不変条件を生成すること、
前記不変条件を用いて、前記プログラムコードの形式的検証を行うこと、
前記形式的検証の結果に基づいて前記プログラムコードを修正すること、
を含むプログラムコードの製造方法。
発明の詳細な説明 【技術分野】
【0001】
本発明は、不変条件生成装置等に関するものである。
【背景技術】
【0002】
不変条件(Invariant)は、プログラムコード(以下、単に「コード」ということがある)の形式的検証(formal verification)に用いられる。形式的検証は、プログラムコードの正当性を数学的な形式的手法で証明することである。プログラムコードに含まれるある処理に対する不変条件は、その処理の実行前後において成立する条件として構成される。while文のようなループ処理に対する不変条件は、ループ不変条件(Loop Invariant)と呼ばれる。ループ不変条件は、ループの開始時点で成立するとともに、ループを何回繰り返しても成立する条件として構成される。
【0003】
不変条件を生成する従来の方法には、非特許文献1等に記載のテンプレート法(template-based method)がある。テンプレート法では、多項式pが、不変条件に関係するテンプレートとして生成される。多項式pは、検証対象のプログラムコードに含まれるシンボルと不定係数によって構成される。シンボルとは、プログラムに含まれる変数又は定数を示す文字又は記号である。そして、p=0が不変条件であるような制約が生成される。この制約を解析することで、不変条件が得られる。
【先行技術文献】
【0004】

【非特許文献1】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.
【非特許文献2】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.
【非特許文献3】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.
【発明の概要】
【0005】
テンプレート法では、テンプレートとなる多項式を用いた制約を明示的に生成するため、処理のための記憶領域が多く必要となり、処理時間も長くなり易い。
【0006】
また、不変条件としては、pの値がコードの1回の実行でλ倍になる不変条件が望ましいことがある。しかし、既存のテンプレート法では、処理コードを実行してもpの値が変わらない不変条件しか生成できない。
【0007】
そこで、不変条件を生成するための新たな技術が望まれる。
【0008】
本発明の一の態様は、不変条件生成装置である。不変条件生成装置は、プログラムコードが記憶される記憶部と、前記不変条件を生成する処理を実行する処理部を備える。前記処理は、前記記憶部から前記プログラムコードを読み出す第1処理と、多項式を構成するための1又は複数の部分式を生成する第2処理と、前記不変条件を生成する第3処理と、を含む。従来のテンプレート法の問題は、第3処理において固有ベクトル法を用いることによって解決される。本発明の他の態様は、不変条件生成装置としてコンピュータを機能させるためのコンピュータプログラムである。本発明の他の態様は、不変条件を生成する処理を実行する処理部によって実行される方法である。本発明の他の態様は、プログラムコード製造方法である。
【図面の簡単な説明】
【0009】
【図1】検証装置の構成図である。
【図2】第2処理の第1例のフローチャートである。
【図3A】第2処理の第2例のフローチャートである。
【図3B】第2処理の第2例の実行例を示す図である。
【図4】第3処理のフローチャートである。
【図5A】第3処理の第1実行例を示す図である。
【図5B】第3処理の第1実行例を示す図である。
【図6A】第3処理の第2実行例を示す図である。
【図6B】第3処理の第2実行例を示す図である。
【図7】プログラムコード製造方法のフローチャートである。
【発明を実施するための形態】
【0010】
[1.実施形態の概要]
(1)実施形態に係る不変条件生成装置は、プログラムコードが記憶される記憶部と、前記不変条件を生成する処理を実行する処理部を備える。プログラムコードとは、例えば、プログラムのソースコードである。前記処理は、前記記憶部から前記プログラムコードを読み出す第1処理と、多項式を構成するための1又は複数の部分式を生成する第2処理と、前記不変条件を生成する第3処理と、を含む。

【0011】
部分式は、典型的には、多項式に含まれる単項式である。単項式は、プログラムに含まれるシンボルの冪積と冪積に掛けられる係数によって構成されていてもよいし、係数を有さず冪積だけで構成されていてもよい。プログラムに含まれるシンボルは、例えば、変数又は定数である。部分式は、多項式に含まれる部分的な多項式であってもよい。なお、単項式は、項数が1である特殊な多項式の形式であると考えることができる。

【0012】
前記第3処理は、前記プログラムコードが実行されることによる1又は複数の前記部分式それぞれの変換を表す変換行列の転置である表現行列を生成する行列生成処理と、前記表現行列の固有値と固有ベクトルを求める演算処理と、前記固有値及び前記固有ベクトルの組と、1又は複数の前記部分式と、に基づいて、前記不変条件を生成する不変条件生成処理と、を含む。

【0013】
(2)前記表現行列の一つの固有値に対して複数の独立な固有ベクトルが存在する場合には、前記不変条件生成処理は、複数の固有ベクトルの線形結合を、前記不変条件の生成に用いることができる。

【0014】
(3)1又は複数の前記部分式それぞれの前記変換が、前記変換行列だけでなく余りベクトルによっても表される場合には、前記不変条件生成処理は、前記固有ベクトルと前記余りベクトルとの内積が0になる条件の下で前記不変条件を生成することができる。

【0015】
(4)実施形態に係るコンピュータプログラムは、(1)項~(3)項のいずれか1項に記載の不変条件生成装置としてコンピュータを機能させる。

【0016】
(5)実施形態に係る方法は、不変条件を生成する処理を実行する処理部によって実行される。方法は、記憶部からプログラムコードを読み出す第1処理を実行すること、多項式を構成するための1又は複数の部分式を生成する第2処理を実行すること、を含む。

【0017】
前記第3処理は、前記プログラムコードが実行されることによる1又は複数の前記部分式それぞれの変換を表す変換行列の転置である表現行列を生成する行列生成処理と、前記表現行列の固有値と固有ベクトルを求める演算処理と、前記固有値及び前記固有ベクトルの組と、1又は複数の前記部分式と、に基づいて、前記ループ不変条件を生成する不変条件生成処理と、を含む。

【0018】
(6)実施形態に係るプログラムコード製造方法は、プログラムコードを作成すること、前記記憶部が、作成されたプログラムコードを記憶すること、(5)項に記載の方法によって、前記プログラムコードの不変条件を生成すること、前記不変条件を用いて、前記プログラムコードの形式的検証を行うこと、前記形式的検証の結果に基づいて前記プログラムコードを修正すること、を含む。

【0019】
[2.実施形態の詳細]

【0020】
[2.1 プログラムコードの例]
以下ではプログラム検証の対象となるプログラムコードの例を説明する。これらのコードは、シンボル同士の積などの非線形表現を含む。

【0021】
[2.1.1 ACCELESIST
【数1】
JP2017138679A_000003t.gif

【0022】
CCELESISTは、質量が1であり、一定の加速度gを持つ質量点の挙動をモデル化したものである。ACCELESISTは、シンボルx,v,t,ε,g,ρを含む。xは質量点の位置である。vは、質量点の速度である。tは時間である。xは初期位置である。vは、初期速度である。gは加速度である。ρは質量点と空気との間の摩擦係数である。εは離散間隔である。

【0023】
while(*){...}は、繰り返し毎に実行を終了するか否かを非決定的に選択するループである。{...}の中身は、ループ本体である。例のループ本体においては、同時代入文が記載されている。同時代入文は、複数の変数を更新するものである。例では、同時代入により、変数x,v,tの値が更新される。

【0024】
xの更新式x:=x+vεは、以下の微分方程式に基づく。
【数2】
JP2017138679A_000004t.gif

【0025】
tの更新式t:=t+εは、以下の微分方程式に基づく。
【数3】
JP2017138679A_000005t.gif

【0026】
vの更新式v:=v-gε-ρvεは、以下の微分方程式に基づく。-ρvは、空気によって質量点に与えられる力である。
【数4】
JP2017138679A_000006t.gif

【0027】
[2.1.2 SUMOWERk,n
【数5】
JP2017138679A_000007t.gif

【0028】
UMOWERk,nは、変数sに、以下の式の値をセットするプログラムコードである。mは、ループ繰り返しの回数である。k,nは、任意の整数である。
【数6】
JP2017138679A_000008t.gif

【0029】
[2.2 テンプレート法による不変条件の生成]
ループ不変条件を生成する従来の方法としては、非特許文献1等に記載のテンプレート法(template-based method)がある。テンプレート法は、最初に、ループ不変表明のテンプレートを指定する。例えば、テンプレート法に基づくアルゴリズムは、ACCELESISTのループ不変表明のテンプレートとして、次の2次多項式p(x,v,t,ε,g,ρ)を生成する。
【数7】
JP2017138679A_000009t.gif

【0030】
上記の多項式p(x,v,t,ε,g,ρ)は、複数の単項式を有して構成されている。単項式は、ACCELESISTに含まれるシンボルx,v,t,ε,g,ρからなる冪積(power products)と、冪積に掛けられた不定係数a,...,a28と、含む。

【0031】
次に、テンプレート法に基づくアルゴリズムは、制約(constraint)を生成する。生成される制約は、p(x,v,t,ε,g,ρ)=0がループ不変条件であるような制約である。この制約を解析することで、a,...,a28を求める。制約を解析するには、以下の条件を計算すればよい。以下の条件は、ACCELESISTのループを1回繰り返しても、p(x,v,t,ε,g,ρ)の値が変わらないことを示している。
【数8】
JP2017138679A_000010t.gif

【0032】
上記の式で示される条件を計算することで、a25=a24=a23=a22=a21=a20=a19=a18=a16=a15=a14=a10=a=a=a=aと、a=a17と、が得られる。

【0033】
得られた係数を、p(x,v,t,ε,g,ρ)=0に代入することで、以下の式がループ不変条件として得られる。以下の式において、a,a,a,a,a11,a12,a13,a17,a26,a27,a28は、任意の定数である。
【数9】
JP2017138679A_000011t.gif

【0034】
上記のループ不変条件が示す本質的な点は、ループ本体に記載された代入が繰り返されても、gt+vが定数のままである、ということである。

【0035】
テンプレート法に基づくアルゴリズムは、SUMOWERk,10のループ不変表明として、以下の式を得ることができる。
【数10】
JP2017138679A_000012t.gif

【0036】
しかし、SUMOWERk,10のループ不変表明を発見するには、次数が11である多項式をテンプレートとして生成する必要がある。一般に、3変数を持つn次多項式は、O(n)もの単項式を持つことになる。単項式の数の増大は、制約を大規模にする。この結果、制約を解析するのに時間を要し、実用的な時間内に不変条件を生成できないこともある。
このように、単項式の数の増大は、高次多項式テンプレートを用いたテンプレート法の適用を困難にする。

【0037】
また、テンプレート法では、テンプレートとなる多項式を用いた制約を明示的に生成するため、処理のための記憶領域が多く必要となり、処理時間も長くなり易い。

【0038】
しかも、不変条件としては、pの値がコードの1回の実行でλ倍になる不変条件(以下、「λ-不変条件」という)が望ましいことがある。しかし、既存のテンプレート法では、コードを実行してもpの値が変わらない不変条件しか生成できない。

【0039】
例えば、ACCELESISTのための他の有用なループ不変条件として、以下の式がある。mは、ループ繰り返しの回数であり、t/εに等しい。
【数11】
JP2017138679A_000013t.gif

【0040】
この不変条件は、ACCELESISTのループの1回の繰り返しで、(v-g/ρ)が、(1-ρε)倍になることを示している。すなわち、λ=(1-ρε)である。したがって、この不変条件は、「(1-ρε)-不変条件」である。また、[数9]に示す不変条件は、ループの1回の繰り返しでpが変わらない、つまり、pが1倍(λ=1)になる不変条件であるから、「1-不変条件」である。

【0041】
[2.3 実施形態に係る不変条件の生成処理]

【0042】
[2.3.1 検証装置]
図1は、プログラムコードの形式的検証のための検証装置100を示している。検証装置100は、処理部200と、記憶部300と、を備えたコンピュータを有して構成されている。処理部200は、例えば、CPUを有して構成されている。記憶部300は、処理部200によって読み取られる情報が格納されている。記憶部300に格納された情報は、検証用プログラム310を含む。記憶部300に格納された情報は、検証対象のプログラムコード330も含む。

【0043】
検証用プログラム310は、コンピュータを、検証装置100として機能させるためのコンピュータプログラムである。処理部200は、検証用プログラム310を実行することで、検証対象のプログラムコード330に対する形式的検証のための処理を行う。検証用プログラム310は、不変条件生成モジュール320を有している。不変条件生成モジュール320は、検証対象のプログラムコード330の形式的検証に用いる不変条件を生成する処理を実行する。したがって、検証装置100は、不変条件生成装置としても機能する。検証用プログラム310は、生成した不変条件を用いて、検証対象のプログラムコード330の形式的検証を行う。

【0044】
検証対象のプログラムコード330は、例えば、前述のACCELESIST又はSUMOWERk,nである。以下の説明では、必要に応じて、前述のACCELESIST又はSUMOWERk,n以外のプログラムコードも説明に用いる。

【0045】
[2.3.2 処理概要]
不変条件の生成処理320は、第1処理321と、第2処理322と、第3処理323と、を含む。第1処理321は、記憶部300から検証対象のプログラムコード330を読み出す処理である。処理部200は、読み出したコード330を用いて、不変条件を生成する。以下では、読み出したコード330に含まれるループ文(while文)のための不変条件であるループ不変条件の生成について説明する。

【0046】
第2処理322は、多項式を構成する部分式を生成する処理である。第2処理322は、従来のテンプレート法でいうと、テンプレートとなる多項式を構成する単項式又は単項式に含まれる冪積(power products)を生成する処理に対応する。従来のテンプレート法では、前述のように単項式の数が増大し易いが、実施形態に係る第2処理322では、多項式を構成する単項式(冪積)の数を削減することができる。

【0047】
第3処理323は、生成した部分式に基づき、読み出したコード330に対する不変条件を生成する処理である。第3処理323は、従来のテンプレート法でいうと、テンプレートである多項式p=0がループ不変条件であるような制約を解いて、ループ不変条件を生成する処理に対応する。従来のテンプレート法では、λ=1である「1-不変条件」しか生成できなかったが、実施形態に係る第3処理323では、λ=1以外のλ-不変条件を生成することができる。また、実施形態に係る第3処理323では、生成された部分式を用いるものの、テンプレートを明示的に生成する必要がないので、第3処理323の際に必要とする記憶容量が比較的少なくて済む。

【0048】
[2.3.3 コード解析による部分式生成(第2処理)の第1例]
第2処理322は、指定部分式wが与えられると、指定部分式wに関連する複数の関連部分式を生成する処理である。図2は、第2処理322の第1例を示している。第2処理322の第1例は、ステップS11からステップS14までの処理を含む。図2には、ACCELESISTを例とした場合の、各ステップの処理結果を示している。

【0049】
ステップS11は、入力受付処理である。入力受付処理では、指定部分式w及び指定次数nの入力をユーザから受け付ける。

【0050】
指定部分式wは、関連部分式を発見するためのものである。指定部分式wは、読み出したコード330に含まれる1又は複数のシンボルからなる式である。指定部分式wは、典型的には、単項式(冪積)であるが、2以上の単項式を含む多項式であってもよい。指定部分式wの次数は、指定次数n以下であるのが好ましい。コード330がACCELESISTである場合、例えば、単項式vが、指定部分式wとして入力される。

【0051】
指定次数nは、関連部分式として生成される式の次数の制限である。指定次数n以下の次数の式が、後述の関連部分式として生成される。ACCELESISTの場合、例えば、2が指定次数nとして入力される。

【0052】
指定部分式w及び/又は指定次数nの取得は、ユーザ入力による取得に代えて、装置100自らが生成した指定部分式w及び/又は指定次数nの取得であってもよい。例えば、装置100は、コード330に含まれる1又は複数のシンボルを用いて、指定次数n以下の次数となるシンボルの組み合わせをランダムに決定して、指定部分式wを得ても良い。また、装置100は、指定次数nをランダムに決定してもよい。さらに、装置100は、指定次数nを1から開始して部分式生成が成功しなければ、指定次数nを+1としてもよい。

【0053】
ステップS12は、コード330に基づく解析によって、コード330に含まれるシンボルの次元型を求める処理(型環境Γの取得処理)である。第2処理322の第1例では、テンプレートを構成し得る部分式(単項式)の数を削減するため、「量の次元(quantity dimension)」という概念を利用する。量の次元は、物理学での概念であり、長さ、時間、速度などの物理量の型である。量の次元は、「物理次元」とも呼ばれる。量の次元は、物理量の基本型である基礎次元の積として表される。例えば、基礎次元としてLとTを考える。Lは、長さを示す基礎次元であり、Tは時間を示す基礎次元である。次元の積は、物理量がどのように計算して得られるかを示す。例えば、速度は、次元型LT-1を有する。速度は、距離を時間で割って得られるからである。加速度は、次元型LT-2を有する。加速度は、速度を時間で割って得られるからである。

【0054】
ここで、ACCELESISTに含まれるシンボルは、x,v,t,ε,g,ρである。ACCELESISTのループ本体中のコマンド(代入文)である(x、v、t):=(x+vε,v-gε-ρvε,t+ε)を解析すると、ACCELESISTにおいて、xの次元型はLであり、vの次元型はLT-1であり、tの次元型はTであり、εの次元型はTであり、gの次元型はLT-2であり、ρの次元型はT-1であることが求まる。コード330に含まれるシンボルx,v,t,ε,g,ρの次元型を示す情報を型環境Γという。

【0055】
なお、コマンド中のx+vεの次元型はLであり、v-gε-ρvεの次元型はLT-1であり、t+εの次元型はTである。

【0056】
物理学上の原則に基づくと、異なる次元型の量同士を加算することはできない。例えば、時間を長さに加算することはできないし、速度を長さに加算することもできない。この原則に基づくと、数7に示すテンプレート多項式p(x,v,t,ε,g,ρ)は、物理的に無意味な量を表していることがわかる。すなわち、テンプレート多項式p(x,v,t,ε,g,ρ)は、例えば、次元型がTとなる単項式(at,aε)と、次元型がLT-1となる単項式(av,a17tg,a26εg,a25xρ)と、の和となっており、異なる次元型の量同士を加算している。したがって、次元型を考慮すれば、異なる次元型の量同士を加算するようなテンプレートが構築されるのを防止して、テンプレートのサイズを小さくすることができる。

【0057】
コード330に含まれるシンボルの次元型の推論(型環境Γの取得)は、型推論アルゴリズムを用いた次元型解析によって行われる。型推論アルゴリズムは、コード330を解析して、コード330に含まれるシンボルの次元型を推論する。型推論アルゴリズムとしては、非特許文献2にて提案された次元型システム(dimension type system)を用いることができる。次元型システムは、関数型プログラミング言語のために提案され、現在では、プログラミング言語F#に実装されている。

【0058】
ステップS13は、型環境Γに基づいて、指定部分式wの次元型を求める処理である。指定部分式wがvである場合、指定部分式wの次元型は、LT-1となる。なお、指定部分式wが、例えば、vtであれば、v及びtそれぞれの次元型LT-1,Tに基づいて、vtの次元型は、Lとなる。

【0059】
ステップS14は、複数の関連部分式を生成する処理である。関連部分式とは、指定部分式wとの関連性が確認された部分式をいう。関連部分式は、テンプレートとなる多項式を構成することができる。テンプレートは、例えば、複数の関連部分式の線形結合として表される。関連部分式wは、典型的には、単項式(冪積)であるが、2以上の単項式を含む多項式であってもよい。

【0060】
第1例では、指定部分式wとの関連性の確認を、指定部分式wの次元型を用いて行う。より具体的には、第1例で生成される関連部分式は、指定部分式wの次元型(LT-1)と一致する次元型を有することが確認された部分式である。関連部分式は、コード330に含まれるシンボルx,v,t,ε,g,ρから構成可能な部分式(冪積)の中から、指定部分式wの次元型(LT-1)と一致する次元型を有する部分式(冪積)を選択することで得られる。関連部分式として生成される部分式の次数は、指定次数n以下である。

【0061】
シンボルx,v,t,ε,g,ρから構成可能な部分式(冪積)であって、指定次数n以下の部分式の集合は、{t,v,x,ε,g,ρ,t,v,x,ε,g,ρ,tv,tx,tε,tg,tρ,vx,vε,vg,vρ,xε,xg,xρ、εg,ερ,gρ}である。この集合の要素数は、指定次数nが大きくなると多くなる。したがって、指定次数nを大きくすると、多くの関連部分式を生成し易くなる。この集合の要素のうち、次元型がLT-1となるのは、{v,ρx,gt,εg}である。したがって、ステップ14では、複数の関連部分式として、{v,ρx,gt,εg}を生成する。関連部分式は、指定部分式を含んでも良い。

【0062】
複数の関連部分式{v,ρx,gt,εg}からテンプレート多項式を構成すると、テンプレート多項式は、av+aρx+agt+aεgとなる。ここで、a,a,a,aは、不定係数である。このテンプレート多項式は、[数7]に示すテンプレート多項式に比べて、単項式の数が少なく、不定係数の数も少ない。したがって、不変条件を求めるのが容易となる。

【0063】
従来のテンプレート法に従うと、コード330に含まれる複数のシンボルが取り得る全ての組み合わせからなる多数の部分式(冪積)によって、テンプレート多項式が構成される(数7参照)。つまり、従来のテンプレート法では、テンプレート多項式の構成の際に、コード330における複数のシンボル間の関係を考慮することなく、コード330に含まれるシンボルから得られる冪積の単なる全列挙によって、テンプレート多項式が構成されている。このため、テンプレート多項式は、コード330における複数のシンボル間の関係に照らして、不適切な単項式まで含むことになり、規模が大きくなり易い。従来のテンプレート法では、不適切な単項式を含むテンプレート多項式を生成し、制約を解くことで、不適切な単項式(係数aが0となる単項式)を見つけていた。この結果、大規模な制約を解く必要があり、演算時間が長くなり易かった。

【0064】
これに対して、実施形態に係る第2処理322では、コード330の解析によって、指定部分式との関連が確認された関連部分式(関連単項式)を生成するため、不適切な単項式(指定部分式との関連性がない部分式)を排除することができる。

【0065】
なお、本実施形態の第3処理323では、テンプレート多項式を明示的に作成する必要がない固有ベクトル法を用いる。したがって、生成された関連部分式{v,ρx,gt,εg}は、テンプレート多項式に変換されることなく、生成された関連部分式{v,ρx,gt,εg}自体が、第3処理323に与えられる。ただし、第3処理323では、テンプレート多項式を明示的に作成して、制約を解くことで不変条件を生成してもよい。

【0066】
実施形態において、どのような手法で第3処理323を行うにしろ、第2処理322で生成された関連部分式の数が少ないため、第3処理323の処理負荷が軽減される。

【0067】
なお、第2処理322において、指定次数n以下では、指定部分式w以外の関連部分式を発見できなかった場合、処理部200が、自動的に、指定次数nを増加(例えば、+1)させて、ステップS14を再度実行してもよい。指定次数nを大きくすると、シンボルx,v,t,ε,g,ρから構成可能な部分式(冪積)の数が増加するため、指定部分式wの次元型と一致する部分式が存在する可能性が高まる。なお、指定次数nの変更は、増加以外の変更であってもよく、例えば、指定次数nのランダムな変更であってもよい。

【0068】
また、第2処理322において、指定部分式w以外の関連部分式を発見できなかった場合、処理部200が、自動的に、指定部分式を他の部分式に変更して、ステップS13及びステップS14を再度実行してもよい。

【0069】
ここで、「量の次元」の概念に基づく部分式の数の削減は、ACCELESISTのように物理現象をモデル化したプログラムコードだけでなく、物理現象をモデル化していないプログラムコード、例えば、SUMOWERk,nにも適用できる。例えば、SUMOWERk,10は、意味のある物理現象に対応していない。しかし、実施形態に係る第2処理322では、SUMOWERk,10に関し、指定部分式wとしてksが与えられ、指定次数nとして11が与えられると、関連部分式の集合として{x11,x10k,x,x,x,x,xk10,ks}を生成することができる。

【0070】
なお、型環境Γとして、sは次元型T10の量であり、kは次元型Tの量であり、xは次元型Tの量であることが求まる。ここで、Tは、基礎次元であるが、物理的な意味のある次元ではなく、仮想的な次元である。このように、次元型の概念は、非物理現象をモデル化したプログラムコードにも適用可能である。したがって、図2に示す第2処理322は、プログラムコードが何をモデル化しているかにかかわらず適用できる。

【0071】
[2.3.4 コード解析による部分式生成(第2処理)の第2例]
第2処理322の第1例では、次元型の一致を、部分式の関連性の確認に用いていたが、第2処理322の第2例では、図3Aに示すアルゴリズムによって、部分式の関連性の確認を行う。第2例においても、第1例と同様に、部分式の関連性の確認のために、コード330の解析を行う。

【0072】
第2処理322の第2例は、ステップ21からステップ24までの処理を含む。図3Bは、while(*){(s,c):=(s+cε、c-sε)}のプログラムコードを例とした場合の、各ステップの処理結果を示している。

【0073】
ステップS21は、入力受付処理である。入力受付処理では、ステップS11と同様に、指定部分式wの入力をユーザから受け付ける。ただし、ステップS21では、指定次数を受け付ける必要はない。ここでは、例として、単項式sが、指定部分式wとして入力される。なお、指定部分式の取得は、装置100が生成した指定部分式の取得であってもよい。

【0074】
ステップS22は、関数φ(q)を取得する処理である。図3Aに示すアルゴリズムでは、部分式の関連性の確認のために関数φ(q)を用いる。ここで、qは、多項式を示す変数である。φは、qが示す式を、プログラムコードに従って変化させる関数である。qが示す多項式は、プログラムコードの実行によって値が更新されるシンボル(変数)sを含んでいる。したがって、qが示す多項式の値は、プログラムコードであるループ文(while文)1回の実行によって変化する。φは、プログラムコードであるループ文(while文)1回の実行により変化した値を示す多項式を生成する。例えば、while(*){(s,c):=(s+cε、c-sε)}の場合、while文1回の実行によって、s:=s+cεの代入及びc:=c-sεの代入が生じ、多項式q=sの値は、(s+cε)=s+2εsc+εに変化する。したがって、φ(s)は、s+2εsc+εを生成する。

【0075】
ステップS22では、プログラムコードwhile(*){(s,c):=(s+cε、c-sε)}を解析し、関数φ(q)を作成するための情報として、s:=s+cε及びc:=c-sεを取得する。関数φ(q)を作成するための情報は、一般に、プログラムコード中において、シンボル(変数)の値を更新するコマンド(例えば、代入文)が相当する。ここでは、取得した情報s:=s+cε及びc:=c-sεに基づき、関数φ(q)は、qに含まれるsをs+cεに写像し、qに含まれるcをc-sεに写像する関数として生成される。

【0076】
ステップS23では、図3AのステップS23のボックス中に示すステップ1からステップ6の処理が実行される。図3Bに示すように、ステップ1では、指定部分式w=sだけを要素として有する初期集合Bが生成される。集合Bは、部分式を要素として持つ集合である。ステップ2では、指定部分式sが変数qの初期値として設定される。

【0077】
ステップ3は、whileループの繰り返し条件判定である。ステップ4,5は、whileループ本体であり、ステップ6は、whileループの終わりを示す。whileループの繰り返し条件判定に含まれる<B>は、集合Bに含まれる部分式の線形結合となる式の集合を示す。whileループの繰り返し条件判定は、ステップ3に示すように、φ(q)が、集合Bに含まれる部分式の線形結合となる式の集合に含まれていないことである。φ(q)が、集合Bに含まれる部分式の線形結合となる式の集合に含まれていれば、whileループは終了する。

【0078】
φ(q)が、集合Bに含まれる部分式の線形結合となる式の集合に含まれているか否かの判定は、例えば、φ(q)を、集合Bに含まれる部分式の線形結合となる式で表現するための線形結合係数が存在するか否かの判定によって行われる。例えば、whileループ1回目の繰り返し条件判定(ステップ3)において、φ(q)=s+2εsc+εであり、B={s}である。したがって、図3Bに示すように、s+2εsc+ε=asを満たす係数aが存在するか否かが判定される。そのような係数aは、存在しないから、whileループの繰り返し条件を満たす。したがって、繰り返しは終了せず、whileループ本体であるステップ4,5が実行される。

【0079】
ステップ4は、集合Bの更新ステップ(第1更新ステップ)である。図3Bに示すように、ステップ4では、集合Bの要素にφ(q)が加えられる。whileループ1回目のステップ4において、B={s,s+2εsc+ε}となる。

【0080】
ステップ5は、変数qの更新ステップ(第2更新ステップ)である。ステップ5では、φ(q)が新たなqとなる。whileループ1回目のステップ5において、q=s+2εsc+εとなる。

【0081】
whileループ2回目の繰り返し条件判定(ステップ3)において、φ(q)=(1-2ε+ε)s+(4ε-4ε)sc+4εであり、B={s,s+2εsc+ε}である。したがって、(1-2ε+ε)s+(4ε—4ε)sc+4ε=as+b(s+2εsc+ε)を満たす係数a,bが存在するか否かが判定される。そのような係数a,bは、存在しないから、whileループの繰り返し条件を満たす。

【0082】
whileループ2回目のステップ4において、B={s,s+2εsc+ε,(1-2ε+ε)s+(4ε—4ε)sc+4ε}となる。

【0083】
whileループ2回目のステップ5において、q=(1-2ε+ε)s+(4ε-4ε)sc+εとなる。

【0084】
whileループ3回目の繰り返し条件判定(ステップ3)において、φ(q)は、(1-6ε+9ε)s+(6ε-20ε+6ε)sc+(9ε-6ε+ε)cであり、B={s,s+2εsc+ε,(1-2ε+ε)s+(4ε—4ε)sc+4ε}である。したがって、(1-6ε+9ε)s+(6ε-20ε+6ε)sc+(9ε-6ε+ε)c=as+b(s+2εsc+ε)+d{(1-2ε+ε)s+(4ε—4ε)sc+4ε}を満たす係数a,b,dが存在するか否かが判定される。

【0085】
a=1+3ε+3ε+ε,b=-3-2ε+ε,d=3-εとした場合、上記の式を満たす。つまり、φ(q)が、集合Bに含まれる1又は複数の部分式の線形結合として表現される式になることが確認されたことになる。したがって、whileループの繰り返し条件は満たされなくなり、whileループは終了する。

【0086】
ステップS24では、whileループを終了した時点での集合B={s,s+2εsc+ε,(1-2ε+ε)s+(4ε—4ε)sc+4ε}が、指定部分式wに関連することが確認された関連部分式の集合として出力される。

【0087】
第2処理322の第2例においても、コード330の解析によって、指定部分式wとの関連が確認された関連部分式(関連多項式)を生成するため、不適切な部分式(指定部分式との関連性がない部分式)を排除することができる。

【0088】
なお、第2処理322の第2例において、ステップS23中のwhileループが所定時間内に終了しない場合、すなわち、関連部分式を発見できなかったものとみなして、whileループを強制終了する。この場合、指定部分式を他の部分式に変更して、ステップS22からステップS24を再度実行すればよい。

【0089】
[2.3.5 固有ベクトル法による不変条件生成(第3処理)]
第3処理323は、第2処理322で生成された関連部分式から、不変条件を生成する処理である。なお、第3処理323において不変条件を生成するのに用いられる部分式は、第2処理322で生成された関連部分式に限られず、従来のテンプレート法において生成されるテンプレート多項式を構成する複数の単項式(冪積)であってもよい。

【0090】
さて、プログラムコードが実行されることによる複数の関連部分式それぞれの変換を表す変換行列Mを考えた場合、その変換行列Mの転置である表現行列(representation matrix)Mは、固有値と固有ベクトルとを持つ。なお、Tは、転置を示す。本発明者らは、表現行列Mの固有値と固有ベクトルとが不変条件を与えることを見出した。したがって、不変条件の生成は、表現行列の固有値と固有ベクトルを求めるという簡易な処理によって行うことができる。なお、表現行列の固有値と固有ベクトルを求めることで、不変条件を生成することを、「固有ベクトル法」というものとする。

【0091】
図4は、固有ベクトル法による不変条件生成(第3処理323)を示している。第3処理323は、ステップ31からステップS33までの処理を含む。図5A,5Bは、ACCELESISTを例とした場合の処理結果を示している。図5A,5Bでは、複数の関連部分式として、第2処理322の第1例に示すように、{v,ρx,gt,εg}が生成されているものとする。

【0092】
ステップS31は、表現行列Mと、余りベクトルqと、を生成する処理(行列生成処理;余りベクトル生成処理)である。

【0093】
表現行列Mは、プログラムコードが実行されることによる複数の関連部分式それぞれの変換を表す変換行列Mの転置行列として生成される。余り行列qは、複数の関連部分式それぞれの変換が、変換行列Mだけでは表現できない場合に生成される。余り行列qは、図5A,5Bの例では生成されないが、図6A,6Bの例では生成される。

【0094】
CCELESISTの場合、ステップS31では、まず、図5Aに示す変換行列Mが生成される。変換行列Mは、ACCELESISTのwhileループ1回の実行による、複数の関連部分式それぞれの変換を表す行列として生成される。関連部分式が{v,ρx,gt,εg}である場合、(x,v,t)=(x+vε,v-gε-ρvε)の実行により、関連部分式gtはg(t+ε)に変換され、関連部分式gεはgεに変換され、vはv-gε-ρvεに変換され、ρxはρ(x+vε)に変換される。これらの変換関係より、図5Aに示す変換行列Mが得られる。関連部分式の変換は、変換行列Mだけで表現することができるので、前述のように余りベクトルqは生成されない。

【0095】
図5Aに示す変換行列Mの転置により、図5Aに示す表現行列Mが生成される。

【0096】
ステップS32は、表現行列Mの固有値と固有ベクトルとを求める処理(演算処理)である。表現行列Mの固有値と固有ベクトルとは既知の手法によって算出される。図5Aに示す表現行列Mは、2つの固有値を持つ。一つ目の固有値は1である。二つ目の固有値は(1-ρε)である。図5Aに示すように、固有値1に対応する固有ベクトルは(-1,0,1,1)及び(0,1,0,0)であり、固有値(1-ρε)に対応する固有ベクトルは(0,-1/ερ,1,0)である。

【0097】
ステップS33は、固有値λとその固有値λに対応する固有ベクトルとの組み合わせから、λ-不変条件を生成する処理(不変条件生成処理)である。λ-不変条件は、前述のように、ループの1回の繰り返しで値がλ倍になる不変条件である。固有値と固有ベクトルとの組が、一つの不変条件に対応する。したがって、固有値と固有ベクトルとの組が複数ある場合には、組ごとに不変条件を生成する処理が行われる。

【0098】
固有値1に対応する固有ベクトル(-1,0,1,1)及び(0,1,0,0)は、1-不変条件として、a(-gt+v+ρx)+b(gε)を与える。複数の関連部分式{gt,gε,v,ρx}をベクトル(gt,gε,v,ρx)として扱うと、固有ベクトルとベクトル(gt,gε,v,ρx)との内積が、1-不変条件となる。1-不変条件は、前述のように、ループの1回の繰り返しで値が変化しない不変条件である。

【0099】
ここで、一つの固有値に対して、複数の独立な固有ベクトルが存在する場合には、複数の独立な固有ベクトルの線形結合を不変条件の生成に用いればよい。例えば、固有値”1”に対応する固有ベクトルが(-1,0,1,1)及び(0,1,0,0)Tである場合、それらの線形結合は、(-a,b,a,b)である。ここで、a,bは、任意の係数である。固有ベクトルの線形結合(-a,b,a,b)とベクトル(gt,gε,v,ρx)との内積は、a(-gt+v+ρε)+b(gε)である。したがって、ステップS33では、a(-gt+v+ρε)+b(gε)が、ACCELESISTの1-不変条件として生成される。

【0100】
固有値(1-ρε)に対応する固有ベクトルは(0,-1/ερ,1,0)は、(1-ρε)-不変条件として、c(-g/ρ+v)を与える。固有ベクトル(0,-1/ερ,1,0)と、ベクトル(gt,gε,v,ρx)と、の内積は、c(-g/ρ+v)である。ここで、cは、任意の係数である。したがって、ステップS33では、c(-g/ρ+v)が、ACCELESISTの(1-ρε)-不変条件として生成される。

【0101】
図6A,6Bは、別のプログラムコードwhile(*){(x,y,z):=(x,y+x,z-x)}についての第3処理323の処理例を示している。ここでは、複数の関連部分式として{z,y,x}が生成されているものとする。

【0102】
ステップS31では、まず、図6Aに示す変換行列Mが生成される。変換行列Mは、プログラムコードwhile(*){(x,y,z):=(x,y+x,z-x)}のwhileループ1回の実行による、複数の関連部分式それぞれの変換を表す行列として生成される。関連部分式が{z,y,x}である場合、(x,y,z):=(x,y+x,z-x)の実行により、関連部分式xはz-xに変換され、関連部分式yはy+xに変換され、xはxに変換される。これらの変換関係より、図6Aに示す変換行列M及び余りベクトルqが生成される。ここでは、関連部分式の変換は、変換行列Mだけは表現することができないので、関連部分式の変換を完全に表現するための余りベクトルqが生成される。

【0103】
図6Aに示す変換行列Mの転置により、図6Aに示す表現行列Mが生成される。

【0104】
ステップS32では、図6Aに示す表現行列Mの固有値として1が求められ、固有値1に対応する2つの固有ベクトル(1,1,0)及び(-1,0,1)が求められる。

【0105】
ステップS33では、まず、固有値1に対応する2つの固有ベクトル(1,1,0)及び(-1,0,1)の線形結合が求められる。2つの固有ベクトルの線形結合は、図6Bに示すように、(C-C,C,Cである。ここで、C,Cは、任意の係数である。

【0106】
本発明者らは、余りベクトルqが存在する場合であっても、固有ベクトル(複数の固有ベクトルの線形結合を含む)と余りベクトルqとの内積が0になる条件が満たされれば、固有値λと固有ベクトル(複数の固有ベクトルの線形結合を含む)とが、λ-不変条件を与えることを見出した。

【0107】
そこで、余りベクトルqが生成されている場合には、ステップ33では、固有ベクトル(複数の固有ベクトルの線形結合を含む)と余りベクトルqとの内積が0になる条件を求める。複数の固有ベクトルの線形結合(C-C,C,Cと余りベクトル(0,0,x)との内積は、図6Bに示すように、Cである。C=0となる条件は、C=0である。C=0という条件を満たす固有ベクトルの線形結合は、図6Bに示すように、(C,C,0)である。C=0という条件を満たす固有ベクトルの線形結合(C,C,0)と関連部分式ベクトル(z,y,x)Tとの内積は、C(z+y)である。したがって、ステップS33では、C(z+y)が、プログラムコードwhile(*){(x,y,z):=(x,y+x,z-x)}の1-不変条件として生成される。

【0108】
以上のように、実施形態の第3処理323では、固有ベクトルを求めるなどの簡単な処理で、不変条件を生成することができる。

【0109】
[2.4 実験結果]
以下の表1は、さまざまなプログラムコードの不変条件を生成した実験結果を示している。表1,2は、実施形態の不変条件生成モジュール320によって、不変条件を生成した結果を示している。なお、第2処理322として、図2に示す第1例を用い、第3処理323としては、固有ベクトル法を用いた。
【表1】
JP2017138679A_000014t.gif
【表2】
JP2017138679A_000015t.gif

【0110】
表1,2において、「名称」は、検証対象のプログラムコードの名称を示す。表1において「プログラム」は、検証対象のプログラムコードのループ本体(while(*){}の中身)を示している。

【0111】
表1,2において、「w」は、指定部分式を示し、nは指定次数を示している。表1において、「λ」は、実施形態に係る処理によって生成された固有値を示し、「Generated invariants」は、実施形態に係る処理によって生成されたλ-不変条件を示している。

【0112】
表2において、「単項式の数の比」は、単項式の数に関し、実施例における数と比較例における数との比を示している。実施例における数は、実施形態の第2処理322の第1例によって関連部分式として生成された単項式の数であり、比較例における数は、従来のテンプレート法によって生成されたテンプレート多項式に含まれる単項式(冪積)の数である。表2において、「演算時間(実施例)」は、実施形態において不変条件生成に要した演算時間であり、「演算時間(比較例)」は、比較例において不変条件生成に要した演算時間であり、単位はいずれも「秒」である。

【0113】
表2の「単項式の数の比」が示すように、実施形態に係る処理(実施例)では、大部分のケースにおいて、比較例に比べて単項式の数を削減できている。表2の「演算時間(実施例)」及び「演算時間(比較例)」が示すように、大部分のケースにおいて、比較例に比べて、不変条件生成に要する演算時間を短縮できている。なお、"MARKUS"及び指定部分式がsである場合の"TRIG"においては、比較例の方が演算時間が短くなっている。これは、実施例においては第2処理322にある程度の時間を要するため、比較例において生成される単項式数が少ないと、比較例の方が演算時間が短くなるからである。

【0114】
表1の「λ」及び「Generated invariants」が示すように、実施形態の第2処理322によって生成された不変条件は、固有値λが1でないλ-不変条件を含んでいる。

【0115】
【表3】
JP2017138679A_000016t.gif

【0116】
表3は、実施形態の不変条件生成モジュール320による不変条件生成の演算時間が、短縮されていることを示す実験結果である。表3において、「実験結果1」は、第2処理322として第1例を用い、第3処理323として固有ベクトル法を用いた場合の不変条件生成の演算時間を示す。「実験結果2」は、第2処理322(単項式の生成)は従来のテンプレート法で行い、第3処理322は固有ベクトル法を用いた場合の不変条件生成の演算時間を示す。「実験結果3」は、非特許文献1記載の従来のテンプレート法を用いた場合の不変条件生成の演算時間を示す。「実験結果4」は、非特許文献3記載のアルゴリズムを用いた場合の不変条件生成の演算時間を示す。

【0117】
表3は、SUMOWER1,n(上段)、SUMOWERk,n(下段)それぞれについての演算時間を示している。演算時間の単位は「秒」であり、表3に示す演算時間は、5回の実行の平均である。T/Oは、タイムアウトを示す。演算時間が600秒を超えるとタイムアウトとした。SUMOWERk,nにおいて、kは任意の値である。表3は、SUMOWER1,n及びSUMOWERk,nにおけるnを1から128にした場合の演算時間を示している。nが大きくなると、生成されるλ-不変条件の次数も大きくなる。

【0118】
実験結果1によれば、nが大きくなっても、タイムアウトせずに、λ-不変条件を生成できていることがわかる。実験結果1と実験結果2とを比較すると、単項式の数が削減されない実験結果2に比べて、実験結果1の演算時間が短くなっている。したがって、実施形態の第2処理322(次元型解析)による効果が確認できる。また、実験結果3,4に比べて、実験結果2の演算時間が短くなっている。したがって、実施形態の第3処理323(固有ベクトル法)による効果が確認できる。

【0119】
[2.5 プログラムコード製造方法]
図7は、実施形態に係る検証装置100を用いたプログラムコード製造工程を示している。プログラムコード製造工程は、ステップS41からステップS46を含んでいる。

【0120】
ステップS41は、プログラムコード(初期コード;検証対象のプログラムコード)を作成するステップである。プログラムコードは、例えば、プログラマーによって作成及び修正される。ステップS42は、検証対象のプログラムコードを、検証装置100の記憶部300が、検証対象のプログラムコードを記憶するステップである。ステップ43は、検証装置100の不変条件生成モジュール320が、検証対象のプログラムコードの不変条件を生成するステップである。ステップS44は、検証装置100が、生成された不変条件と、記憶部300に記憶されたプログラムコードと、を用いて、そのプログラムコードの形式的検証を行うステップである。ステップS45においては、検証の結果の判定、すなわち、プログラムコードが不変条件を満たしていたか否かが判定される。ステップS46は、検証の結果に基づいて、プログラムコードを修正するステップである。プログラムコードの検証・修正は、必要に応じて何度か繰り返される。

【0121】
プログラムコードの検証・修正を経て、最終的に、不変条件を満たしていると判定されたプログラムコードは、仕様等に照らして、正しいことが証明されたものとなる。したがって、より高品質のプログラムコードが得られる。

【0122】
プログラムコードの製造工程について、以下のプログラムコードを例として説明する。
【数12】
JP2017138679A_000017t.gif

【0123】
このプログラムコードは、変数sumとiの値を0に初期化し、iが自然数n0に等しくなるまでsumの値にiを加え、iを1増加させるという動作を繰り返す。プログラムコードの末尾のassert(2*sum==n0*(n0+1))は、プログラムが停止したならば、その時点で等式2* sum== n0* (n0+1)が成り立っていなければならないというプログラムの仕様を表す。

【0124】
このプログラムについて、実施形態に係る検証装置100を用いて、プログラムコードのバグを修正する方法を示す。検証装置100は、このプログラムコード中のwhileループについて、ループ不変条件として、2*sum==i*(i-1)を生成することができる。

【0125】
ループが実行されるための条件はi≠n0なので、ループを抜けた時点では、この否定i == n0が成り立っているはずである。したがって、
【数13】
JP2017138679A_000018t.gif
という条件が、任意のi、sum、非負のn0について成り立てば、このプログラムコードは仕様を満たす。この条件を、以下で条件Cと呼ぶことにする。

【0126】
しかしながらsum=0,i=1,n0 =1であるときに条件Cは満たされない。これは、n0=1であるときに、ループを抜けたときのsumとiの値がそれぞれ0,1であると、仕様が満たされないことを示している。実際に、n0=1であるときの各変数の値を考えると、sumとiの値はプログラム開始時点でそれぞれ0,0であり、ループを一回実行した時点で0,1であり、その後ループを抜けるため、このプログラムコードは仕様を満たしていない。

【0127】
n0=1のときに仕様を満たすためにはsumの値がプログラム終了時に1でなければならない。このあるべきsumの値と上記の状態遷移とを比較すると、仕様が満たされるためにはもう一回ループが実行されなければならないことが分かる。もう一回ループが実行されるためには、ループが実行されるための条件をi != n0からi != n0+1に変更しなければならないことが分かる。こうして、修正を加えられた以下のプログラムコードが得られる。
【数14】
JP2017138679A_000019t.gif

【0128】
修正されたプログラムコードが、仕様を満たすための条件C’を条件Cを得たのと同様に求める。すなわち、
【数15】
JP2017138679A_000020t.gif
という条件C’が、任意のsum,iと非負のn0について成り立てば、この修正プログラムコードは仕様を満たす。この条件は実際に成り立っているため、修正プログラムは仕様を満たす。
【符号の説明】
【0129】
100 不変条件生成装置
200 処理部
300 記憶部
310 検証用プログラム
320 不変条件生成モジュール
321 第1処理
322 第2処理
323 第3処理
330 検証対象のプログラムコード
図面
【図1】
0
【図2】
1
【図3A】
2
【図3B】
3
【図4】
4
【図5A】
5
【図5B】
6
【図6A】
7
【図6B】
8
【図7】
9