氏名: 大塚 正人 (m06735)
論文題目: 代数的仕様の検証自動化に関する研究
論文概要
プログラムの検証の技術はソフトウェアの信頼性を保証するための
基礎技術として重要である。プログラム検証の自動化や機械的支援
に適した形式的仕様記述法として代数的仕様記述法があり、その記
述法で書かれた仕様を検証する様々な方法が研究されている。代数
的仕様の検証は、仕様の意味する代数が等式で与えられる性質を満
たしているかどうかを調べることで行われる。仕様が等式集合であ
り、仕様の意味する代数が仕様のモデルのクラスの始代数であると
きは、仕様の検証は帰納的定理の証明に帰着する。帰納的定理の証
明法の代表的なものとして、構造帰納法やその拡張である被覆集合
帰納法がある。本論文では、帰納法を行うときに用いる仮定を定め
る大小関係に、従来の被覆集合帰納法と比較してより多くの仮定を
用いることができるような文脈消去関係を提案し、これをもとにし
た被覆集合帰納法の原理を示し、その健全性を証明する。また、従
来の被覆集合帰納法で証明できる帰納的定理は本方法でも証明でき
ること、および、従来の方法で証明できないが本方法では証明でき
る実例があることを示し、本論文の被覆集合帰納法の有効性を明ら
かにする。
目次に戻る