氏名: 宅見 貴代 (m05768)

論文題目: 書換え計算モデルに基づくプログラム検証系の実現に関する研究

論文概要

プログラムの等価変換や検証は、計算の表現であるプログラムをデータとして操作・処理するものであり、メタ計算と呼ばれている。このようなメタ計算に、もし誤りがあれば、誤りのあるプログラムを大量に作り出すことになったり、また、信頼性の保証の基礎を危うくするなど、ソフトウェアの信頼性に重大な影響を与える。したがって、メタ計算の信頼性を確保するための技術を開発することは重要である。このような観点から、メタ計算を記述し、それを検証するための枠組を与えることを目的として、項の書換えを基本ステップとする計算モデル：メタ項書換え計算(Metaterm Rewriting Calculus, MRC)が提案されている。

本研究では、プログラム検証というメタ計算をMRCによって記述し、その記述が正しくプログラム検証を実現していることを証明する手法を開発することを目的として、具体的なプログラム検証系であるHoare logicをMRCで記述し、その正しさを証明する。また、MRCプログラムの検証手法について考察する。

目次に戻る