抄録
B-013
定理証明技術を用いたソースコードの補完手法
小池遼平(早大)・小野康一(日本IBM)・深澤良彰(早大)
ソフトウェア開発を効率的に行うための技術の1つに,途中まで記述されたソースコードの不足部分を自動で補うコード補完がある.近年では,実装途中のコードと類似したソースコードを探索することで,補完候補として複数の命令文からなるコード断片を推薦するような手法が提案されている.しかし,従来手法では実装途中のコードに対する推薦コードの妥当性までは保証されない.我々は,形式手法を活用させ定理証明技術を組み込んだコード補完手法を提案する.本手法では実装途中のソースコードに加え,実装中のコードに与えられた事前条件/事後条件を考慮するため,開発者が求めている仕様を充足するコードに限定して推薦を行うことができる.