C言語を対象とした記述問の差異に基づく効率的な等価性検証手法

摘要

本稿では、C言語を対象とした記号シミュレーションによる効率的な等価性検証の手法を提案する。 検証の対象は、ハードウエア化のために、原則としてポインタや再帰呼び出しを取り除いた、制限されたC言語プログラムとしている。 検証は、与えられた2つのC言語記述に対する記号シミュレーションの結果を用いて行われる。 従来の手法では、それぞれの記述の差異に対して等価性を判定して全体の等価性を導いていたが、等価でない差異がある場合は、それ以降の全ての文に対して等価性判定をする必要があり、非効率的であつた。本稿では、記述間の差異を利用して検証が必要な関数に対してのみ記号シミュレーションを行い、また、記述が等しい部分のシミュレーションでは、等価性判定を省略することによつて、差異の小さな2っの記述を効率的に検証できる手法を提案する。