| 研究概要 |
対話的定理証明による検証の事例研究及び,プログラム解析の研究を行った.
1.アルゴリズム検証の事例研究として,深さ優先探索の検証の精密化を行った.先行研究で深さ優先探索の検証を行ったが,下で述べるソフトウェアの検証を進める中でより精密に深さ優先探索の性質を検証する必要が生じた.そこで,深さ優先探索の各ステップが保存する性質をより精密に分析し,その検証を行った.
2.対話的定理証明によるソフトウェア検証では,プログラムの細かな性質を詳細に検証する必要がある.そのような細かな性質の検証を自動化するために,プログラム解析の研究を行った.具体的には,プログラムが出力しうる文字列の集合を文脈自由言語で近似するプログラム解析を開発した.さらに,このプログラム解析に基づきプログラムの性質を検査するため,XML言語,正則生垣言語と呼ばれる文脈自由言語のサブクラスについて,文脈自由言語との包含を決定するアルゴリズムを構築した.
3.ソフトウェアの精密な検証の事例研究として,2の研究で開発した決定アルゴリズムを検証する研究を行った.Isabelle/HOL上で文脈自由言語を形式化し,以下の三つの決定アルゴリズムの正しさを検証した.1)文脈自由言語と正則言語の包含を決定するアルゴリズム.2)与えられた文脈自由言語に属する語がすべて括弧に関してバランスがとれているか決定するアルゴリズム.3)文脈自由言語と正則生垣言語の包含を決定するアルゴリズム,さらに,Isabelle/HOL上で形式化したアルゴリズムから,実行可能な検査プログラムを自動生成し,実際のプログラム検査器の一部として使用可能であることを確認した.
|
