(57)【要約】  ソースコード等価性検証装置は、変更前ソースコードと変更前ソースコードを変更した変更後ソースコードとを対象に、それぞれ記号実行計算する記号実行計算部、記号実行計算部の記号実行計算結果である記号実行サマリに基づいて、変更前ソースコードと変更後ソースコードとの、同じ入力に対して同じ出力が得られることである等価性を検証するための等価性検証式を生成する等価性検証式生成部、等価性検証式生成部で生成された等価性検証式を検証する等価性検証式検証部、等価性検証式検証部における検証結果を用いて検証結果レポートを生成する検証結果生成部を有する。
2016038741.tif 000002
【特許請求の範囲】
【請求項１】
変更前ソースコードと前記変更前ソースコードを変更した変更後ソースコードとを対象に、それぞれ記号実行計算する記号実行計算部（１１３）、
前記記号実行計算部の記号実行計算結果である記号実行サマリに基づいて、前記変更前ソースコードと前記変更後ソースコードとの、同じ入力に対して同じ出力が得られることである等価性を検証するための等価性検証式を生成する等価性検証式生成部、
前記等価性検証式生成部で生成された前記等価性検証式を検証する等価性検証式検証部、および
前記等価性検証式検証部における検証結果を用いて検証結果レポートを生成する検証結果生成部を有することを特徴とするソースコード等価性検証装置。
【請求項２】
請求項１に記載のソースコード等価性検証装置において、前記等価性検証式生成部は、前記変更前ソースコードおよび前記変更後ソースコードの前記記号実行サマリを構成する各スナップショットの組合せに対する、前記変更前ソースコードと前記変更後ソースコードとで対応する出力変数間の等号制約式、前記変更前ソースコードの前記スナップショットのスナップショット制約式、および前記変更後ソースコードの前記スナップショットの前記スナップショット制約式を含むパス等価性検証式を生成することを特徴とするソースコード等価性検証装置。
【請求項３】
請求項２に記載のソースコード等価性検証装置において、前記検証結果生成部は、前記スナップショットの組合せに対して、前記変更前ソースコードおよび前記変更後ソースコードの前記スナップショットに対応するパスの経路、および、前記等価性検証式検証部による前記パスの組合せに対する検証結果が非等価であるときはその反例を表示する前記検証結果レポートを生成することを特徴とするソースコード等価性検証装置。
【請求項４】
請求項３に記載のソースコード等価性検証装置において、検証結果生成部は、複数の前記スナップショットが選択された場合に、それぞれの前記スナップショットに対応する前記パスの経路の共通部分および合併部分の一方を表示する前記検証結果レポートを生成することを特徴とするソースコード等価性検証装置。
【請求項５】
請求項２に記載のソースコード等価性検証装置において、前記等価性検証式検証部は、前記変更前ソースコードの特定のパスを通ったときと前記変更後ソースコードの特定のパスを通ったときとの間の等価性を検証するパス等価性検証式、および、前記等価性検証式を並列に検証することを特徴とするソースコード等価性検証装置。
【請求項６】
請求項５に記載のソースコード等価性検証装置において、前記等価性検証式検証部が並列に検証した、前記等価性検証式および前記パス等価性検証式の検証式の検証の終了に応じて、前記検証結果レポートを生成することを特徴とするソースコード等価性検証装置。
【請求項７】
ソースコード等価性検証装置におけるソースコード等価性検証方法であって、前記ソースコード等価性検証装置は、
変更前ソースコードと前記変更前ソースコードを変更した変更後ソースコードとを対象に記号実行計算し、
前記記号実行計算結果である記号実行サマリに基づいて、前記変更前ソースコードと前記変更後ソースコードとの、同じ入力に対して同じ出力が得られることである等価性を検証するための等価性検証式を生成し、
生成された前記等価性検証式を検証し、
前記検証結果を用いて検証結果レポートを生成することを特徴とするソースコード等価性検証方法。
【請求項８】
請求項７に記載のソースコード等価性検証方法において、前記ソースコード等価性検証装置は、は、前記変更前ソースコードおよび前記変更後ソースコードの前記記号実行サマリを構成する各スナップショットの組合せに対する、前記変更前ソースコードと前記変更後ソースコードとで対応する出力変数間の等号制約式、前記変更前ソースコードの前記スナップショットのスナップショット制約式、および前記変更後ソースコードの前記スナップショットの前記スナップショット制約式を含むパス等価性検証式を生成することを特徴とするソースコード等価性検証方法。
【請求項９】
請求項８に記載のソースコード等価性検証方法において、前記ソースコード等価性検証装置は、前記スナップショットの組合せに対して、前記変更前ソースコードおよび前記変更後ソースコードの前記スナップショットに対応するパスの経路、および、前記パスの組合せに対する検証結果が非等価であるときはその反例を表示する前記検証結果レポートを生成することを特徴とするソースコード等価性検証方法。
【請求項１０】
請求項９に記載のソースコード等価性検証方法において、前記ソースコード等価性検証装置は、複数の前記スナップショットが選択された場合に、それぞれの前記スナップショットに対応する前記パスの経路の共通部分および合併部分の一方を表示する前記検証結果レポートを生成することを特徴とするソースコード等価性検証方法。
【請求項１１】
請求項８に記載のソースコード等価性検証方法において、前記ソースコード等価性検証装置は、前記変更前ソースコードの特定のパスを通ったときと前記変更後ソースコードの特定のパスを通ったときとの間の等価性を検証するパス等価性検証式、および、前記等価性検証式を並列に検証することを特徴とするソースコード等価性検証方法。
【請求項１２】
請求項１１に記載のソースコード等価性検証方法において、前記ソースコード等価性検証装置は、並列に検証した、前記等価性検証式および前記パス等価性検証式の検証式の検証の終了に応じて、前記検証結果レポートを生成することを特徴とするソースコード等価性検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソースコードを変更した際に変更前後のソースコード間の実行内容が等価であることを検証するための装置、および、検証方法に関する。
【背景技術】
【０００２】
ソースコードの等価性を検証するための手法として、特許文献１に記載の技術がある。特許文献１では、ソースコード比較によって差異が生じている部分にテストを実施し、その結果を比較する手法が開示されている。【０００３】
また、非特許文献１では、記号実行を用いて実行内容が維持されていることを検証する手法が開示されている。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】米国特許出願公開第２００７／００３３５７６号公報
【非特許文献】
【０００５】
【非特許文献１】S. Person, M. B. Dwyer, S. Elbaum, C. S. Pasareanu, "Differential Symbolic Execution", Proc. of ACM SIGSOFT International Symposium on the Foundations of Software Engineering 2008, pp. 226-237, USA, 2008
【発明の概要】
【発明が解決しようとする課題】
【０００６】
近年、情報処理社会が進展することにより、ソフトウェアシステムが一般社会に浸透し、ソフトウェアに求められる信頼性が非常に高度なものになってきている。一方で、ソフトウェアは、長年にわたる差分・派生開発によって複雑化および大規模化の一途をたどり、ソフトウェアの拡張しやすさや理解しやすさといった保守性の低下が問題となっている。【０００７】
ソフトウェアの保守性を向上させる方法としてリファクタリングや言語リプレースがある。リファクタリングは、ソフトウェアの実行内容を変えずに、内部構造を変更することにより、ソフトウェアの設計品質を改善する手法の総称である。言語リプレースは、保守性の低いプログラミング言語を用いて開発されたソフトウェアに対して、そのソフトウェアと同じ機能を保守性の高い他のプログラミング言語を用いて作り直すことにより置き換えることである。【０００８】
このリファクタリングや言語リプレースの手法は、複雑化および大規模化の一途をたどるソフトウェアの保守性を確保するために有望な技術である。しかし、ソフトウェアのソースコードの変更や作り直しの際に、対象となっているソースコードの実行内容を変えてしまうと、新たに不具合を混入してしまう可能性がある。そのため、ソフトウェア開発者が、リファクタリングや言語リプレースが原因で正しく動作していたソフトウェアに不具合が混入することをおそれ、それらを行わない判断が有り得る。ソフトウェアの保守段階において、リファクタリングや言語リプレースを積極的に行うためには、ソースコードの変更前後で、両者のソースコードの実行内容の変化が無いことを検証する手法が求められる。【０００９】
本明細書中において、変更前と変更後の二つのソースコードの外的な実行内容が同じであること、すなわち、任意の同じ入力に対して、実行時に同じ出力が得られることを、両ソースコードが「等価」であると定義する。また、変更前のソースコードと変更後のソースコードが、等価であるかどうかを検証することを「等価性検証」ということにする。【００１０】
変更前のソースコードと変更後のソースコードが等価であることを検証する手法に求められる条件としては以下のような条件がある。
（１）一つの条件は、その作業の大部分が自動化されており、人手による作業が少ないことである。従来、ソースコードの等価性は、人手によるレビューやテストによって検証されていた。これをツールによる自動的な検証を実現にすることにより、検証工数が削減され、リファクタリング等が促進される。
（２）他の条件は、等価性検証手法により非等価であると判断された場合に、その根拠となる情報や修正すべき箇所に関する情報を開発者に提供することである。開発者に分かり易く修正すべき箇所の情報を提供することにおり、開発者による修正が容易となり、開発期間や工数の短縮につながる。
（３）さらに他の条件は、ツールによる検証時間が短い、もしくは、並列化により短縮すること可能であることである。検証作業が自動化されたとしても、その検証に長時間の計算が必要であれば、検証後に修正して再度検証するというサイクルを繰り返すことが困難となる。そのため、計算量が少ない検証手法を用いるか、計算量が多くても並列化により計算時間を短縮できる検証手法が必要となる。【００１１】
特許文献１による手法は、テストを必要としており、（１）の条件を満たすことができない。また、非特許文献１による手法は、非等価な場合に等価とするために必要な修正をすべき箇所の情報を得ることができず、（２）の条件を満たすことができない。さらに、非特許文献１では、等価性を検証するための論理式を生成し、ソルバを用いて検証しているが、この検証式を並列に実行することができず（３）の条件を満たすことができない。【００１２】
そこで、記号実行を用いたソースコード等価性検証装置において、検証結果が非等価である場合に、開発者が等価にするために必要なソースコード上の修正箇所に関する情報を提供する技術と、等価性検証を並列に実行する技術とが必要とされる。
【課題を解決するための手段】
【００１３】
開示するソースコード等価性検証装置は、変更前ソースコードと変更前ソースコードを変更した変更後ソースコードとを対象に、それぞれ記号実行計算する記号実行計算部、記号実行計算部の記号実行計算結果である記号実行サマリに基づいて、変更前ソースコードと変更後ソースコードとの、同じ入力に対して同じ出力が得られることである等価性を検証するための等価性検証式を生成する等価性検証式生成部、等価性検証式生成部で生成された等価性検証式を検証する等価性検証式検証部、等価性検証式検証部における検証結果を用いて検証結果レポートを生成する検証結果生成部を有する。
【発明の効果】
【００１４】
開示するソースコード等価性検証装置によれば、等価性を検証するソースコード上の制御フローのパス毎に等価性を検証するため、個々の検証を並列化することにより、検証時間の短縮を実現することができる。【００１５】
また、制御フローのパス毎の等価性検証結果を用いることにより、等価にするための修正を行う際に、ソースコード上で調査が必要な範囲を絞り込むことが可能となり、開発者による修正の時間と工数を削減することができる。
【図面の簡単な説明】
【００１６】
【図１】ソースコード等価性検証に用いる変更前ソースコードの例である。
【図２】ソースコード解析の結果得られる構造グラフの例を示す図である。
【図３】記号実行を計算することにより得られる実行木を示す図である。
【図４】ソースコード等価性検証装置のハードウェア構成図である。
【図５】ソースコード等価性検証装置のソフトウェア構成図である。
【図６】ソースコード等価性検証装置の機能構成図である。
【図７】ソースコード等価性検証装置の制御部と記憶部のデータフローを示した図である。
【図８】ソースコード等価性検証の処理フローチャートである。
【図９】ソースコード等価性検証に用いる、等価となるような変更を実施した変更後ソースコードの例である。
【図１０】記号実行を計算することにより得られる実行木を示す図である。
【図１１】等価性検証装置が出力する検証結果レポートの例を示す図である。
【図１２】ソースコード等価性検証に用いる、非等価となるような変更を実施した変更後ソースコードの例である。
【図１３】記号実行を計算することにより得られる実行木を示す図である。
【図１４】等価性検証装置が出力する検証結果レポートの例を示す図である。
【図１５】等価性検証式生成部の処理フローチャートである。
【図１６】等価性検証式検証部における各パス等価性検証式の検証結果の例である。
【図１７】等価性検証装置が出力する検証結果レポートの例を示す図である。
【図１８】複数のスナップショットを選択した時の表示例を示す図である。
【図１９】ソースコード等価性検証装置における等価性検証式検証処理部の処理フローチャートである。
【発明を実施するための形態】
【００１７】
本実施形態の前提となる技術である記号実行について説明する。記号実行とは、ソースコードの検証に際し、ソースコード中に用いられている変数（入力変数、グローバル変数等）に具体的な値を代入しつつソースコードを実行する代わりに、記号を用いて実行し、ソースコードの実行過程における変数の状態（以下、変数状態とも称する。）とソースコード中の当該制御パスを経るための条件式（以下、パス制約とも称する。）との組み合わせ（以下、スナップショットとも称する。）を用いてソースコードが示すソフトウェアの入出力関係を求める技術である。
【００１８】
記号実行によれば、ソースコードが取り得るすべてのパスを網羅してソースコードを検証することができる。以下、図１のＣ言語で記述されたソースコードＣ１００について情報処理装置を用いて記号実行を行う場合を例として説明する。
【００１９】
記号実行において、情報処理装置は、ソースコードＣ１００を対象に、コンパイルと同様の字句分析や構文分析を行うことにより、図２に示す構造グラフＮ１００を生成する。構造グラフＮ１００は、ソースコードの抽象構文木（構文木から、言語の意味に関係ない情報を取り除き、意味に関係ある情報のみを取り出した（抽象した）木構造のデータ構造）の各ノード間の制御フローを示しており、実線矢印は条件の付かない制御フロー、破線矢印は条件付き制御フローを表している。
【００２０】
図２に示す関数ｆｏｏの構造グラフＮ１００では、関数のエントリーポイントに対応するノードＮ１から始まり、関数の出口であるｒｅｔｕｒｎ文に対応するノードＮ５に終わる各制御フローが図示されている。また、ｉｆ文に対応するノードＮ２からは複数の条件付き制御フローがあり、ｉｆ文の条件の成立／不成立に応じて異なる制御フローがあることを示している。
【００２１】
構造グラフＮ１００の生成にあたって、情報処理装置は、各ノードに対応するソースコードＣ１００上の位置情報を付与する。図２に示す例においては、情報処理装置は、ソースコードＣ１００中の行番号を位置情報として付与しており、例えばソースコードＣ１００の４行目のｉｆ文に対応して、ノードＮ２にはＬ４という位置情報を付与している。
【００２２】
情報処理装置は、構造グラフＮ１００に基づき、図３に示す実行木Ｓ１００を生成する。実行木Ｓ１００の各ノードは、前述したパス制約（上欄）と変数状態（中欄）との組み合わせで表され、さらに、ソースコード上で経由した位置を表わす位置情報（下欄）が表されている。実行木Ｓ１００の根ノード（ルートノード）Ｓ１０１は、ソースコードの実行の初期状態に対応する。情報処理装置は、ソースコードの実行に伴って変数が更新される度に実行木Ｓ１００に新たなノードを追加していく。
【００２３】
実行木Ｓ１００の生成に際し、情報処理装置は、関数ｆｏｏの入力変数となる変数の値に対応する記号変数を割り当てる。入力変数となる変数の値とは、関数外部から与えられて、当該関数の動作に影響を与える変数の値であり、関数の引数や関数内でアクセスするグローバル変数を含む。
【００２４】
例示するソースコードＣ１００においては、関数の引数ａとグローバル変数ｇが入力変数となる。本例では、情報処理装置は、変数ａとｇに「α」と「γ」を記号変数として割り当てている。
【００２５】
情報処理装置は、構造グラフＮ１００のノードＮ１に基づき、実行木Ｓ１００に根ノードＳ１０１を生成する。本例では、情報処理装置は、根ノードＳ１０１のパス制約（上欄）Ｓ１０１ａに、「制約無し」を示す「ｎｏ  ｃｏｎｄｉｔｉｏｎ」を設定し、変数状態（中欄）Ｓ１０１ｂに、入力変数ａとｇの値がそれぞれ割り当てられた記号変数αとγであることを示す「ａ＝α，ｇ＝γ」を設定している。また、位置情報（下欄）Ｓ１０１ｃに、ノードＮ１から取得した位置情報Ｌ２を設定する。
【００２６】
情報処理装置は、構造グラフＮ１００のノードＮ１の制御フロー上の次ノードＮ２に基づき処理を実行する。ノードＮ２は２つの条件付き制御フローＮ２１とＮ２２を持つ条件分岐ノードであり、情報処理装置は、条件付き制御フローＮ２１に対応する子ノードＳ１０２を、条件付き制御フローＮ２２に対応する子ノードＳ１０５を、それぞれノードＳ１０１の子ノードとして生成する。
【００２７】
ノードＮ２における条件式は「ｇ＝＝０」であり、Ｓ１０１ｂにおける変数ｇの変数状態はγであるため、条件付き制御フローＮ２１における分岐条件は「γ＝０」と表現できる。そのため、ノードＳ１０２のパス制約（上欄）は、Ｓ１０１ａにおけるパス制約「制約無し」と合わせて「γ＝０」と設定される。
【００２８】
ノードＳ１０２の変数状態（中欄）は、ｉｆ文によって変数状態が変化しないため親ノードＳ１０１の変数状態Ｓ１０１ｂと同一に設定される。また、位置情報（下欄）は、親ノードＳ１０１の位置情報Ｓ１０１ｃに加えて、ノードＮ２の位置情報（Ｌ４）が追加され「Ｌ２，４」となり、ソースコードの２行目と４行目を経由してきたことを意味する。
【００２９】
条件付き制御フローＮ２２における分岐条件は、制御フローＮ２２がｉｆ文の条件が成立しなかった場合に対応するフローであることから、「¬（γ＝０）」と表現できる。そのため、ノードＳ１０５のパス制約（上欄）は、Ｓ１０１ａにおけるパス制約「制約無し」と合わせて「¬（γ＝０）」と設定される。
【００３０】
ノードＳ１０５における変数状態（中欄）は、ｉｆ文によって変数状態が変化しないため親ノードＳ１０１の変数状態Ｓ１０１ｂと同一に設定される。また、位置情報（下欄）は、親ノードＳ１０１の位置情報Ｓ１０１ｃに加えて、ノードＮ２の位置情報（Ｌ４）が追加され「Ｌ２，４」となる。
【００３１】
情報処理装置は、ノードＮ２の制御フローＮ２１上の次ノードであるＮ３に基づき処理を実行する。情報処理装置は、ノードＮ３に対応する実行木Ｓ１００におけるノードとしてＳ１０２の子ノードＳ１０３を生成する。
【００３２】
ノードＳ１０３においては、条件分岐が無いため、パス制約（上欄）はＳ１０２と同一に設定する。また、ノードＮ３において変数ｒに値０を代入しているため変数状態（中欄）に「ｒ＝０」を追加する。位置情報（下欄）にはＳ１０２における位置情報にノードＮ３の位置情報である「Ｌ５」を追加する。
【００３３】
情報処理装置は、ノードＮ３の制御フロー上の次ノードであるＮ５に基づき処理を実行する。ノードＮ５に対応する実行木Ｓ１００におけるノードとしてＳ１０３の子ノードＳ１０４を生成する。ノードＮ５は変数ｒを返り値とするｒｅｔｕｒｎ文に対応しているため、変数状態（中欄）には、返り値を表わすこととする変数Ｒに対して変数ｒの現在の値である０を割り当てた「Ｒ＝０」を追加する。ｒｅｔｕｒｎ文により関数の実行は終わるため、情報処理装置は、実行木Ｓ１００における、この枝の生成を終了し、まだ生成の終わっていない枝の生成へと移行する。
【００３４】
情報処理装置は、Ｎ２の制御フローＮ２２上の次ノードであるＮ４に基づき処理を実行する。ノードＮ４は２つの条件付き制御フローＮ４１とＮ４２を持つ条件分岐ノードであり、情報処理装置は、条件付き制御フローＮ４１に対応する子ノードＳ１０６を、条件付き制御フローＮ４２に対応する子ノードＳ１１０を、それぞれノードＳ１０５の下に生成する。
【００３５】
ノードＮ４におけるｉｆ文の条件式は「ａ＞０」であり、変数状態よりａに対応する値はαであるため、条件付き制御フローＮ４１における分岐条件は「α＞０」と表現される。そのため、Ｓ１０６におけるパス制約（上欄）はＳ１０５におけるパス制約「¬（γ＝０）」と「α＞０」との論理積である「¬（γ＝０）∧（α＞０）」を設定する。
【００３６】
以下、情報処理装置は、各枝に対して、すべての枝の生成が終了するまでに上記の処理を繰り返す。
【００３７】
ノードＮ６に対する処理では、情報処理装置は、ノードＳ１０７の子ノードＳ１０８を生成している。ノードＮ６では変数ｇの値をｇ−１に更新している。この時、変数ｇに対応する値はＳ１０７の変数状態（中欄）からγであると分かる。そこで、子ノードＳ１０８では、情報処理装置は、変数ｇに対する変数状態（中欄）を「ｇ＝γ―1」に更新する。このように、記号変数を含む計算に対しては具体的な値ではなく式のままの形で変数状態を保持する。
【００３８】
情報処理装置は、上記の処理によって、最終的に図２に示す構造グラフＮ１００から図３に示すような実行木Ｓ１００を得る。記号実行においては取り得る全ての制御フローが網羅されるように条件分岐に応じた子ノードが実行木に生成される。
【００３９】
実行木における葉ノードは、ソースコードの入力値に対する条件（パス制約）と、出力変数の状態（変数状態）の組の集合を求めることであるということができる。以下の説明において、記号実行が終了した時点における実行木の葉ノードを「スナップショット」と称し、スナップショットの集合ことを「記号実行サマリ」と称する。ただし、変数状態に含まれる変数のうち、ローカル変数（関数の引数を含む）は関数の実行完了時点で破棄されるため、スナップショットおよび記号実行サマリからローカル変数の変数状態は除外することとする。
【００４０】
実行木Ｓ１００における葉ノードはＳ１０４、Ｓ１０９，Ｓ１１３の３ノードであり、これらはそれぞれスナップショットとなり、これらの集合が記号実行サマリＳ１２０となる。ただし、ローカル変数である変数ｒおよびaの変数状態は除外する。
【００４１】
本例では、Ｃ言語で記述されたソースコードを用いて記号実行を説明したが、Ｃ言語に限定されず他のプログラミング言語を用いて記述されたソースコードに対しても同様に実施可能である。
【実施例１】
【００４２】
以下、図４から図１４を用いて、実施例１のソースコード等価性検証装置１０００の構成と処理について説明する。【００４３】
図４は、本実施例のソースコード等価性検証装置のハードウェア構成である。本実施例のソースコード等価性検証装置は、例えば、図４に示されるような一般的なコンピュータで実現される。ソースコード等価性検証装置１０００は、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）１０１、主記憶装置１０２、ネットワークＩ／Ｆ１０３、グラフィックＩ／Ｆ１０４、入出力Ｉ／Ｆ１０５、補助記憶装置Ｉ／Ｆ１０６が、バスにより結合された形態になっている。【００４４】
ＣＰＵ１０１は、ソースコード等価性検証装置１０００の各部を制御し、主記憶装置１０２にソースコード等価性検証プログラム２００をロードして実行する。【００４５】
主記憶装置１０２は、通常、ＲＡＭなどの揮発メモリで構成され、ＣＰＵ１０１が実行するプログラム、参照するデータが補助記憶装置などからロードされて、記憶される。【００４６】
ネットワークＩ／Ｆ１０３は、外部ネットワーク１５０と接続するためのインタフェースである。【００４７】
グラフィックＩ／Ｆ１０４は、ＬＣＤ（Ｌｉｑｕｉｄ  Ｃｒｙｓｔａｌ  Ｄｉｓｐｌａｙ）などの表示装置１２０を接続するためのインタフェースである。【００４８】
入出力Ｉ／Ｆ１０５は、入出力装置を接続するためのインタフェースである。図４の例では、キーボード１３１とポインティングデバイスのマウス１３２が接続されている。【００４９】
補助記憶装置Ｉ／Ｆ１０６は、ＨＤＤ（Ｈａｒｄ  Ｄｉｓｋ  Ｄｒｉｖｅ）１４１やＤＶＤ（Ｄｉｇｉｔａｌ  Ｖｅｒｓａｔｉｌｅ  Ｄｉｓｋ）ドライブ装置１４２などの補助記憶装置を接続するためのインタフェースである。【００５０】
ＨＤＤ１４１は、大容量の記憶容量を有しており、本実施例の処理を実行するためのソースコード等価性検証プログラム２００が格納されている。【００５１】
ＤＶＤドライブ装置１４２は、ＤＶＤやＣＤなどの光学ディスクにデータを書き込んだり、光学ディスクからデータを読み込んだりする装置であり、ソースコード等価性検証プログラム２００は、例えば、ＣＤ−ＲＯＭにより提供されたものをインストールすることができる。【００５２】
本実施例のテストデータ生成装置１０００は、上記のようなコンピュータに、ソースコード等価性検証プログラム２００をインストールして、各機能を実行するものである。【００５３】
図５は、本実施例のソースコード等価性検証装置のソフトウェア構成である。ソースコード等価性検証装置１０００で実行するソースコード等価性検証プログラム２００は、ソースコード読込みモジュール２０１、構造グラフ生成モジュール２０２、記号実行計算モジュール２０３、等価性検証式生成モジュール２０４、等価性検証式検証モジュール２０５、および検証結果表示モジュール２０６を含む。【００５４】
なお、プログラム等価性検証プログラム２００は、ＯＳ（Ｏｐｅｒａｔｉｎｇ  Ｓｙｓｔｅｍ）上で動作するアプリケーションソフトウェアであり、ソースコード等価性検証装置のソフトウェア構成として、ＯＳやライブラリプログラムも含むが図５では、省略している。【００５５】
ソースコード読込みモジュール２０１は、検証対象の変更前ソースコードと変更後ソースコードとをＨＤＤや他の計算機から読込み、記憶部に格納するモジュールである。【００５６】
構造グラフ生成モジュール２０２は、ソースコード（たとえば、前述したＣ１００）の字句解析・構文解析を行い、制御フローを抽出することにより、構造グラフ（たとえば、前述したＮ１００）を生成するモジュールである。【００５７】
記号実行計算モジュール２０３は、構造グラフ生成モジュール２０２が生成した構造グラフに基づき、記号実行を行って実行木（たとえば、前述したＳ１００）を計算し、その葉ノードを集めた記号実行サマリ（たとえば、前述したＳ１２０）を生成するモジュールである。【００５８】
等価性検証式生成モジュール２０４は、記号実行計算モジュール２０３が生成した、変更前ソースコードの記号実行サマリおよび変更後ソースコードの記号実行サマリから、両者の等価性を判定するための検証論理式である等価性検証式を生成するモジュールである。【００５９】
等価性検証式検証モジュール２０５は、等価性検証式生成モジュール２０４が生成した等価性検証式をＳＡＴ（ＳＡＴｉｓｆｉａｂｉｌｉｔｙ）ソルバやＳＭＴ（Ｓａｔｉｓｆｉａｂｉｌｉｔｙ  Ｍｏｄｕｌｏ  Ｔｈｅｏｒｉｅｓ）ソルバを用いてグラフ理論における充足可能性問題として解くモジュールである。【００６０】
検証結果生成モジュール２０６は、等価性検証式検証モジュール２０５が出力した検証結果や記号実行サマリ、ソースコードの情報を用いて検証結果レポートを生成し、表示または通知するモジュールである。【００６１】
図６は、ソースコード等価性検証装置１０００の機能構成図を示す。制御部１１０は、図４のＣＰＵ１０１、主記憶装置１０２により実現し、記憶部１４０は主に図４のＨＤＤ１４１により実現するが、主記憶装置１０２を含めることもある。入力装置１３０は、図４の入出力Ｉ／Ｆ１０５、キーボード１３１、マウス１３２などを含み、さらに補助記憶装置Ｉ／Ｆ１０６を介してＤＶＤドライブ装置１４２から読込む構成を含めてもよい。出力装置１２１は、グラフィックＩ／Ｆ１０４、表示装置１２０などを含み、さらに補助記憶装置Ｉ／Ｆ１０６を介してＤＶＤドライブ装置１４２へ書き込む構成を含めてもよい。通信部１０３は、図４のネットワークＩ／Ｆ１０３を表わすが、ネットワーク１５０を介して例えば外部計算機１６０と接続されている。図６の制御部１１０および記憶部１４０の詳細は、図７を用いて説明する。【００６２】
図７は、ソースコード等価性検証装置１０００の制御部１１０および記憶部１４０内の構成およびデータフローを示す。ソースコード入力部１１１は、検証対象とする変更前ソースコード３０１および変更後ソースコード３０２を読込み、変更前／後ソースコード記憶領域２０１にそれぞれ格納する。【００６３】
本実施例では、変更前ソースコード３０１と変更後ソースコード３０２がＣ言語で記述された例を用いて説明しているが、他の言語にも対応した構造グラフ生成部１１２および記号実行計算部１１３を用いることにより、他のプログラミング言語で記述されたソースコードを用いることも可能である。また、変更前ソースコード３０１と変更後ソースコード３０２とで異なるプログラミング言語を用いても良い。【００６４】
構造グラフ生成部１１２は、変更前／後ソースコード記憶領域２０１に格納されている、変更前ソースコードおよび変更後ソースコードのそれぞれのソースコード解析を実行し、その解析結果である変更前構造グラフおよび変更後構造グラフを変更前／後構造グラフ記憶領域２０２に格納する。【００６５】
記号実行計算部１１３は、変更後構造グラフを変更前／後構造グラフ記憶領域２０２に格納されている、変更前／後構造グラフのそれぞれを記号実行し、その計算結果（実行結果）である記号実行サマリを変更前／後記号実行結果記憶領域２０３に格納する。【００６６】
等価性検証式生成部１１４は、変更前／後記号実行結果記憶領域２０３に格納されている、変更前／後記号実行サマリから、変更前および変更後の両者の等価性を検証するための論理式である等価性検証式を生成し、等価性検証式記憶領域２０４に格納する。【００６７】
等価性検証式検証部１１５は、等価性検証式記憶領域２０４に格納されている等価性検証式の検証を実行し、検証式の検証結果を等価性検証式結果記憶領域２０５に格納する。【００６８】
検証結果生成部１１６は、等価性検証式の検証結果、記号実行サマリ、およびソースコードに関する情報を用いて、検証結果レポート３１０を生成し、検証結果記憶領域２０６に格納するとともに出力装置１２１を用いて画面に表示する、または、通信部１０３を用いて外部計算機１６０に送信する。【００６９】
以上の説明から明らかなように、制御部１１０に含まれる各部の動作は、図５に示したソースコード等価性検証プログラムの各モジュールをソースコード等価性検証装置１０００が実行することによって実現される。【００７０】
図８は、ソースコード等価性検証の処理フローチャートである。変更前ソースコードとして図１に示す変更前ソースコードＣ１００を、変更後ソースコードとしてＣ１００と等価に変更した図９に示す変更後ソースコードＣ２００を入力した場合を例として説明する。【００７１】
ソースコード入力部１１１は、検証対象とする変更前ソースコード３０１を読込み、変更前／後ソースコード記憶領域２０１にそれぞれ格納する。（Ｐ１１０）。構造グラフ生成部１１２は、変更前／後ソースコード記憶領域２０１に格納されている変更前ソースコードのソースコード解析を実行し、その解析結果である変更前構造グラフを生成し、変更前／後構造グラフ記憶領域２０２に格納する（Ｐ１２０）。記号実行計算部１１３は、変更前／後構造グラフ記憶領域２０２に格納されている変更前構造グラフに対して記号実行し、その実行結果を変更前記号実行サマリとして生成し、変更前／後記号実行結果記憶領域２０３に格納する（Ｐ１３０）。【００７２】
変更後ソースコードに対しても同様に、ソースコード入力部１１１の処理（Ｐ１１１）、構造グラフ生成部１１２の処理（Ｐ１２1）、および記号実行計算部１１３の処理（Ｐ１３１）を実行し、変更後記号実行サマリを変更前／後記号実行結果記憶領域２０３に格納する。【００７３】
変更前ソースコードに対する処理ステップＰ１１０、Ｐ１２０、Ｐ１３０と、変更後ソースコードに対する処理ステップＰ１１１、Ｐ１２１、Ｐ１３１は、独立に実行することができるため、両者を並列に処理しても良い。【００７４】
また、以前に同じ内容のソースコードに対して処理を実行した場合には、変更前／後記号実行結果記憶領域２０３に格納されている以前の処理結果を再利用することにより、構造グラフ生成と記号実行計算を省略することができる。【００７５】
等価性検証式生成部１１４は、変更前ソースコードの記号実行サマリと変更後ソースコードの記号実行サマリを用いて等価性検証式を生成する（Ｐ１４０）。図９は、変更前ソースコードＣ１００から変更した変更後ソースコードＣ２００である。図１０は、変更後ソースコードＣ２００から生成した記号実行サマリＳ２２０である。図１に示す変更前ソースコードＣ１００から生成した図３に示す記号実行サマリＳ１２０と、図９に示す変更後ソースコードＣ２００から生成した図１０に示す記号実行サマリＳ２２０とを用いて、等価性検証式の生成について、具体的に説明する。【００７６】
記号実行サマリの各スナップショットに対して、パス制約と各変数状態の等号条件との連言を取ることによりスナップショット制約式を生成する。【００７７】
例えば、スナップショットＳ１０４、Ｓ１０９、Ｓ１１３に対しては、それぞれ（γ＝０）∧（ｇ＝γ）∧（Ｒ＝０）、¬（γ＝０）∧（α＞０）∧（ｇ＝γ−１）∧（Ｒ＝α）、¬（γ＝０）∧¬（α＞０）∧（ｇ＝γ−１）∧（Ｒ＝―α）という制約式が生成される。この際、前述のようにローカル変数である変数ｒおよび変数ａに対する変数状態の等号制約は除外される。【００７８】
次に、各スナップショット制約式の選言を取ることにより、記号実行サマリ制約式を生成する。たとえば、記号実行サマリＳ１２０に対する記号実行サマリ制約式は、{（γ＝０）∧（ｇ＝γ）∧（Ｒ＝０）}∨{¬（γ＝０）∧（α＞０）∧（ｇ＝γ−１）∧（Ｒ＝α）}∨{¬（γ＝０）∧¬（α＞０）∧（ｇ＝γ−１）∧（Ｒ＝―α）}となる。【００７９】
変更後ソースコードから生成された変更後記号実行サマリＳ２２０に対しても同様にして、記号実行サマリ制約式{（γ＝０）∧（ｇ’＝γ）∧（Ｒ’＝０）}∨{¬（γ＝０）∧（α＜０）∧（ｇ’＝γ−１）∧（Ｒ’＝−α）}∨{¬（γ＝０）∧¬（α＜０）∧（ｇ’＝γ−１）∧（Ｒ’＝α）}と求まる。ただし、変更後記号実行サマリ制約式中の出力変数ｇとＲに対しては、変更前記号実行サマリ制約式中の変数名との衝突を回避するため、それぞれｇ’とＲ’に置換している。【００８０】
変更前ソースコードと変更後ソースコードが等価である時、任意の入力変数に対して出力変数が等しくなるため、対応する出力変数間の等号制約の連言が常に成立する。そこで、本式の否定と変更前記号実行サマリ制約式と変更後記号実行サマリ制約式との連言を取り、これを等価性検証式とし、等価性検証式記憶領域２０４に格納する。【００８１】
この等価性検証式が充足不可能である場合、任意の入力変数に対して出力変数が等しいことを意味するため、両ソースコードが等価であると判定される。また、充足可能な場合には、出力変数が異なるケースがあることを意味するため、非等価であると判定される。【００８２】
本例では（Ｒ＝Ｒ’）∧（ｇ＝ｇ’）の否定と、変更前記号実行サマリ制約式と、変更後記号実行サマリ制約式との連言である、¬（（Ｒ＝Ｒ’）∧（ｇ＝ｇ’））∧（（γ＝０）∧（ｇ＝γ）∧（Ｒ＝０）∨¬（γ＝０）∧（α＞０）∧（ｇ＝γ−１）∧（Ｒ＝α）∨¬（γ＝０）∧¬（α＞０）∧（ｇ＝γ−１）∧（Ｒ＝―α））∧（（γ＝０）∧（ｇ’＝γ）∧（Ｒ’＝０）∨¬（γ＝０）∧（α＜０）∧（ｇ’＝γ−１）∧（Ｒ’＝−α）∨¬（γ＝０）∧¬（α＜０）∧（ｇ’＝γ−１）∧（Ｒ’＝α））が等価性検証式である。【００８３】
等価性検証式検証部１１５は、ＳＡＴソルバやＳＭＴソルバ等を用いて、等価性検証式生成部１１４が生成した等価性検証式の充足可能性を判定する（Ｐ１５０）。等価性検証式検証部１１５は、等価性検証式の充足可能か不可能かの判定結果と、充足可能な場合にはソルバが出力する充足するような変数の値の例である反例とを検証結果として等価性検証式検証結果記憶領域２０５に格納する。本例では、等価性検証式が充足不可能と判定されるため、充足不可能と格納される。【００８４】
検証結果生成部１１６は、等価性検証式検証部１１５による検証結果に基づき、たとえば、図１１に示すような検証結果レポート５００を生成する（Ｐ１６０）。検証結果レポート５００には、検証結果表示５１０として、等価性検証式検証結果が充足不可能な場合には「等価」と、充足可能な場合には「非等価」と表示される。本例では、等価性検証式が充足不可能と格納されているため検証結果５１０は「等価」と表示されている。【００８５】
また、検証結果レポート５００は、変更前／後ソースコード記憶領域２０１に格納されているソースコードを用いて、変更前ソースコード５２１および変更後ソースコード５２２の表示を含んでも良い。さらに、検証結果レポート５００は、変更前／後記号実行結果記憶領域２０３に格納されている記号実行サマリ情報を用いて、変更前記号実行サマリ５３１および変更後記号実行サマリ５３２の表示を含んでも良い。図１１における記号実行サマリ表示５３１および５３２においては、スナップショットごとにそのパス制約と変数状態とを一行で表示している。【００８６】
次に、図８に示すソースコード等価性検証の処理に関して、変更前ソースコードとして図１に示す変更前ソースコードＣ１００を、Ｃ１００と非等価な変更である変更後ソースコードとして図１２に示す変更後ソースコードＣ３００を入力した場合を例として説明する。【００８７】
制御部１１０の各処理は上述の通りであり、記号実行計算部１１３の処理（Ｐ１３１）により、変更後ソースコードＣ３００からは図１３に示すような実行木Ｓ３００および記号実行サマリＳ３２０が生成される。【００８８】
記号実行サマリＳ３２０に対応する記号実行サマリ制約式は（γ＝０）∧（ｇ’＝γ）∧（Ｒ’＝０）∨¬（γ＝０）∧（α＜０）∧（ｇ’＝γ＋１）∧（Ｒ’＝−α）∨¬（γ＝０）∧¬（α＜０）∧（ｇ’＝γ＋１）∧（Ｒ’＝α）と求まる。【００８９】
そのため、等価性検証式生成処理ステップＰ１４０が生成する等価性検証式は、¬（（Ｒ＝Ｒ’）∧（ｇ＝ｇ’））∧（（γ＝０）∧（ｇ＝γ）∧（Ｒ＝０）∨¬（γ＝０）∧（α＞０）∧（ｇ＝γ−１）∧（Ｒ＝α）∨¬（γ＝０）∧¬（α＞０）∧（ｇ＝γ−１）∧（Ｒ＝―α））∧（（γ＝０）∧（ｇ’＝γ）∧（Ｒ’＝０）∨¬（γ＝０）∧（α＜０）∧（ｇ’＝γ＋１）∧（Ｒ’＝−α）∨¬（γ＝０）∧¬（α＜０）∧（ｇ’＝γ＋１）∧（Ｒ’＝α））となる。【００９０】
価性検証式検証部１１５は、上記の等価性検証式の充足可能性をＳＡＴソルバ等により判定することにより、充足可能という判定と、例えばα＝１、γ＝１、Ｒ＝１、ｇ＝０、Ｒ’＝１、ｇ’＝２という反例が得られるので、それらを検証結果として格納する。【００９１】
検証結果生成部１１６は、たとえば図１４に示すような検証結果レポート５５０を生成する。【００９２】
検証結果レポート５５０には、等価性検証式検証結果が充足可能であるため検証結果表示５６０として「非等価」が表示される。また、変更前ソースコード５７１および変更後ソースコード５７２の表示や、変更前記号実行サマリ５８１および変更後記号実行サマリ５８２の表示を含んでも良い。【００９３】
さらに、検証結果レポート５５０は、等価性検証式検証結果記憶領域２０５に格納されている反例情報を用いて、非等価となるような反例情報５９０の表示を含んでも良い。【００９４】
反例情報５９０では、反例に対して、入力変数、変更前ソースコードの出力変数、変更後ソースコードの出力変数に分類し、反例として求められた値を表示している。変更前出力変数と変更後出力変数で値が異なる変数に対しては、下線を付す等により強調表示させても良い。この表示により、開発者は具体的に非等価となる入力変数の値、および、その時の変更前、変更後それぞれの出力変数の値を知ること可能となる。
【実施例２】
【００９５】
図１５から図１８を用いて、実施例２のソースコード等価性検証装置の処理の具体例について説明する。本実施例では、変更前ソースコードの特定のパスを通ったときと変更後ソースコードの特定のパスを通ったときとの間の等価性（パス等価性と呼ぶ）を、すべてのパスの組合せに対して検証することにより等価性検証を実現する。【００９６】
変更前ソースコードとして図１に示す変更前ソースコードＣ１００を、Ｃ１００と非等価な変更である変更後ソースコードとして図１２に示す変更後ソースコードＣ３００を入力した場合を例として説明する。【００９７】
本実施例では、ソースコード入力部１１１、構造グラフ生成部１１２、および記号実行計算部１１３の各処理は、実施例1と同一であり、その説明を省略する。【００９８】
図１５は、本実施例における、等価性検証式生成部１１４の処理フローチャートである。等価性検証式生成部１１４は、変更前／後記号実行結果記憶領域２０３から変更前ソースコードの記号実行サマリを取得する（Ｐ１４１）。等価性検証式生成部１１４は、未処理の変更前スナップショットが無ければ（Ｐ１４２）、処理を終了する。【００９９】
等価性検証式生成部１１４は、変更前記号実行前サマリからスナップショットを一つ選択し（Ｐ１４３）、変更前／後記号実行結果記憶領域２０３から変更後記号実行サマリを取得する（Ｐ１４４）。等価性検証式生成部１１４は、未処理の変更後スナップショットが無くなければ（Ｐ１４５）、Ｐ１４２に戻る。等価性検証式生成部１１４は、変更後記号実行サマリのスナップショットを一つ選択し（Ｐ１４６）、パス等価性検証式を生成し（ステップＰ１４７）、Ｐ１４５に戻る。等価性検証式生成部１１４は、未処理の変更前スナップショットが無ければ（Ｐ１４５）、Ｐ１４２に戻るため、変更前スナップショットと変更後スナップショットのすべての組合せに対してパス等価性検証式生成できる。【０１００】
等価性検証式生成部１１４は、選択した変更前スナップショットと変更後スナップショットに対して、スナップショットに対応するパスを通った範囲内での等価性を検証するためのパス等価性検証式を生成し、等価性検証式記憶領域２０４に格納する（Ｐ１４７）。【０１０１】
パス等価性検証式は、対応する出力変数間の等号制約式の連言の否定式と、選択した変更前スナップショットのスナップショット制約式と、選択した変更後スナップショットのスナップショット制約式との連言となる。【０１０２】
たとえば変更前記号実行サマリＳ１２０中のスナップショットＳ１０４と変更後記号実行サマリＳ３２０中のスナップショットＳ３２１を選択したときのパス等価性検証式は、¬（（Ｒ＝Ｒ’）∧（ｇ＝ｇ’））∧（（γ＝０）∧（ｇ＝γ）∧（Ｒ＝０））∧（（γ＝０）∧（ｇ’＝γ）∧（Ｒ’＝０））となる。【０１０３】
上記の説明例では、等価性検証式生成部１１４は、一度に一つずつのスナップショットを選択し、パス等価性検証式を生成する。等価性検証式生成部１１４は、一度に複数のスナップショットを選択しても良い。その場合、パス等価性検証式生成に用いるスナップショット制約式の代わりに、選択したスナップショットに対応するスナップショット制約式の選言を用いる。【０１０４】
また、上記の説明例では、記号実行計算部１１３の処理が完了してから、パス等価性検証式を生成する等価性検証式生成部１１４が処理を開始しているが、記号実行計算部１１３の実行中において、一部のスナップショットの生成が完了した時点で、当該スナップショットに係る組合せに対するパス等価性検証式の生成のために、等価性検証式生成部１１４の処理を開始しても良い。【０１０５】
等価性検証式検証部１１５は、等価性検証式生成部１１４によって生成された複数のパス等価性検証式に対して、それぞれＳＡＴソルバ等を用いて充足可能性を判定する。等価性検証式検証部１１５は、それぞれのパス等価性検証式に対して、充足可能か不可能かの結果と、充足可能な場合にはソルバが出力する充足するような変数の値の例である反例とを等価性検証式検証結果記憶領域２０５に記録する。【０１０６】
図１６は、本例における各パス等価性検証式の検証結果７００である。変更前スナップショットと変更後スナップショットの組合せ９通りのうち、６通りに関しては充足不可能である。また、残りの３通りに関しては充足可能であり、例えば図１６の反例の列に示すような反例を得られる。【０１０７】
検証結果生成ステップＰ１６０では、検証結果生成部１１６は、たとえば図１７に示すような検証結果レポート６００を生成する。【０１０８】
検証結果レポート６００には、検証結果表示６１０として、すべてのパス等価性検証式検証結果が充足不可能な場合には「等価」と、充足可能なパス等価性検証式がある場合には「非等価」と表示される。本例では、例えばスナップショットＳ１１３とスナップショットＳ３２２を選択したときのパス等価性検証式が充足可能であるため「非等価」と表示される。【０１０９】
検証結果レポート６００には、変更前／後記号実行結果記憶領域２０３に格納されている記号実行サマリ情報を用いて、変更前記号実行サマリ６３１および変更後記号実行サマリ６３２の表示を含んでも良い。この時、スナップショットの検証結果６３９を表示することができる。【０１１０】
スナップショットの検証結果６３９は、各パス等価性検証式の検証結果７００を参照し、当該スナップショットを選択したパス等価性検証式の検証結果すべてが充足不可能であれば「等価」、充足可能なパス等価性検証式があれば「非等価」を表示する。【０１１１】
本例では、スナップショットＳ１０４を選択しているすべてのパス等価性検証式、および、スナップショットＳ３２１を選択しているすべてのパス等価性検証式は充足不可能であるため、対応する検証結果が「等価」と表示されている。一方、それ以外のスナップショットにおいては、充足可能なパス等価性検証式を含むため「非等価」と表示されている。【０１１２】
検証結果レポートは、等価性検証式検証結果記憶領域２０５に格納されている反例情報を用いて、非等価となるような反例情報６４０の表示を含んでも良い。この時、記号実行サマリの表示中にスナップショットを選択するためのチェックボックス６３８を設け、選択したスナップショットの組合せに対するパス等価性検証式の反例を表示するようにしても良い。【０１１３】
図１７に示す例では、スナップショットＳ１１３とスナップショットＳ３２２に対応するチェックボックスを選択した際に、図１６にあるスナップショットＳ１１３とスナップショットＳ３２２から生成されたパス等価性検証式の反例７０８から得られた情報が表示されている。【０１１４】
検証結果レポート６００には、さらに、変更前／後ソースコード記憶領域２０１に格納されているソースコードを用いて、変更前ソースコード６２１および変更後ソースード６２２の表示を含んでも良い。このとき、スナップショットを選択するためのチェックボックス６３８を用いて選択されたスナップショットに対して、当該スナップショットが持つ位置情報から、ソースコード上においてそのスナップショットの経路を表示させても良い。【０１１５】
図１７に示す例では、変更前ソースコード６２１上に、スナップショットＳ１１３の位置情報を用いてスナップショットＳ１１３の経路を下線で表示している。また、変更後ソースコード６２２上に、スナップショットＳ３２２の位置情報を用いてスナップショットＳ３２２の経路を下線で表示している。【０１１６】
経路を表示する方法としては、図１７に示す下線で表示する方法の他にも、背景を別の色で表示する、字体や文字サイズを変えて強調表示する、経路以外の部分の表示を消去して経路のみ表示されるようにする、などの方法がある。【０１１７】
あるスナップショットの組合せに対する等価性検証結果が非等価であり、非等価である原因を調査する場合、そのスナップショットの経路上に原因が存在しており、経路以外の箇所は当該スナップショットの結果には影響を与えないため調査不要である。【０１１８】
選択したスナップショットに対応する経路がソースコード上に表示され、また、それらの組合せに対応する反例が表示されることにより、非等価となる入力および出力に対して、開発者がソースコード上で調査すべき範囲を絞り込むことが可能となり、非等価である原因を発見することが容易となる。【０１１９】
図１８は検証結果レポート６００において、スナップショットを選択するチェックボックス６３８で複数のスナップショットを選択した際の表示の例を示している。複数のスナップショットを選択した際には、複数のスナップショット経路が存在する。そこで、複数のスナップショット経路に対する表示方法を選択するラジオボタン６５０を設けて、そこで選択された表示方法に従い経路を表示させることができる。【０１２０】
スナップショット経路表示方法６５０として、「共通」と「合併」が用意されている。「共通」を選択した場合には、選択された複数のスナップショットすべてが通過する部分のみが経路として表示される。また、「合併」を選択した場合には、選択された複数のスナップショットのうち少なくとも一つが通過する部分が経路として表示される。【０１２１】
図１８中の変更後ソースコード６２２に示す例では、非等価なスナップショットであるスナップショットＳ３２２とスナップショットＳ３２３が選択されており、表示方法としては「共通」が選択されている。そのため、両スナップショットが通過する部分のみが経路として表示される。【０１２２】
一般に、複数のスナップショットに対して等価性検証結果が非等価となった場合、それぞれ個別の原因により非等価となっている可能性より、同一の要因により非等価となっている可能性の方が高い。同一の原因により非等価となっている場合には、複数のスナップショットの経路の共通部分の中にその原因が存在する。そのため、経路の共通部分を表示することにより、開発者がソースコード上で調査すべき範囲を絞り込むことができる。【０１２３】
図１８の例では、表示された経路のうち、条件評価やｒｅｔｕｒｎ文を除くと６行目のｇ＝ｇ＋１の処理のみとなる。実際、この行をｇ＝ｇ−１に修正することにより、等価な変更を得ることが可能であり、共通経路を表示することにより、開発者が修正に必要な調査範囲を絞込むことが可能となっている。【０１２４】
複数のスナップショットの経路を表示する方法としては、図１８に示す共通部分や合併範囲を表示する方法の他にも、通過するスナップショットの数に対応させて、色の濃度を変化させる、もしくは、文字サイズを変化させる方法などがある。
【実施例３】
【０１２５】
図１９を用いて、本実施例のソースコード等価性検証装置の処理の具体例について説明する。【０１２６】
等価性検証式生成部１１４が、実施例１で生成した等価性検証式（本実施例の説明では全体等価性検証式と呼ぶ）と、実施例２で生成したパス等価性検証式とを比較すると、個々のパス等価性検証式の項数は全体等価性検証式の項数よりも小さく、計算量も小さくなるため、そのソルバでの検証時間も短くなる。一方、すべてのパス等価性検証式の合計の計算量は、全体等価性検証式の計算量よりも大きくなる。【０１２７】
本実施例は、これらの特徴を用いて、ソースコード等価性検証装置１０００が、全体等価性検証式による検証とパス等価性検証式による検証とを組合せて実行する。【０１２８】
本実施例においては、ソースコード等価性検証装置１０００は複数のＣＰＵ１０１またはＣＰＵコアを持ち、複数の計算を同時並列で実行可能であるとする。複数のＣＰＵコアで並列計算する代わりに、外部ネットワーク１５０を通じてクラウドコンピューティング環境またはグリッドコンピューティング環境の外部計算機１６０を用いることにより並列計算を実現しても良い。【０１２９】
図１５は、本実施例における、等価性検証式生成部１１４の処理ステップＰ１４０における処理フローチャートである。の詳細を図１５に示す。変更前記号実行サマリの取得ステップＰ１４１では等価性検証式生成部１１４は、変更前／後記号実行結果記憶領域２０３から変更前ソースコードの記号実行サマリを取得する（Ｐ１４１）。【０１３０】
本実施例では、ソースコード入力部１１１、構造グラフ生成部１１２、および記号実行計算部１１３の各処理は実施例1と同一であり、その説明を省略する。また、本実施例の等価性検証式生成部１１４の処理は、実施例１に示す等価性検証式生成部１１４の処理と実施例２に示す等価性検証式生成部１１４の処理の両方を実行し、全体等価性検証式とパス等価性検証式との両方を等価性検証式記憶領域２０４に格納する。【０１３１】
図１９は、本実施例における等価性検証式検証部１１５の処理フローチャートの一例である。等価性検証式検証部１１５は全体等価性検証式の検証を開始する（Ｐ２０１）。【０１３２】
等価性検証式検証部１１５は、パス等価性検証式の内、まだ検証を開始していない式が残っているかどうかを判定し（Ｐ２０２）、残っていればＰ２０３に、残っていなければＰ２０６に移行する。【０１３３】
等価性検証式検証部１１５は、新たにパス等価性検証式の検証を開始するために、空いているＣＰＵコアがあるかどうかを判定し（Ｐ２０３）、あればＰ２０４に、なければＰ２０６に移行する。【０１３４】
等価性検証式検証部１１５は、まだ検証を開始していないパス等価性検証式の内、一つを選択する（Ｐ２０４）。等価性検証式検証部１１５は、選択したパス等価性検証式の検証を空いているＣＰＵコア上で開始し（Ｐ２０５）、Ｐ２０６に移行する。【０１３５】
等価性検証式検証部１１５は、以降では、検証を開始した各等価性検証式の検証終了を判定する。等価性検証式検証部１１５は、全体等価性検証式の検証が終了したかどうかを判定し（Ｐ２０６）、終了した場合にはＰ２０７に、終了していない場合にはＰ２０８に移行する。【０１３６】
等価性検証式検証部１１５は、全体等価性検証式の検証結果が充足不可能かどうかを判定する（Ｐ２０７）。充足不可な場合には、等価性検証の結果が「等価」であるので、パス等価性検証式の検証を継続する必要がなく、等価性検証式検証部１１５は、処理を終了する。【０１３７】
検証結果が充足可能である場合、等価性検証の結果は「非等価」であるが、全体等価性検証式の検証結果のみでは、スナップショット単位での等価性の情報を得ることができない。そのため、等価性検証式検証部１１５は、Ｐ２０８に移行し、パス等価性検証式の検証を継続する。【０１３８】
等価性検証式検証部１１５は、新たに検証が終了したパス等価性検証式があるかどうかを判定し（Ｐ２０８）、ある場合はＰ２０９に、ない場合はＰ２１１に移行する。【０１３９】
等価性検証式検証部１１５は、新たに検証が終了したパス等価性検証式の検証結果が充足可能かどうかを判定し（Ｐ２０９）、充足可能な場合には、Ｐ２１０に移行し、充足不可能な場合にはＰ２１１に移行する。【０１４０】
等価性検証式検証部１１５は、部分検証結果レポートを生成する（Ｐ２１０）。この処理（Ｐ２１０）は、新たに「非等価」であるスナップショットの組合せが発見されたときに実行される。【０１４１】
部分検証結果レポートは、終了しているパス等価性検証式検証結果を用いて、実施例２で説明した検証結果生成部１１６の処理と同様の方法で生成する。この部分検証結果レポートを用いることにより、すべてのパス等価性検証式の検証が終了する前に、開発者は非等価となるスナップショットの組合せ、および、それらのスナップショットの経路を知ることが可能となる。【０１４２】
ステップＰ２１１では、等価性検証式検証部１１５は、すべてのパス等価性検証式の検証が終了したかどうかを判定し（Ｐ２１１）、終了した場合には、処理を終了する。【０１４３】
終了していない検証式（まだ開始していない検証式を含む）が存在する場合には、等価性検証式検証部１１５は、Ｐ２０２に移行し、新たなパス等価性検証式の検証開始や終了待ちの処理を繰り返す。【０１４４】
Ｐ２０４における、まだ検証を開始していないパス等価性検証式の内、一つを選択する方法としては、パス等価性検証式の項数が少ない検証式を選択する方法や、式中に使用されている変数の種類数が少ない検証式を選択する方法がある。これらは、検証時間が短くなる可能性の高い検証式を先に実行することにより、短時間で多くの検証式の検証を終了できるという効果がある。【０１４５】
他の選択方法として、ソースコード上の修正した箇所を経由するスナップショットに係るパス等価性検証式を選択する方法がある。これは、修正した箇所を経由するスナップショットは非等価になる可能性が高く、これを先に検証することにより、より早いタイミングで開発者に非等価であるスナップショットを提示することが可能となる効果がある。【０１４６】
本実施例における変形例として、全体等価性検証式を用いた検証を省略することができる。具体的には図１９に示す処理ステップの内、Ｐ２０１、Ｐ２０６、Ｐ２０７を省略することができる。【０１４７】
これは、検証結果が非等価となる可能性が高いと予想されるとき、および、ＣＰＵコア数が多く、全体等価性検証式の検証が終了する前に、各パス等価性検証式の検証が終了すると見込まれるときに、結果として不要となる全体等価性検証式の検証を省略し、計算量を削減できるという効果がある。【０１４８】
本実施例におけるさらに他の変形例として、部分検証結果生成を省略することができる。具体的には図１９に示す処理ステップの内、Ｐ２０８、Ｐ２０９、Ｐ２１０を省略することができる。【０１４９】
これは、開発者に迅速に非等価な部分を提示する必要性が低い場合、および、部分的な検証結果を表示し、修正すべき場所以外の場所を修正することを避けたい場合に、部分検証結果を生成するための計算量を削減できる効果がある。【０１５０】
なお、本発明は上記した実施例１から３に限定されるものではなく、様々な変形例が含まれる。例えば、上記した実施例は本発明を分かりやすく説明するために詳細に説明したものであり、必ずしも説明した全ての構成を備えるものに限定されない。また、ある実施例の構成の一部を他の実施例に置き換えることが可能であり、また、ある実施例の構成に他の実施例の構成を加えることも可能である。また、各実施例の構成の一部について、他の構成の追加・削除・置換をすることが可能である。また、上記の各構成、機能、処理部、処理手段等は、それらの一部または全部を、例えば集積回路で設計する等によりハードウェアで実現してもよい。
【符号の説明】
【０１５１】
１０００…ソースコード等価性検証装置、１０１…ＣＰＵ、１０２…主記憶装置、１０３…ネットワークＩ／Ｆ、１０５…入出力Ｉ／Ｆ、１０６…補助記憶装置Ｉ／Ｆ、１１０…制御部、１２０…表示・出力装置、１３０…入力装置、１４０…記憶部、１５０…外部ネットワーク、１６０…外部計算機、２００…ソースコード等価性検証プログラム、２０１…変更前／後ソースコード記憶領域、２０２…変更前／後構造グラフ記憶領域、２０３…変更前／後記号実行結果記憶領域、２０４…等価性検証式記憶領域、２０５…等価性検証式検証結果記憶領域、２０６…検証結果記憶領域、１１１…ソースコード入力部、１１２…構造グラフ生成部、１１３…記号実行計算部、１１４…等価性検証式生成部、１１５…等価性検証式検証部、１１６…検証結果生成部、３０１…変更前ソースコード、３０２…変更後ソースコード、３１０…検証結果レポート、Ｓ１００、Ｓ２００、Ｓ３００…記号実行の実行木、Ｓ１２０、Ｓ２２０、Ｓ３２０…記号実行サマリ、Ｓ１０４、Ｓ１０９、Ｓ１１３、Ｓ３２１〜Ｓ３２３…記号実行におけるスナップショット、５００、５５０、６００…検証結果レポート。
【図１】
2016038741.tif 000003
【図２】
2016038741.tif 000004
【図３】
2016038741.tif 000005
【図４】
2016038741.tif 000006
【図５】
2016038741.tif 000007
【図６】
2016038741.tif 000008
【図７】
2016038741.tif 000009
【図８】
2016038741.tif 000010
【図９】
2016038741.tif 000011
【図１０】
2016038741.tif 000012
【図１１】
2016038741.tif 000013
【図１２】
2016038741.tif 000014
【図１３】
2016038741.tif 000015
【図１４】
2016038741.tif 000016
【図１５】
2016038741.tif 000017
【図１６】
2016038741.tif 000018
【図１７】
2016038741.tif 000019
【図１８】
2016038741.tif 000020
【図１９】
2016038741.tif 000021
【国際調査報告】
2016038741.tif 000022
2016038741.tif 000023
2016038741.tif 000024
2016038741.tif 000025