アサーションの情報を取り入れた静的解析に基づくデバッグ支援ツールの開発
（2019年度 修士論文）
氏名：関口雄太
概要：
ソフトウェアからバグを取り除くために，様々な手法が提案されている．静的型検査は，プログラム全体を網羅的に検査できる反面，型として表現できない性質は検証できないので，デバッグのにためにはアサーションや契約などの動的手法も用いられる．アサーションは，プログラムの実行時にデータが満たすべき条件 (不変条件) を，プログラムの実行時に検査して違反が 見つかると即座にプログラムの実行を中断することでバグの感染を抑える．アサーションは，プログラミング言語で表せる任意の述語を用いて不変条件を表現できるため，プログラムの仕様や開発者の意図を比較的容易に記述できる．しかし，不変条件の検証のためにプログラムを 実行する必要があり，検証結果は実行に用いたテストケースに依存してしまうため，検証の網羅性は静的な手法に劣る．
本研究では，プログラム内の各変数に対し，アサーション内の述語を静的解析で網羅的に集めて不変条件を生成することで，変数がプログラムの実行中に果たす役割を明らかにする手法を 提案する．アサーション内に書かれた述語は，プログラマがデータに対して想定する性質や役 割を表す．そのため，変数が満たしたアサーションの述語を求めることで，変数が果たす役割も明らかにすることができると思われる．
本論文では，Flanagan が Scheme プログラムのために定義した Set-based Analysis という解析手法を用いてプログラム内の各式の間に成り立つデータフローを静的に計算し，そのデータフローに沿って述語を伝播させることで，変数のとる値を説明するような述語の集合を求めて不変条件を計算する手法について述べる．加えて，この手法を実装した解析ツールを実際にバグのあるプログラムに適用する例を挙げて，その有用性を示す．
[研究室内部向け情報]