氏名: 江場 雅彦 (289734088)

論文題目: 型のないオブジェクト指向プログラムの代数的意味記述に関する研究


論文概要

抽象データ型を実現するオブジェクト指向プログラムに対する正当性検証 の枠組みとして、オブジェクト指向言語の意味論を代数的に記述し、その 上でプログラムの検証を代数的に行なうことがHennicker等により提案され ている。また、そこで用いられるオブジェクト指向言語を継承機構などオ ブジェクト指向言語として基本的な機能を持ち、型宣言が不要なオブジェ クト指向言語TinyObjectに拡張する研究が大久保等により行なわれている。 この拡張によりオブジェクト指向的な機能を利用したプログラムに対して もこの枠組みでの検証が可能となっている。

しかしながら、大久保等によるTinyObjectの代数的意味記述の枠組みには 次のような問題点がある。

  1. 既存の検証機構に直ちに適用できない。
  2. プログラム記述量に比較して得られる意味記述の量が膨大に なる。
  3. TinyObjectの次の機能の意味記述が与えられていない。
本研究では上記の問題点を解決することを目的として、TinyObjectから CafeOBJへの変換手続きを与える。 1.の問題点に関しては仕様記述言語としてCafeOBJを用いることでその検 証機構が利用可能となる。2.については意味記述の構成面から冗長性を除 き、意味記述の量を削減できることを示した。3.については相互参照の問 題は意味記述の構成をプログラム単位にすることにより、残り2つの問題に は順序ソートの適用とメソッドの意味記述の改良により解決した。

目次に戻る


asakura@nuie.nagoya-u.ac.jp