氏名: 二井靖彦 (089333489)

論文題目: オブジェクト指向プログラムによる抽象データ型実現の 正当性検証法に関する研究


論文概要

データの集合とその上の演算からなる抽象データ型は、インスタン ス変数とメソッド定義からなるオブジェクト指向言語におけるクラ スの概念に自然に対応するので、オブジェクト指向プログラムによっ て抽象データ型を実現することは自然な考えである。このことから、 オブジェクト指向言語の意味論を代数的に記述し、その上で、代数 的に仕様記述された抽象データ型を実現するオブジェクト指向プロ グラムの検証を代数的な手法を用いる、という検証の枠組が提案さ れている[1]。本研究では、上記の枠組において、文脈帰納法と呼 ばれる帰納法によってオブジェクト指向プログラムが抽象データ型 の観測的実現であることを証明する手法を検討し、その評価を行な う。
[1] R.Hennicker and C. Schmits: "Object-Oriented Implementation of Abstract Data Type Specifications", Proc. AMAST '96, LNCS 1101, pp.164--179, 1996
目次に戻る