(57)【要約】【課題】人手で実施されたリファクタリングに対する等価性検証を、記号実行によりおこなうときに、計算量を爆発させずに、迅速におこなえるようにする。【解決手段】ソースコードの等価性を検証する際に、ソースコードを解析した構造グラフによる構造比較による検証と記号実行による検証の二種類の検証をおこなう。そして、構造グラフによる構造比較によって構造が一致すると判定できる場合は、記号実行をおこなわない。また、構造比較による検証の前には、リファクタリング前後の各々のソースコードを、リファクタリングパターンごとに定められた正規化情報に基づき、構造グラフを正規化し、リファクタリングが正当なときには、構造が一致するように調整する。さらに、リファクタリング前後の各々の構造グラフを抽象化したものを記号実行して検証することにより、記号実行をおこなう箇所を限定する。【選択図】  図３
2014126985.tif 000002
【特許請求の範囲】
【請求項１】
ＣＰＵと記憶装置とを有し、前記記憶装置に記憶されたプログラムを前記ＣＰＵにより実行させることにより、ソースコードの変更の前後の等価性を検証するソースコード等価性検証装置であって、
変更前のソースコードと、変更後のソースコードを入力するソースコード入力手段と、
前記ソースコードの変更の変更種別パターン情報を入力する変更種別パターン入力手段と、
前記変更前のソースコードと、前記変更後のソースコードの各々に対して、変更前ソースコード情報と、変更後ソースコード情報を生成するソースコード情報生成手段と、
ソースコード変更種別パターンに対して、定義される正規化情報を参照し、前記変更前ソースコード情報と、前記変更後ソースコード情報を正規化し、各々変更前ソースコード正規化情報と、変更後ソースコード正規化情報を生成する正規化手段と、
前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報の構造を比較する構造比較手段と、
前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報を記号実行する記号実行手段と、
前記記号実行手段により記号実行の結果を比較して、前記変更前ソースコードと前記変更後ソースコードの等価性を判定する等価性判定手段とを有することを特徴とするソースコード等価性検証装置。
【請求項２】
前記構造比較手段により、前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報の構造が比較され、構造が一致すると判定されたときに、前記記号実行手段は、前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報に対して記号実行をおこなわないようにすることを特徴とする請求項１記載のソースコード等価性検証装置。
【請求項３】
さらに、ソースコード情報を抽象化して縮減する抽象化手段を有し、
前記構造比較手段により、前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報の構造が比較され、構造が不一致であると判定されたときに、前記抽象化手段が、前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報の各々の抽象化をおこなって、前記変更前ソースコード抽象化情報と、前記変更後ソースコード抽象化情報を生成し、
前記記号実行手段は、前記変更前ソースコード抽象化情報と、前記変更後ソースコード抽象化情報に対して、記号実行をすることを特徴とする請求項１記載のソースコード等価性検証装置。
【請求項４】
ＣＰＵと記憶装置とを有し、前記記憶装置に記憶されたプログラムを前記ＣＰＵにより実行させることにより、ソースコードの変更の前後の等価性を検証するソースコード等価性検証装置によるソースコード等価性検証方法であって、
変更前のソースコードと、変更後のソースコードとを入力するソースコード入力ステップと、
前記ソースコードの変更の変更種別パターン情報を入力する変更種別パターン入力ステップと、
前記変更前のソースコードと、前記変更後のソースコードの各々に対して、変更前ソースコード情報と、変更後ソースコード情報を生成するソースコード情報生成ステップと、
ソースコード変更パターンに対して、定義される正規化情報を参照し、前記変更前ソースコード情報と、前記変更後ソースコード情報を正規化し、各々変更前ソースコード正規化情報と、変更後ソースコード正規化情報を生成する正規化ステップと、
前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報の構造を比較する構造比較ステップと、
前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報を記号実行する記号実行ステップと、
前記記号実行手段により記号実行の結果を比較して、前記変更前ソースコードと前記変更後ソースコードの等価性を判定する等価性判定ステップと、
前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報の各々の抽象化をおこなって、前記変更前ソースコード抽象化情報と、前記変更後ソースコード抽象化情報を生成する抽象化ステップとを有し、
前記構造比較ステップにより、前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報の構造が比較され、構造が一致すると判定されたときに、前記記号実行ステップにおいて、前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報に対して記号実行をおこなわないようにし、
前記構造比較ステップにより、前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報の構造が比較され、構造が不一致であると判定されたときに、前記抽象化ステップを実行し、前記変更前ソースコード正規化情報と、前記変更後ソースコード正規化情報の各々に対して、前記変更前ソースコード抽象化情報と、前記変更後ソースコード抽象化情報を生成し、
前記記号実行ステップにおいて、前記変更前ソースコード抽象化情報と、前記変更後ソースコード抽象化情報に対して、記号実行をすることを特徴とするソースコード等価性検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソースコード等価性検証装置、および、ソースコード等価性検証方法に係り、特に、ソフトウェアのリファクタリングにおいて、リファクタリング実施による不具合混入を防ぐために、記号実行の手法により、プログラムとしての振る舞いが等価であることを検証する場合に、計算量の爆発的増加を防止し、迅速にリファクタリングの正当性を検証するのに好適なソースコード等価性検証装置、および、ソースコード等価性検証方法に関する。
【背景技術】
【０００２】
近年、情報処理社会が進展することにより、ソフトウェアシステムが一般社会に浸透し、ソフトウェアに求められる信頼性が非常に高度なものになってきている。一方で、ソフトウェアは、長年にわたる差分・派生開発によって複雑化および大規模化の一途をたどり、ソフトウェアの拡張しやすさや理解しやすさといった保守性の低下が問題となっている。
【０００３】
リファクタリングは、非特許文献１に開示されている方法であって、ソフトウェアの振る舞いを変えずに、内部構造を変更することにより、ソフトウェアの設計品質を改善する手法の総称であり、複雑さを軽減し保守性を向上させるものである。
このリファクタリングの手法は、複雑化および大規模化の一途をたどるソフトウェアの保守性を確保するために有望な技術であるが、ソースコードを変更するため新たに不具合を混入してしまう可能性がある。具体的には、リファクタリングには、複数のパターンとして類別される方法が存在し、それぞれソースコードの変更の手順と、その変更によりソフトウェアの振る舞いを変えないことを保証するためのソースコードに対する条件とが、明示的もしくは暗黙的に定められている。この変更の手順に従わずに、ソースコードを変更した場合、または、そのような条件に従っていないソースコードを変更した場合には、対象となっているソフトウェアの振る舞いを変えないことが保証されないため、ソフトウェアに不具合が混入する可能性がある。したがって、ソフトウェア開発者が、ソフトウェアの保守段階において、リファクタリングが原因で正しく動作していたソフトウェアに不具合が混入することをおそれ、リファクタリングをおこなわない判断が有り得る。そのため、ソフトウェアの保守段階において、リファクタリングを積極的におこなうために、リファクタリングによる不具合の混入が無いことを検証する手法が求められる。
【０００４】
非特許文献４では、７２種の典型的に用いられるリファクタリングのパターン（以下、単に「リファクタリングパターン」という）が定義されている。
【０００５】
本明細書中において、二つのソースコードが外的な振る舞いが同じであることを、すなわち、同じ入力に対して、実行時に、同じ出力が得られることを、各々のソースコードが「等価」であると定義し、リファクタリング実施前のソースコードとリファクタリング実施後のソースコードが、等価であることを検証することを「等価性検証」ということにする。
【０００６】
等価性検証の手法として、特許文献１に開示されるソースコード比較によって差異が生じている部分のみテストを実施する手法、非特許文献２に開示されるソースコードをグラフで表現しリファクタリングごとに定めた事前条件をグラフが満たすかを検証する手法、非特許文献３に開示される記号実行を用いて振る舞いが保持されていることを検証する手法がある。
【先行技術文献】
【特許文献】
【０００７】
【特許文献１】特開２０１０−６７１８８号公報
【非特許文献】
【０００８】
【非特許文献１】W. F. Opdyke，“Refactoring: A Program Restructuring Aid in Designing Object−Oriented Application Frameworks”，Technical Report UIUC−DCS−R−92−1759， USA， University of Illinois at Urbana−Champaign，1992
【非特許文献２】T. Mens，S. Demeyer， D. Janssens，“Formalising Behaviour Preserving Program Transformations”，Proceedings of the First International Conference on Graph Transformation，USA，2002
【非特許文献３】S. Person，M. B. Dwyer，S. Elbaum，C. S. Pasareanu，“Differential Symbolic Execution”，Proc. of ACM SIGSOFT Symposium on the Foundations of Software Engineering 2008，USA，2008
【非特許文献４】M. Fowler et al.，“Refactoring: Improving the Design of Existing Code”，USA，Addison−Wesley Professional，1 edition，July 8，1999
【発明の概要】
【発明が解決しようとする課題】
【０００９】
特許文献１に開示される方法によると、リファクタリング前とリファクタリング後のソースコード上の差異を検出する。そして、検出した差異部分に関するテストを生成し、リファクタリング前と後のソースコードに対して生成したテストを実施し、それらの結果を検証する。これは、リファクタリング実施時に特別なプロセスを必要としない半面、いくつかの問題が存在する。リファクタリング箇所によっては影響が広範囲に波及し、生成したテストのみでは等価性を検証しきれない可能性が残る。また、影響の波及がなく差異部分のみの検証であっても、テストのカバレッジによって、検証漏れが生じる可能性が残る。テストによる等価性検証は、検証漏れなどの可能性のため不完全である。
【００１０】
非特許文献２では、プログラムのメソッド呼び出し関係をグラフで表現し、リファクタリングごとに定めた事前条件を満たすか否かを検証する手法を開示している。このアプローチは、振る舞いの検証を構造上の検証で実現するため、リファクタリングごとに、その操作を厳密に定義した上で、振る舞いに影響を及ぼさないための条件を網羅している。そのため、事実上、リファクタリングがツールにより自動化されることが必須であり、リファクタリング操作そのものを誤りうる、人手でのリファクタリングの検証には利用できないという問題点がある。
【００１１】
非特許文献３では、リファクタリング前後のソースコードに対して等価性検証をおこなう技術として、記号実行を用いる手法を開示している。
【００１２】
記号実行とは、対象のプログラムの入力として、数値を与える代わりに、記号を与えることにより、プログラムの振る舞いを網羅的に解析する手法である。
【００１３】
以下、図１７を用いて記号実行の一例について説明する。  
図１７は、記号実行の一例を説明するために、ソースコードとそれより派生するデータ構造について示した図である。
【００１４】
記号実行においては、入力変数の値を記号変数と呼ばれる記号を用いて表現し、その記号変数がプログラム中でどのように参照・更新されていくかを解析する。ここでは、Ｃ言語で記述されたソースコードＥ００１に記載する関数ｆｏｏを対象に記号実行を実施するものとする。記号実行の対象となるソースコードＥ００１に対して記号実行をおこなうにあたり、先ず、通常のソースコードをコンパイルするときと、同様に字句解析や構文解析を実施する。その結果から、ソースコードＥ００１から制御フローや制御依存グラフ、データ依存グラフなどを抽出した構造グラフＥ００２が得られる。記号実行では、構造グラフＥ００２を用いて、実行木Ｅ０２０を生成していく。実行木Ｅ０２０中の各ノードは、そのノードに到達するための記号変数で表現されたパス制約と、そのノードにおける各変数の値を記号変数で表現した変数状態から構成される。図１７の実行木Ｅ０２０では、各ノードの上側にパス制約を、下側に変数状態を表現している。
【００１５】
実行木Ｅ０２０の生成過程について以下に詳細を説明する。
【００１６】
記号実行の開始段階において、ソースコードＥ００１中で、プログラムの入力となる変数に対して記号変数を割当てる。ソースコードＥ００１の例では、グローバル変数ａ，ｂ，ｃが入力となる変数であるため、それぞれに対して、α，β，γという記号変数を割当てる。構造グラフＥ００２上では、ノードＥ００３に対応する開始状態においては、実行木Ｅ０２０は、ノードＥ０１０の単一のノードのみからなる実行木となる。ノードＥ０１０のパス制約Ｅ０１０ａは、制約無し（任意の変数状態に対して制約を満たす）を意味するｔｒｕｅとなり、変数状態Ｅ０１０ｂは記号変数の割当てに従って、各変数と対応する記号変数が等しいことを示している。
【００１７】
構造グラフＥ００２上では、ノードＥ００３の次にはノードＥ００４が実行される。それにともなって、実行木においてもＥ０１０の子ノードＥ０１１が生成される。子ノードＥ０１１におけるパス制約Ｅ０１１ａ、および、変数状態Ｅ０１１ｂは、親ノードＥ０１０のパス制約Ｅ０１０ａ、および、変数状態Ｅ０１０ｂがコピーされた上で、構造グラフＥ００２上のノードＥ００４が実行される。
【００１８】
ノードＥ００４においては、変数ａに対して０が代入されている。そのため、実行木のノードＥ０１１の変数状態Ｅ０１１ｂにおける、変数ａに対する状態はａ＝０に更新される。
【００１９】
構造グラフＥ００２上で、ノードＥ００４に次となるノードはＥ００５である。ノードＥ００５においては、変数状態の更新がおこなわれていないため、実行木における新たなノードを生成しない。ノードＥ００５は、ｉｆ文による条件分岐である。そのため、構造グラフＥ００２の制御フローで次となるノードは、ノードＥ００６とノードＥ００７の二つのノードがある。記号実行においては、取り得る制御フローをすべて網羅するために、条件分岐においては、それぞれの分岐に応じた子ノードを生成する。すなわち、ノードＥ００６に対応して実行木中のノードＥ０１１の子ノードとしてＥ０１２を生成し、ノードＥ００７に対応して実行木中のノードＥ０１１の子ノードとしてＥ０１３を生成する。
【００２０】
実行木のノードＥ０１２のパス制約Ｅ０１２ａは、親ノードのパス制約Ｅ０１１ａと条件分岐の分岐条件との論理積（ＡＮＤ、図では、＆）になる。ノードＥ００５における分岐条件は、ｃ＜０であり、また、変数状態Ｅ０１１ｂから、変数ｃを記号変数で表わすとγとなることから、条件分岐が成立するための条件はγ＜０であることが分かる。そこで、ｔｒｕｅとγ＜０との論理積であるγ＜０がノードＥ０１２におけるパス制約Ｅ０１２ａとなる。
【００２１】
次に、子ノードＥ０１３のパス制約Ｅ０１３ａは、Ｅ０１３が条件分岐の分岐条件が成立しない場合に対応していることから、親ノードのパス制約Ｅ０１１ａと条件分岐の分岐条件の否定（ＮＯＴ、図では、！）との論理積になる。すなわち、ｔｒｕｅと！（γ＜０）との論理積である！（γ＜０）が、子ノードＥ０１３のパス制約Ｅ０１３ａとなる。
【００２２】
ノードＥ０１１の子ノードＥ０１２の変数状態Ｅ０１２ｂ、子ノードＥ０１３の変数状態Ｅ０１３ｂは、親ノードＥ０１１の変数状態Ｅ０１１ｂがコピーされた上で、計算が続行される。ノードＥ０１２の変数状態Ｅ０１２ｂは、ノードＥ００６で変数ｃに０が代入されるため、ｃに対する変数状態がｃ＝０に更新される。ノードＥ０１３の変数状態Ｅ０１３ｂは、ノードＥ００７で変数ａに変数ｃの値が代入されている。この時点において、変数ｃの変数状態が記号変数のγとなっているので、変数状態Ｅ０１３ｂにおいて、変数ａの変数状態がａ＝γに更新される。
【００２３】
以降も上記と同様の手順により実行木を生成していく。制御フロー上においてノードＥ００６の次のノードはＥ００８であり、このＥ００８は条件分岐であるため、実行木においては、ノードＥ０１２に対して二つの子ノードＥ０１４およびＥ０１５が生成される。ノードＥ００８における分岐条件は（ｂ＜０）であるが、これを変数状態を用いて記号変数で表現すると（β＜０）になる。そのため、子ノードＥ０１４、および、Ｅ０１５のパス制約は、親ノードＥ０１２のパス制約Ｅ０１２ａにそれぞれ（β＜０）、および、！（β＜０）との論理積をとったものとなる。子ノードＥ０１４では、次に制御フロー上のノードＥ００９ａが実行される。Ｅ００９ａは変数ａにａ−ｂの値を代入するものであり、変数状態から、変数ａの状態が０、変数ｂの状態がβであると分かるので、変数ａの状態が−βに更新される。子ノードＥ０１５では、次に制御フロー上のノードＥ００９ｂが実行される。Ｅ００９ｂは変数ａにａ＋ｂの値を代入するものであり、変数状態から、変数ａの状態が０、変数ｂの状態がβと分かるので、変数ａの状態がβに更新される。
【００２４】
制御フロー上においてノードＥ００７の次のノードはＥ００８であり、このＥ００８は条件分岐であるため、実行木においては、ノードＥ０１３に対して二つの子ノードＥ０１６およびＥ０１７が生成される。ノードＥ００８における分岐条件は（ｂ＜０）であるが、これを変数状態を用いて記号変数で表現すると（β＜０）になる。そのため、子ノードＥ０１６、および、Ｅ０１７のパス制約は、親ノードＥ０１３のパス制約Ｅ０１３ａにそれぞれ（β＜０）、および、！（β＜０）との論理積をとったものとなる。子ノードＥ０１６では、次に制御フロー上のノードＥ００９ａが実行される。Ｅ００９ａは、変数ａにａ−ｂの値を代入するものであり、変数状態から、変数ａの状態がγ、変数ｂの状態がβであると分かるので、変数ａの状態がγ−βに更新される。子ノードＥ０１７では、次に制御フロー上のノードＥ００９ｂが実行される。Ｅ００９ｂは変数ａにａ＋ｂの値を代入するものであり、変数状態から、変数ａの状態がγ、変数ｂの状態がβと分かるので、変数ａの状態がγ＋βに更新される。
【００２５】
実行木Ｅ０２０のすべての葉ノードに対して、その制御フローが関数の終了まで到達すると、実行木の生成が終了する。図１７の実行木Ｅ０２０は、関数ｆｏｏに対する記号実行が終了した時点での実行木を示している。記号実行が終了した時点での実行木の各葉ノードを集めたものが記号実行の結果となる（これを「記号実行サマリ」ということにする）。記号変数α，β，γの任意の組合せは、記号実行サマリ中の各葉ノードのうちいずれかのパス制約を満たす。そのノードに含まれる変数状態を用いることによって、入力となる記号変数の値から、プログラム実行後の各変数の値を知ることができる。例えば、関数ｆｏｏの実行前の変数ａ，ｂ，ｃのいずれの値も１である場合、記号変数はα＝β＝γ＝１となり、ノードＥ０１７のパス制約を満たす。ノードＥ０１７の変数状態から関数ｆｏｏ実行後の変数ａの値はａ＝γ＋β＝２、ｂ＝β＝１、ｃ＝γ＝１となることが分かる。上記のように、記号実行は、プログラムが取り得る制御パスを網羅した上で、プログラム実行前後の変数値の関係を入力値の条件（パス条件）と、出力変数の状態（変数状態）の組の集合である記号実行サマリを求める計算であるということができる。
【００２６】
リファクタリング前後のソースコードの構造グラフに対して、それぞれ記号実行し、論理的に等価な記号実行サマリが得られたとき、すなわち、同じ入力に対し同じ出力が得られる場合に、上で定義したように、ソースコードが等価であると判断できる。このように、記号実行は、対象のプログラムの取り得る動作系列を網羅的に解析するため、テストを用いた検証におけるカバレッジの問題や、事前条件の検証におけるツール依存の問題が生じない。その一方で、繰り返し文や再帰構造をもつプログラムでは、実行木が複雑なものになり、計算量が発散し爆発しやすい。計算量を抑えるためには、記号実行の範囲の限定や、事前条件による実行の制限が必要であり、記号実行の利点である検証の完全性が失われる。
【００２７】
非特許文献３では、比較するソースコード間に共通部分が存在する点に着目し、完全性を維持したまま計算量を減らす工夫をしている。変更されていない共通のブロックの実行結果を関数（uninterpreted function）で表現することにより、実行木の上の計算量の発散を防ぐ。しかしながら、差異部分の実行木上の計算量が発散するケースが依然として残り、計算量が爆発する可能性が残る。また、ハードウェア等外界との相互作用を持つプログラムの扱いに対しては言及されていない。
【００２８】
本発明は、上記問題点を解決するためになされたもので、その目的は、人手で実施されたリファクタリングに対する等価性検証を、記号実行によりおこなうときに、計算量を爆発させずに、迅速におこなえるようなソースコード等価性検証方法を提供することにある。
【課題を解決するための手段】
【００２９】
本発明のソースコード等価性検証装置は、ＣＰＵと記憶装置とを有し、記憶装置に記憶されたプログラムをＣＰＵにより実行させることにより、ソースコードの変更の前後の等価性を検証するソースコード等価性検証装置であって、変更前のソースコードと、変更後のソースコードを入力するソースコード入力手段と、ソースコードの変更の変更種別パターン情報を入力する変更種別パターン入力手段と、変更前のソースコードと、変更後のソースコードの各々に対して、変更前ソースコード情報と、変更後ソースコード情報を生成するソースコード情報生成手段と、ソースコード変更種別パターンに対して、定義される正規化情報を参照し、変更前ソースコード情報と、変更後ソースコード情報を正規化し、各々変更前ソースコード正規化情報と、変更後ソースコード正規化情報を生成する正規化手段と、変更前ソースコード正規化情報と、変更後ソースコード正規化情報の構造を比較する構造比較手段と、変更前ソースコード正規化情報と、変更後ソースコード正規化情報を記号実行する記号実行手段と、記号実行手段により記号実行の結果を比較して、変更前ソースコードと変更後ソースコードの等価性を判定する等価性判定手段と、ソースコード情報を抽象化して縮減する抽象化手段とを有するものである。
【００３０】
そして、構造比較手段により、変更前ソースコード正規化情報と、変更後ソースコード正規化情報の構造が比較され、構造が一致すると判定されたときに、記号実行手段は、変更前ソースコード正規化情報と、変更後ソースコード正規化情報に対して記号実行をおこなわないようにする。
【００３１】
一方、構造比較手段により、変更前ソースコード正規化情報と、変更後ソースコード正規化情報の構造が比較され、構造が不一致であると判定されたときに、抽象化手段が、変更前ソースコード正規化情報と、変更後ソースコード正規化情報の各々の抽象化をおこなって、変更前ソースコード抽象化情報と、変更後ソースコード抽象化情報を生成し、記号実行手段は、変更前ソースコード抽象化情報と、変更後ソースコード抽象化情報に対して、記号実行をするようにする。
【００３２】
本発明のソースコード等価性検証装置によれば、リファクタリングパターン情報に対応したソースコード情報正規化を、リファクタリング前ソースコード情報とリファクタリング後ソースコード情報に適用し、構造比較をおこない、構造の一致・不一致により、ソースコードの等価・非等価を判定する。そして、構造比較をおこない構造が一致すると判定されたときには、記号実行をおこなうまでもなく、ソースコードが等価であると判定されるので、計算量が多くなる記号実行の必要がなくなるというメリットがある。また、構造比較において、構造が不一致であると判定された場合は、ソースコード情報の抽象化をおこない、ソースコード情報を縮減して、抽象化をおこなったソースコード情報に対して、記号実行により等価性の検証をおこなうことが可能となる。そのため、本発明によれば、完全性を維持したまま計算量を爆発させずにソースコード等価性検証が可能となる。
【発明の効果】
【００３３】
本発明によれば、人手で実施されたリファクタリングに対する等価性検証を、記号実行によりおこなうときに、計算量を爆発させずに、迅速におこなえるようなソースコード等価性検証方法を提供することができる。
【図面の簡単な説明】
【００３４】
【図１】本発明の一実施形態に係るソースコード等価性検証装置のハードウェア構成図である。
【図２】本発明の一実施形態に係るソースコード等価性検証装置のソフトウェア構成図である。
【図３】本発明の一実施形態に係るソースコード等価性検証装置全体の機能と、データフローを示した図である。
【図４】本発明の一実施形態に係るソースコード等価性検証装置の処理を示すフローチャートである。
【図５】入力部１１００の機能の詳細とデータフローを示した図である。
【図６】正規化部１２００の機能の詳細とデータフローを示した図である。
【図７】構造比較検証処理部１３００の機能の詳細とデータフローを示した図である。
【図８】記号実行実施判定部１７００の機能の詳細とデータフローを示した図である。
【図９】記号実行検証処理部１４００の機能の詳細とデータフローを示した図である。
【図１０】リファクタリング前後のソースコードの例を示す図である（その一）。
【図１１】リファクタリング前後のソースコードに対応するソースコード情報の例を示す図である（その一）。
【図１２】ソースコード情報に対しておこなわれる正規化の例を示す図である。
【図１３】リファクタリング前後のソースコードの例を示す図である（その二）。
【図１４】リファクタリング前後のソースコードに対応するソースコード情報の例を示す図である（その二）。
【図１５】抽象化されたソースコード情報の例を示す図である。
【図１６】リファクタリング前ソースコードとリファクタリング後ソースコードに対して記号実行したときの実行木を示した例である。
【図１７】記号実行の一例を説明するために、ソースコードとそれより派生するデータ構造について示した図である。
【発明を実施するための形態】
【００３５】
以下、本発明における一実施形態を、図１ないし図１６を用いて説明する。
【００３６】
〔ソースコード等価性検証装置の構成と処理〕
以下、図１ないし図９を用いて本発明の一実施形態に係るソースコード等価性検証装置の構成と処理について説明する。
先ず、図１を用いて本発明の一実施形態に係るソースコード等価性検証装置のハードウェア構成について説明する。
図１は、本発明の一実施形態に係るソースコード等価性検証装置のハードウェア構成図である。
【００３７】
本発明の一実施形態に係るソースコード等価性検証装置のハードウェア構成としては、例えば、図１に示されるような一般的なパーソナルコンピュータで実現される。
【００３８】
ソースコード等価性検証装置１０００は、ＣＰＵ（Central Processing Unit）１０１、主記憶装置１０２、ネットワークＩ／Ｆ１０３、グラフィックＩ／Ｆ１０４、入出力Ｉ／Ｆ１０５、補助記憶装置Ｉ／Ｆ１０６が、バスにより結合された形態になっている。
【００３９】
ＣＰＵ１０１は、ソースコード等価性検証装置１００の各部を制御し、主記憶装置１０２にソースコード等価性検証プログラム２００をロードして実行する。
【００４０】
主記憶装置１０２は、通常、ＲＡＭなどの揮発メモリで構成され、ＣＰＵ１０１が実行するプログラム、参照するデータが記憶される。
【００４１】
ネットワークＩ／Ｆ１０３は、外部ネットワーク１５０と接続するためのインタフェースである。
【００４２】
グラフィックＩ／Ｆ１０４は、ＬＣＤ（Liquid Crystal Display）などの表示装置１２０を接続するためのインタフェースである。
【００４３】
入出力Ｉ／Ｆ１０５は、入出力装置を接続するためのインタフェースである。図１の例では、キーボード１３１とポインティングデバイスのマウス１３２が接続されている。
【００４４】
補助記憶装置Ｉ／Ｆ１０６は、ＨＤＤ（Hard Disk Drive）１４１やＤＶＤドライブ（Digital Versatile Disk）１４２などの補助記憶装置を接続するためのインタフェースである。
【００４５】
ＨＤＤ１４１は、大容量の記憶容量を有しており、本実施形態を実行するためのソースコード等価性検証プログラム２００が格納されている。
【００４６】
ＤＶＤドライブ１４２は、ＤＶＤやＣＤなどの光学ディスクにデータを書き込んだり、光学ディスクからデータを読み込んだりする装置であり、ソースコード等価性検証プログラム２００は、例えば、ＣＤ−ＲＯＭにより提供されたものをインストールすることができる。
【００４７】
本実施形態のソースコード等価性検証装置１０００は、上記のようなパーソナルコンピュータに、ソースコード等価性検証プログラム２００をインストールして、各機能を実行するものである。
【００４８】
次に、図２を用いて本発明の一実施形態に係るソースコード等価性検証装置のソフトウェア構成について説明する。
図２は、本発明の一実施形態に係るソースコード等価性検証装置のソフトウェア構成図である。
【００４９】
ソースコード等価性検証装置のソフトウェア構成は、図２に示したように、プログラム等価性検証プログラム２００よりなり、プログラム等価性検証プログラム２００は、サブルーチンであるソースコード解析モジュール２０１、構造グラフ生成・更新モジュール２０２、構造グラフ解析モジュール２０３、実行木生成モジュール２０４、記号実行実行モジュール２０５、入出力モジュール２０６、データベースモジュール２０７からなる。
【００５０】
なお、プログラム等価性検証プログラム２００は、ＯＳ（Operating System）上で動作するアプリケシーンソフトウェアであり、ソースコード等価性検証装置のソフトウェア構成として、ＯＳやライブラリプログラムも含むが図では、省略している。
【００５１】
プログラム等価性検証プログラム２００は、サブルーチンであるソースコード解析モジュール２０１、構造グラフ生成・更新モジュール２０２、構造グラフ解析モジュール２０３、実行木生成モジュール２０４、記号実行実行モジュール２０５、入出力モジュール２０６、データベースモジュール２０７からなる。
【００５２】
ソースコード解析モジュール２０１は、ソースコードの字句解析・構文解析をおこない、構造グラフ生成のために必要な情報を取り出すモジュールである。
【００５３】
構造グラフ生成・更新モジュール２０２は、ソースコード解析モジュール２０１の解析結果に基づいて、構造グラフを生成したり、更新したりするモジュールである。
【００５４】
構造グラフ解析モジュール２０３は、構造グラフのグラフ構造を解析するモジュールである。
【００５５】
実行木生成モジュール２０４は、構造グラフ解析モジュール２０３の解析結果に基づき、実行木を生成するモジュールである。
【００５６】
記号実行実行モジュール２０５は、実行木生成モジュール２０４が生成した実行木に対する記号実行をおこなうモジュールである。
【００５７】
入出力モジュール２０６は、外部から必要なデータの入出力をおこなうモジュールである。
【００５８】
データベースモジュール２０７は、各種データベースにアクセスするためのモジュールである。
【００５９】
次に、図３ないし図９を用いて本発明の一実施形態に係るソースコード等価性検証装置の機能と、その処理について説明する。
図３は、本発明の一実施形態に係るソースコード等価性検証装置全体の機能と、データフローを示した図である。
図４は、本発明の一実施形態に係るソースコード等価性検証装置の処理を示すフローチャートである。
図５は、入力部１１００の機能の詳細とデータフローを示した図である。
図６は、正規化部１２００の機能の詳細とデータフローを示した図である。
図７は、構造比較検証処理部１３００の機能の詳細とデータフローを示した図である。
図８は、記号実行実施判定部１７００の機能の詳細とデータフローを示した図である。
図９は、記号実行検証処理部１４００の機能の詳細とデータフローを示した図である。
【００６０】
本実施形態のソースコード等価性検証装置１０００は、図３に示されるように、リファクタリング前ソースコード０００１とリファクタリング後ソースコード０００２の二つのソースコードと、リファクタリング前ソースコード０００１に対して適用されたリファクタリングパターンに関する入力情報であるリファクタリングパターン入力情報０００３の入力によって、リファクタリング前ソースコード０００１とリファクタリング後ソースコード０００２のソースコードの等価性を検証するものである。本実施形態のソースコード等価性検証装置１０００の処理は、図１に示されたＰＣなどのハードウェアが、図２に示されたソースコード等価性検証プログラム２００を実行することによりおこなわれる。
【００６１】
先ず、入力部１１００において、入力されたリファクタリング前ソースコード０００１の入力を受け付ける（図４のＳ１０１）。リファクタリング後ソースコード入力ステップＳ１０２では、入力部１１００において、リファクタリング後ソースコード０００２を受け付ける（Ｓ１０２）。また、入力部１１００において、リファクタリングパターン入力情報０００３の入力を受け付ける（Ｓ１０３）。
【００６２】
以下、図５を用いて上記の入力部１１００の機能の詳細とその処理について説明する。
【００６３】
リファクタリング前ソースコード０００１は、図５に示されるように、入力部１１００におけるソースコード入力部１１０１によって受け取られ、ソースコードの字句解析と構文解析をおこない、リファクタリング前ソースコード情報１００１に変換される。リファクタリング後ソースコード０００２も、入力部１１００におけるソースコード入力部１１０１によって受け取られ、ソースコードの字句解析と構文解析をおこない、リファクタリング後ソースコード情報１００２に変換され、記憶部１６００に格納される。また、リファクタリングパターン入力情報０００３は、入力部１１００におけるリファクタリングパターン入力部１１０２によって受け付けられ、リファクタリングパターン種別を表すリファクタリングパターン情報１００３に変換され、記憶部１６００に格納される。
【００６４】
次に、リファクタリング前ソースコード情報１００１と、リファクタリング後ソースコード情報１００２を比較し、ソースコードの構造上の変更箇所を特定する（Ｓ１０４１）。
【００６５】
そして、正規化部１２００は、記憶部１６００に格納された情報を用いて、リファクタリング前ソースコード情報１００１とリファクタリング後ソースコード情報１００２の正規化をおこなう（Ｓ１０４２）。
【００６６】
ここで、正規化とは、リファクタリングがおこなわれたソースコードのソースコード情報を、そのソースコードと等価なソースコードに対応するソースコード情報に変換することを意味する。この正規化は、この後に続く構造比較ステップＳ１０４３と記号実行ステップＳ１０４５に適した形にするためにおこなわれる。
【００６７】
以下、図６を用いて上記の正規化部１２００の機能の詳細とその処理について説明する。  
リファクタリング前ソースコード情報１００１とリファクタリング後ソースコード情報１００２は、正規化部１２００の変更箇所特定部１２０１に入力される。一方、正規化ＤＢ１６０１に格納されているリファクタリングパターン情報１００３に対応した変更箇所特定情報１００７ｂを取得される。そして、変更箇所特定部１２０１はソースコード情報を比較し、リファクタリングパターン情報１００３に対応した変更箇所特定情報１００７ｂを参照し、ソースコードの構造上の変更箇所を特定し、変更箇所情報１００４を生成する（Ｓ１０４１）。
【００６８】
次に、リファクタリングパターン入力情報１００３に対応する正規化の方法を示した正規化情報１００７ａを記憶部１６００の正規化ＤＢ１６０１から取得する（Ｓ１０４２）。正規化ＤＢ１６０１には、リファクタリングパターンごとに対応した正規化情報１００７ａを格納してある。正規化部１２００のソースコード正規化部において、リファクタリング前ソースコード情報１００１に対して、取得した正規化情報１００７ａに基づき正規化をおこない、リファクタリング前正規化ソースコード情報１００５を生成する。また、正規化部１２００のソースコード正規化部において、リファクタリング後ソースコード情報１００２に対して、正規化情報１００７ａに基づき、正規化をおこない、リファクタリング後正規化ソースコード情報１００６を生成する。
【００６９】
次に、構造比較検証処理部１３００は、リファクタリング前正規化ソースコード情報１００５とリファクタリング後正規化ソースコード情報１００６の構造を比較し、同じ構造であるか否かを検証する（ステップＳ１０４２）。
【００７０】
以下、図７を用いて構造比較検証処理部１３００の機能の詳細とその処理について説明する。
【００７１】
構造比較検証処理部１３００は、リファクタリング前正規化ソースコード情報１００５とリファクタリング後正規化ソースコード情報１００６を受け取り、二つの正規化後のソースコード情報の構造が一致しているか否かの比較をおこない、一致した場合は、構造比較結果１００８として、一致しているという情報を生成し、不一致の場合は、構造比較結果１００８として、不一致であるいう情報を生成する（Ｓ１０４３）。
【００７２】
次に、記号実行実施判定部１７００では、記号実行をおこなうべきか否かを判定する（Ｓ１０４７）。ここで、上記の構造比較ステップＳ１０４３の結果で、構造が一致していると判定されたときには、等価非等価出力ステップＳ１０５に行き、構造が不一致であると判定されたときには、ソースコード抽象化ステップＳ１０４４に行く。
【００７３】
以下、図８を用いて記号実行実施判定部１７００の機能の詳細とその処理について説明する。
【００７４】
記号実行実施判定部１７００は、構造比較結果１００８を受け取り、構造比較結果１００８で、構造が「一致」であれば、等価非等価出力ステップＳ１０５へ移行し、出力部１５００に、ソースコードが等価であるとして検証結果０００４を出力させる。
【００７５】
ソースコードが等価であるいう結果が出力されたときには、ユーザは、おこなわれたリファクタリングが正当であると判断することができる。
【００７６】
記号実行実施判定部１７００は、構造比較結果１００８を受け取り、構造比較結果１００８で、構造が「不一致」であれば、記号実行開始指示１００９を生成する。
【００７７】
次に、ソースコード情報の抽象化をおこなう（Ｓ１０４４）。
【００７８】
ここで、ソースコード情報の抽象化とは、各々のソースコード情報に対して、記号実行したときに、同じ入力を与えて、同じ結果がでるようにした状態を保ったまま、ソースコード情報を縮約することを意味する。
【００７９】
次に、抽象化したリファクタリング前のソースコード情報と、抽象化したリファクタリング後のソースコード情報に対して、記号実行をおこなう（Ｓ１０４５）。
【００８０】
そして、記号実行の結果を比較し、同じ入力に対して、同じ出力（記号実行サマリ）が得られるときには、元のソースコードが等価であると、判断し、出力（記号実行サマリ）が異なるときには、元のソースコードが非等価であると、判断して（Ｓ１０４６）、等価非等価の結果出力をおこなう。
【００８１】
ここで、ソースコードが等価であるいう結果が出力されたときには、ユーザは、おこなわれたリファクタリングが正当であると判断することができ、ソースコードが非等価であるいう結果が出力されたときには、ユーザは、おこなわれたリファクタリングが不当であると判断することができる。そして、ユーザは、おこなわれたリファクタリングが不当であると判断したときには、おこなったリファクタリングを見直して、正当なものに修正する作業を開始することができる。
【００８２】
記号実行検証処理部１４００は、記号実行開始指示１００８を受けて、ソースコード抽象化ステップＳ１０４４を開始する。ソースコード抽象化ステップ１０４４では、記憶部１６００の抽象化ＤＢ１６０２に格納されている抽象化方法情報を用いて、リファクタリング前正規化ソースコード情報と変更箇所情報１００４を受け取り、抽象化をおこない、リファクタリング前抽象化ソースコード情報を生成する。また、ソースコード抽象化ステップ１０４４では、記憶部１６００の抽象化ＤＢ１６０２に格納されている抽象化手法を用いて、リファクタリング後正規化ソースコード情報と変更箇所情報１００４を受け取り、抽象化をおこない、リファクタリング後抽象化ソースコード情報を生成する。ここで、抽象化ＤＢに格納されている抽象化方法情報は、正規化後のソースコード情報に対して、変更箇所情報１００４に関わらない箇所とループや再帰呼び出しの箇所を置き換えて、この後の記号実行ステップＳ１０４５の時に、変更箇所情報１００４に関わらない箇所とループや再帰呼び出しの箇所を記号実行しないように変換する処理の方法に関する情報である。
【００８３】
記号実行ステップＳ１０４５では、記号実行部１４０２において、リファクタリング前抽象化ソースコード情報１４０３とリファクタリング後抽象化ソースコード情報１４０４に対して、記号実行をおこない、それぞれリファクタリング前記号実行結果１４０５とリファクタリング後記号実行結果を得る。記号実行結果比較ステップＳ１０４６では、記号実行結果比較部１４０７において、リファクタリング前記号実行結果１４０５とリファクタリング後記号実行結果が同じものであるか否かを比較し判定する。記号実行結果比較部１４０７において、リファクタリング前記号実行結果１４０５とリファクタリング後記号実行結果が同じものであった場合、等価非等価出力ステップＳ１０５へ移行し、等価として出力部１５００に検証結果０００４を出力させる。記号実行結果比較部１４０７において、リファクタリング前記号実行結果１４０５とリファクタリング後記号実行結果が異なるものであった場合、等価非等価出力ステップＳ１０５へ移行し、非等価として出力部１５００に検証結果０００４を出力させる。
【００８４】
本実施形態のソースコード等価性検証装置によれば、計算量が爆発しやすい記号実行をおこなう前に、それぞれのリファクタリング前後のそれぞれのソースコード情報に対して、正規化後に、構造比較をおこない、その元になるソースコードが等価であると判定された場合には、記号実行をおこなわない。
【００８５】
また、構造比較で元になるソースコードが非等価と判定された場合には、ソースコード情報の抽象化をおこなって、ソースコード情報を縮減してから、記号実行をおこなうので、記号実行の計算量を削減することができる。
【００８６】
〔ソースコード等価性検証装置の処理の具体例（構造一致と判定されるときの例）〕
以下、上記の図４を参照しながら、図１０ないし図１２を用いて本発明の一実施形態に係るソースコード等価性検証装置の処理の具体例について説明する。
この例は、図４の記号実行実施判定の処理で、ソースコード情報である構造グラフの構造が一致すると判定される例である。
図１０は、リファクタリング前後のソースコードの例を示す図である（その一）。
図１１は、リファクタリング前後のソースコードに対応するソースコード情報の例を示す図である（その一）。
【００８７】
図１２は、ソースコード情報に対しておこなわれる正規化の例を示す図である。
【００８８】
この例では、ソースコードに対するリファクタリングとして、リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄに基づいたリファクタリングがおこなわれる場合について説明する。リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄは、複数個所で同じ処理をしているソースコードにおいて、その同じ処理を関数として抜き出し、複数個所で同じ処理をしていた箇所を抜き出した関数への呼び出しに置き換えて、複数箇所に存在したソースコードを共通化するリファクタリングのパターンである。このリファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄは、一つの関数においてソースコードの記述量が多い場合に、関数の可読性を向上させるために、その関数内のソースコードの一部を別の関数として抜き出すリファクタリングとしても用いられる。
【００８９】
以下、図１０によりリファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄによって、ソースコードのリファクタリングをおこなう例を説明する。
【００９０】
ソースコードＣ００１は、リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄの適用前のソースコードであり、グローバル変数ｇｌｏｂａｌ＿ｖａｒに対してｍａｉｎ関数において１０を代入するプログラムである。このソースコードＣ００１に対して、リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄを適用したソースコードがＣ００２となる。ソースコードＣ００２は、ソースコードＣ００１におけるｇｌｏｂａｌ＿ｖａｒ＝１０；というグローバル変数への代入文を関数ｆｏｏとして抜き出し、ｇｌｏｂａｌ＿ｖａｒ＝１０；の記述部分であった箇所を関数ｆｏｏの呼び出しに変換している。
【００９１】
先ず、図１０に示したリファクタリングの例における、図４のリファクタリング前ソースコード入力Ｓ１０１とリファクタリング後ソースコード入力Ｓ１０２とリファクタリングパターンＳ１０３のステップについて説明する。
【００９２】
入力部１１００では、ソースコード入力部１１０１によって、リファクタリング前ソースコード０００１とリファクタリング後ソースコード０００２を受け付けて、対応するリファクタリング前ソースコード情報１００１とリファクタリング後ソースコード情報を生成する。ここで、リファクタリング前ソースコード０００１はソースコードＣ００１、リファクタリング後ソースコード０００２はソースコードＣ００２に対応する。
【００９３】
ソースコード等価性検証装置１０００は、入力されたリファクタリング前ソースコード０００１とリファクタリング後ソースコード０００２をソースコード入力部１１０１によって字句解析と構文解析し、図１１の例で示されるような内部で扱う構造グラフに変換される。リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄの例では、ソースコードＣ００１は、構造グラフＭ００１、ソースコードＣ００２は、グラフＭ００２に変換される。ここで、リファクタリング前ソースコード情報１００１は構造グラフＭ００１、リファクタリング後ソースコード情報１００２は構造グラフＭ００２に対応する。
【００９４】
入力部１１００では、リファクタリングパターン入力部１１０２において、リファクタリングパターン入力情報０００３を受け付けて、リファクタリングパターン情報１００３を生成する。この例では、例えば、リファクタリングパターン入力情報０００３が、リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄを表す文字列“ＥｘｔｒａｃｔＭｅｔｈｏｄ”や、画面のメニューでの選択番号のときに、リファクタリングパターン情報１００３として、内部で、リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄを指し示すコードを生成する。
【００９５】
次に、図４の変更箇所特定Ｓ１０４１のステップについて説明する。  
正規化部１２００の変更箇所特定部１２０１において、リファクタリング前ソースコード情報１００１とリファクタリング後ソースコード情報１００２とリファクタリングパターン情報１００３から、正規化ＤＢ１６０１の中にある対応する変更箇所特定情報１００７ｂを参照し、ソースコード上のどこを変更したのかを特定し、変更箇所情報１００４を出力する。このリファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄの例では、リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄは、リファクタリング後ソースコード情報１００２において関数が増加するという特徴から、リファクタリング前ソースコード情報１００１とリファクタリング後ソースコード情報１００２の関数の宣言を比較し、リファクタリング後ソースコード情報１００２のみに現れる関数を変更箇所として特定する。図１１上では、リファクタリング前ソースコード情報１００１の構造グラフＭ００１とリファクタリング後ソースコード情報１００２の構造グラフＭ００２の中で、関数を示すｅｎｔｒｙを比較し、ノードＭ００３が指し示すｅｎｔｒｙのｆｏｏ関数が増えていることから、ノードＭ００３およびｆｏｏ関数を呼び出すノードＭ００４が、変更箇所情報１００４に該当する。
【００９６】
次に、図４のソースコード正規化Ｓ１０４２のステップについて説明する。  
正規化部１２００のソースコード正規化部１２０２において、変更箇所情報１００４とリファクタリング前ソースコード情報１００１から、正規化ＤＢ１６０１の中にある対応する正規化情報１００７ａを用いて正規化をおこない、リファクタリング前正規化ソースコード情報１００５を生成する。リファクタリング後ソースコード情報１００２も同様に正規化をおこない、リファクタリング後正規化ソースコード情報１００６を生成する。このリファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄにおけるソースコード正規化部１２０２の例を示すと、図１２のようになる。先ず、正規化ＤＢ１６０１からリファクタリングパターン情報１００３であるリファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄに該当する正規化情報１００７ａを取得する。リファクタリングパターン情報１００３のＥｘｔｒａｃｔＭｅｔｈｏｄに対応する正規化情報１００７ａによれば、正規化方法は、Ｅｘｔｒａｃｔしたリファクタリング後ソースコード情報０００２における変更箇所１００４の関数を、インライン展開にして基に戻したときのソースコードを表す構造にすることである。
【００９７】
図１２における変更箇所１００４は、リファクタリング後ソースコード情報１００２の構造グラフＭ００２におけるノードＭ００３とノードＭ００４であり、これらのノードは、リファクタリングより作られたＥｘｔｒａｃｔされた関数ｆｏｏであるので、その関数ｆｏｏを正規化して元に戻すと、構造グラフＭ００６のようになる。これがリファクタリング後正規化ソースコード情報１００６となる。リファクタリング前正規化ソースコード情報１００５は、リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄに関して正規化処理が無いため、図１２上のリファクタリング前ソースコード情報０００１の構造グラフＭ００１は正規化では何も変更されずに、そのまま、構造グラフＭ００５となる。
【００９８】
次に、図４の構造比較Ｓ１０４３のステップについて説明する。  
構造比較検証処理部１３００では、リファクタリング前正規化ソースコード情報１００５とリファクタリング後正規化ソースコード情報１００６を受け取り、ソースコード情報の構造の比較をおこない、その結果を構造比較結果１００８として生成する。リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄによるリファクタリングをおこなったこの図１０による例において、構造比較検証処理部１３００は、リファクタリング前正規化ソースコード情報１００５のグラフＭ００５とリファクタリング後正規化ソースコード情報１００６のグラフＭ００６の二つのグラフが同じ構造でありそれぞれのノードが同じであるため、構造比較結果１００８として、ソースコードＣ００１とソースコードＣ００２を等価であると判定する。
【００９９】
次に、図４の記号実行実施判定Ｓ１０４７のステップについて説明する。  
記号実行実施判定部１７００は、リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄによるリファクタリングをおこなったこの図１０による例において、構造比較結果１００８として、リファクタリング前後のソースが等価として判定されるため、等価非等価出力ステップＳ１０５に移行し、出力部１５００は、構造比較検証処理部１３００が等価と判定した結果を受けて、検証結果０００４として等価であることを出力する。
【０１００】
記号実行実施判定部１７００は、リファクタリングパターンＥｘｔｒａｃｔＭｅｔｈｏｄによるリファクタリングをおこなったこの図１０による例では、正規化部１２００による変換と構造比較検証処理部１３００の判定処理によって、リファクタリング前後のソースコードが、各々等価と判定できるため、記号実行検証処理部１４００により、記号実行の計算を必要とせず、計算量を不必要に増加させずに、迅速な等価判定が可能となる。
【０１０１】
〔ソースコード等価性検証装置の処理の具体例（構造不一致と判定されるときの例）〕
以下、上記の図４を参照しながら、図１３ないし図１６を用いて本発明の一実施形態に係るソースコード等価性検証装置の処理の具体例について説明する。
この例は、図４の記号実行実施判定の処理で、ソースコード情報である構造グラフの構造が不一致であると判定される例である。
図１３は、リファクタリング前後のソースコードの例を示す図である（その二）。
図１４は、リファクタリング前後のソースコードに対応するソースコード情報の例を示す図である（その二）。
図１５は、抽象化されたソースコード情報の例を示す図である。
図１６は、リファクタリング前ソースコードとリファクタリング後ソースコードに対して記号実行したときの実行木を示した例である。
【０１０２】
この例では、ソースコードに対するリファクタリングとして、ソースコードにおける条件式を変更せずに変数への代入を整理するリファクタリングがおこなわれる場合について説明する。
【０１０３】
図１３では、リファクタリング前のソースコードＣ００３とリファクタリング後のソースコードＣ００４が示されており、ソースコードＣ００３とソースコードＣ００４の間で、ソースコードにおける条件式を変更せずに変数への代入を整理するリファクタリングが適用されている。具体的には、リファクタリング前のソースコードＣ００３では、ソースコード部分Ｃ００５が示す所において、変数ａに対して値を代入し、ソースコード部分Ｃ００６が示す所において、変数ａ（左辺）の値を用いて演算し変数ａ（右辺）に代入している。リファクタリング後のソースコードＣ００４では、ソースコード部分Ｃ００７が示す所において、変数ｂに対して値を代入し、ソースコード部分Ｃ００８が示す所において、変数ｂの値を用いて演算し変数ａに代入している。リファクタリング前と後で、ソースコード部分Ｃ００５が示す所とソースコード部分Ｃ００７が示す所に存在する条件式、ソースコード部分Ｃ００６が示す所とソースコード部分Ｃ００８が示す所に存在する条件式が一致しているが用いている変数を変更し、ソースコードＣ００４の方が、ソースコード行数が少なく可読性が高いものになっている。図１３の例で示すリファクタリングは、非特許文献４に記載されているリファクタリングパターン７２種に該当せず、本実施形態のソースコード等価性検証装置１０００においてもパターンとしてデータベースに登録されていないものとする。
【０１０４】
先ず、図１３に示したリファクタリングの例における、図４のリファクタリング前ソースコード入力Ｓ１０１とリファクタリング後ソースコード入力Ｓ１０２について説明する。このリファクタリングの例では、リファクタリング前ソースコード０００１がソースコードＣ００３、リファクタリング後ソースコード０００２がソースコードＣ００４に対応する。入力部１１００では、ソースコード入力部１１０１によって、リファクタリング前ソースコード０００１とリファクタリング後ソースコード０００２を受け付けて、対応するリファクタリング前ソースコード情報１００１とリファクタリング後ソースコード情報を生成する。図１３のリファクタリングの例において、ソースコード入力部１１０１がリファクタリング前ソースコード０００１としてソースコードＣ００３を受けつけ、字句解析と構文解析をおこない、リファクタリング前ソースコード情報１００１として図１４の構造グラフＭ００８に変換する。また、ソースコード入力部１１０１は、リファクタリング後ソースコード０００２としてソースコードＣ００４を受けつけ、字句解析と構文解析をおこない、リファクタリング後ソースコード情報１００２として図１４の構造グラフＭ００９に変換する。ここで、リファクタリング前ソースコード情報１００１は構造グラフＭ００８、リファクタリング後ソースコード情報１００２は構造グラフＭ００９に対応する。
【０１０５】
次に、リファクタリングパターンに関する情報を入力するＳ１０３のステップについて説明する。
【０１０６】
入力部１１００では、リファクタリングパターン入力部１１０２において、リファクタリングパターン入力情報０００３を受け付けて、リファクタリングパターン情報１００３を生成する。このリファクタリングの例では、リファクタリングパターンは、登録されていないものと仮定しているため、「該当無し」を示す文字列やメニューの選択番号がリファクタリングパターン入力部１１０２に入力され、リファクタリングパターン入力部は、リファクタリングパターン情報１００３として、「該当無し」を示すコードを生成する。
【０１０７】
次に、図４の変更箇所特定Ｓ１０４１のステップについて説明する。  
正規化部１２００の変更箇所特定部１２０１において、リファクタリング前ソースコード情報１００１とリファクタリング後ソースコード情報１００２から、ソースコード上のどこを変更したのかを特定し、変更箇所情報１００４を出力する。このリファクタリングの例では、リファクタリング前ソースコード情報１００１である構造グラフＭ００８とリファクタリング後ソースコード情報０００２である構造グラフＭ００９を比較し、両方に関数ｆｏｏと関数ｖａｒが存在しているため関数レベルの増減が無く、ｆｏｏ関数の内部に差異がみられるため、変更箇所特定部１２０１は、ｆｏｏ関数の内部を変更箇所情報１００４として出力する。なお、この例では、リファクタリングパターンとして「該当無し」なので、正規化ＤＢ１６０１の変更箇所特定情報１００７ｂは、参照せず、構造グラフの構造を解析することだけで、変更箇所を特定する。
【０１０８】
次に、図４のソースコード正規化Ｓ１０４２のステップについて説明する。
【０１０９】
正規化部１２００のソースコード正規化部１２０２において、変更箇所情報１００４とリファクタリング前ソースコード情報１００１から、正規化ＤＢ１６０１の中にある対応する正規化情報１００７ａの正規化手法を用いて正規化をおこない、リファクタリング前正規化ソースコード情報１００５を生成する。リファクタリング後ソースコード情報１００２も同様に正規化をおこない、とリファクタリング後正規化ソースコード情報１００６を生成する。このリファクタリングの例では、正規化ＤＢ１６０１からリファクタリングパターン情報１００３である「該当無し」に対応する正規化情報を取得する。ここで、リファクタリングパターン情報１００３である「該当無し」に対応する正規化情報は、変換無しとなるため、ソースコード正規化部１２０２は、リファクタリング前ソースコード情報１００１とリファクタリング後ソースコード情報１００２に関して、何も変更せずにリファクタリング前正規化ソースコード情報１００５とリファクタリング後正規化ソースコード情報１００６を出力する。正規化部１２０２で変換されていないので、リファクタリング前正規化ソースコード情報１００５は、図１４における構造グラフＭ００８であり、リファクタリング後正規化ソースコード情報は、図１４における構造グラフＭ００９である。
【０１１０】
次に、図４の構造比較Ｓ１０４３のステップについて説明する。  
構造比較検証処理部１３００では、リファクタリング前正規化ソースコード情報１００５とリファクタリング後正規化ソースコード情報１００６を受け取り、ソースコード情報の構造の比較をおこない、構造比較結果１００８を生成する。このリファクタリングの例では、リファクタリング前正規化ソースコード情報１００５のグラフＭ００８とリファクタリング後正規化ソースコード情報１００６の構造グラフＭ００９を比較し、明らかにグラフ構造が異なるため、構造比較結果１００８として、リファクタリング前後の構造が不一致であると判定する。
【０１１１】
次に、図４の記号実行実施判定ステップＳ１０４７について説明する。  
記号実行実施判定部１７００は、このリファクタリングの例において、構造比較結果１００８として、ソースコードが非等価と判定されため、記号実行開始指示１００９のコマンドを生成する。
【０１１２】
次に、図４のソースコード抽象化ステップＳ１０４４について説明する。  
記号実行検証処理部１４００は、記号実行開始指示１００９を受け取ると、抽象化部１４０１において、変更箇所情報１００４と抽象化ＤＢ１６０２の抽象化方法を記録した抽象化情報１０１０を用いて、リファクタリング前正規化ソースコード情報１００５とリファクタリング後正規化ソースコード情報１００６の抽象化をおこなう。抽象化ＤＢ１６０１の抽象化情報１６０３には、変更箇所情報１００４に対応して適切な抽象化手法が記録されている。このリファクタリングの例では、変更箇所情報１００４は関数ｆｏｏの内部と判明しているため、抽象化ＤＢ１６０１から、関数ｆｏｏを除いたソースコードの中で、リファクタリング前後で差異が生じていない関数を変数に変換して抽象化する方法を記載した抽象化情報１６０３を取得する。抽象化部１４０１において、リファクタリング前後で差異が生じていない関数を変数に変換して抽象化する方法を、リファクタリング前正規化ソースコード情報１００５のグラフＭ００８とリファクタリング後正規化ソースコード情報１００６のグラフＭ００９に適用した結果を示すと、図１５のようになる。図１４のリファクタリング前正規化ソースコード情報１００５の構造グラフＭ００８において、ノードＭ０１０の関数ｖａｒはリファクタリングによって差異が生じていないため、関数ｖａｒを呼び出す箇所のノードＭ０１１と合わせて変数ｖとして抽象化をおこない、図１５の構造グラフＭ０１４のように変換する。ただし、この抽象化は、ノードＭ０１０と他のノードとのＤａｔａＤｅｐｅｎｄｅｎｃｙ（データの依存性）がないことが必要である。図１４におけるリファクタリング後正規化ソースコード情報１００６のグラフＭ００９に関しても、同様に抽象化をおこない制御フローグラフＭ０１５に変換される。抽象化部１４０１は、前記制御フローグラフＭ０１４をリファクタリング前抽象化ソースコード情報１４０３、前記制御フローグラフＭ０１５をリファクタリング後抽象化ソースコード情報１４０４として出力する。ここで、この抽象化は、構造グラフＭ００８、Ｍ００９の各々において、ノードがカットされて、各々が記号実行されたときには、計算量が減ることに留意する。
【０１１３】
次に、図４の記号実行Ｓ１０４５のステップについて説明する。  
記号実行検証処理部１４００では、抽象化部１４０１において抽象化をおこなった後、リファクタリング前抽象化ソースコード情報１４０３とリファクタリング後抽象化ソースコード情報１４０４のそれぞれに対して、記号実行部１４０２において、記号実行を実行し、その結果としてリファクタリング前記号実行結果１４０５とリファクタリング後記号実行結果１４０６を生成する。このリファクタリングの例において、記号実行部１４０２にて、前記リファクタリング前抽象化情報１４０３とリファクタリング後抽象化情報１４０４を記号実行した結果は、図１６に示されるようになる。このリファクタリングの例では、リファクタリング前抽象化情報１４０３は、図１５の構造グラフＭ０１４に該当し、構造グラフＭ０１４に対して記号実行をおこなうと、図１６における実行木Ｅ１００ができる。また、図１６の実行木Ｅ１００における記号実行サマリであるＥ１０１，Ｅ１０２，Ｅ１０３，Ｅ１０４が、リファクタリング前抽象化情報１４０３に対するリファクタリング前記号実行結果１４０５となる。リファクタリング後抽象化情報１４０４は、図４のリファクタリングの例では、図１５の構造グラフＭ０１５に該当し、構造グラフＭ０１５に対して記号実行をおこなうと、図１６における実行木Ｅ２００ができる。また、図１６の実行木Ｅ２００における記号実行サマリであるＥ２０１，Ｅ２０２，Ｅ２０３，Ｅ２０４が、リファクタリング後抽象化情報１４０４に対するリファクタリング後記号実行結果１４０６となる。
【０１１４】
次に、図４の記号実行結果比較Ｓ１０４６のステップについて説明する。  
記号実行検証処理部１４００の記号実行結果比較部１４０７では、リファクタリング前記号実行結果１４０５とリファクタリング後記号実行結果１４０６の比較をおこない、リファクタリング前後のソースコードが等価か非等価かの判定をおこなう。図１３のリファクタリングの例では、リファクタリング前記号実行結果１４０５は、Ｅ１０１，Ｅ１０２，Ｅ１０３，Ｅ１０４であり、リファクタリング後記号実行結果１４０５は、Ｅ２０１，Ｅ２０２，Ｅ２０３，Ｅ２０４である。これらの二つの記号実行結果を比較すると、Ｅ１０１とＥ２０１のペアと、Ｅ１０２とＥ２０２のペアと、Ｅ１０３とＥ２０３のペアと、Ｅ１０４とＥ２０４のペアがそれぞれパス制約と変数状態が一致しているため、記号実行結果比較部１４０７は、ソースコードが等価と判定し、等価非等価出力部に送る。このとき、リファクタリング前の記号実行木Ｅ１００とリファクタリング後の記号実行木Ｅ２００の間には構造上の差異が生じているが、記号実行の最終的な記号実行サマリが一致しているため。ソースコードが等価と判定する。
【０１１５】
次に、図４の等価非等価出力Ｓ１０５のステップについて説明する。  
出力部１５００は、記号実行比較部１４０７が、ソースコードが等価と判定した結果を受けて、検証結果０００４として、ソースコードが等価であることを出力する。そして、これにより、ユーザは、リファクタリングが妥当なものであることを判断できる。
【０１１６】
本例では、Ｓ１０４７の判定で、ソースコード情報である構造グラフ上の構造の差異を生じるため、ソースコードが等価であることを検証するために、記号実行する必要があるが、ソースコード情報の抽象化をおこない、ソースコード情報の縮減をおこなうために、記号実行における計算量を削減することができる。
【符号の説明】
【０１１７】
０００１…リファクタリング前ソースコード
０００２…リファクタリング後ソースコード
０００３…リファクタリングパターン
０００４…検証結果
１０００…ソースコード等価性検証装置
１１００…入力部
１２００…正規化部
１３００…構造比較検証処理部
１４００…記号実行検証処理部
１５００…出力部
１６００…記憶部
１７００…記号実行実施判定部
１００１…リファクタリング前ソースコード情報
１００２…リファクタリング後ソースコード情報
１００３…リファクタリングパターン情報
１００４…変更箇所情報
１００５…リファクタリング前正規化ソースコード情報
１００６…リファクタリング後正規化ソースコード情報
１００７ａ…正規化情報
１００７ｂ…変更箇所特定情報
１００８…構造比較結果
１００９…記号実行開始指示
１０１０…抽象化情報
１１０１…ソースコード入力部
１１０２…リファクタリングパターン入力部
１２０１…変更箇所特定部
１２０２…ソースコード正規化部
１４０１…抽象化部
１４０２…記号実行部
１４０３…リファクタリング前抽象化ソースコード情報
１４０４…リファクタリング後抽象化ソースコード情報
１４０５…リファクタリング前記号実行結果
１４０６…リファクタリング後記号実行結果
１４０７…記号実行結果比較部
１６０１…正規化データベース
１６０２…抽象化データベース
Ｓ１０１…リファクタリング前ソースコード入力ステップ
Ｓ１０２…リファクタリング後ソースコード入力ステップ
Ｓ１０３…リファクタリングパターン入力情報入力ステップ
Ｓ１０４１…変更箇所特定ステップ
Ｓ１０４２…ソースコード正規化ステップ
Ｓ１０４３…構造比較ステップ
Ｓ１０４４…ソースコード抽象化ステップ
Ｓ１０４５…記号実行ステップ
Ｓ１０４６…記号実行結果比較ステップ
Ｓ１０４７…記号実行実施判定ステップ
Ｓ１０５…等価非等価出力ステップ
Ｃ００１…リファクタリング適用前のソースコード
Ｃ００２…リファクタリング適用後のソースコード
Ｃ００３…リファクタリング適用前のソースコード
Ｃ００４…リファクタリング適用後のソースコード
Ｃ００５…Ｃ００３における関数ｆｏｏ内のソースコードの前半部
Ｃ００６…Ｃ００３における関数ｆｏｏ内のソースコードの後半部
Ｃ００７…Ｃ００４における関数ｆｏｏ内のソースコードの前半部
Ｃ００８…Ｃ００４における関数ｆｏｏ内のソースコードの後半部
Ｅ００１…記号実行を説明するためのソースコード
Ｅ００２…ソースコードの構造グラフ
Ｅ００３…構造グラフにおける関数ｆｏｏのエントリーを示すノード
Ｅ００４…構造グラフにおけるＥ００３の遷移先のノード
Ｅ００５…構造グラフにおけるＥ００４の遷移先のノード
Ｅ００６…構造グラフにおけるＥ００５の分岐先のノード
Ｅ００７…構造グラフにおけるＥ００５の分岐先のノード
Ｅ００８…構造グラフにおけるＥ００６と７の遷移先のノード
Ｅ００９ａ…構造グラフにおけるＥ００８の分岐先のノード
Ｅ００９ｂ…構造グラフにおけるＥ００８の分岐先のノード
Ｅ０１０…Ｅ００３に対応する実行木ノード
Ｅ０１０ａ…Ｅ０１０のパス制約
Ｅ０１０ｂ…Ｅ０１０の変数状態
Ｅ０１１…Ｅ００４に対応する実行木ノード
Ｅ０１１ａ…Ｅ０１１のパス制約
Ｅ０１１ｂ…Ｅ０１１の変数状態
Ｅ０１２…Ｅ００６に対応する実行木ノード
Ｅ０１２ａ…Ｅ０１２のパス制約
Ｅ０１２ｂ…Ｅ０１２の変数状態
Ｅ０１３…Ｅ００７に対応する実行木ノード
Ｅ０１３ａ…Ｅ０１３のパス制約
Ｅ０１３ｂ…Ｅ０１３の変数状態
Ｅ０１４…Ｅ００６を経由した場合のＥ００９に対応する実行木ノード
Ｅ０１５…Ｅ００６を経由した場合のＥ００９ａに対応する実行木ノード
Ｅ０１６…Ｅ００７を経由した場合のＥ００９に対応する実行木ノード
Ｅ０１７…Ｅ００７を経由した場合のＥ００９ａに対応する実行木ノード
Ｅ０２０…記号実行の実行木
Ｅ１００…リファクタリング適用前のソースコード情報の記号実行の実行木
Ｅ１０１…Ｅ１００における記号実行サマリに含まれるノード
Ｅ１０２…Ｅ１００における記号実行サマリに含まれるノード
Ｅ１０３…Ｅ１００における記号実行サマリに含まれるノード
Ｅ１０４…Ｅ１００における記号実行サマリに含まれるノード
Ｅ２００…リファクタリング適用後のソースコード情報の記号実行の実行木
Ｅ２０１…Ｅ２００における記号実行サマリに含まれるノード
Ｅ２０２…Ｅ２００における記号実行サマリに含まれるノード
Ｅ２０３…Ｅ２００における記号実行サマリに含まれるノード
Ｅ２０４…Ｅ２００における記号実行サマリに含まれるノード
Ｍ００１…リファクタリング適用前のソースコードの構造グラフ
Ｍ００２…リファクタリング適用後のソースコードの構造グラフ
Ｍ００３…リファクタリングによって追加された関数を示すノード
Ｍ００４…リファクタリングによって追加された関数を呼び出すノード
Ｍ００５…リファクタリング適用前のソースコード情報の正規化済みの構造グラフ
Ｍ００６…リファクタリング適用後のソースコード情報の正規化済みの構造グラフ
Ｍ００７…正規化によって関数が展開された結果のリンク
Ｍ００８…リファクタリング適用前のソースコードの構造グラフ
Ｍ００９…リファクタリング適用後のソースコードの構造グラフ
Ｍ０１０…Ｍ００８における関数ｖａｒを示すノード
Ｍ０１１…Ｍ００８における関数ｖａｒを呼び出すノード
Ｍ０１２…Ｍ００９における関数ｖａｒを示すノード
Ｍ０１３…Ｍ００９における関数ｖａｒを呼び出すノード
Ｍ０１４…リファクタリング適用前のソースコード情報の抽象化済みの構造グラフ
Ｍ０１５…リファクタリング適用後のソースコード情報の抽象化済みの構造グラフ
Ｍ０１６…Ｍ０１４における抽象化された箇所を示すノード
【図１】
2014126985.tif 000003
【図２】
2014126985.tif 000004
【図３】
2014126985.tif 000005
【図４】
2014126985.tif 000006
【図５】
2014126985.tif 000007
【図６】
2014126985.tif 000008
【図７】
2014126985.tif 000009
【図８】
2014126985.tif 000010
【図９】
2014126985.tif 000011
【図１０】
2014126985.tif 000012
【図１１】
2014126985.tif 000013
【図１２】
2014126985.tif 000014
【図１３】
2014126985.tif 000015
【図１４】
2014126985.tif 000016
【図１５】
2014126985.tif 000017
【図１６】
2014126985.tif 000018
【図１７】
2014126985.tif 000019