氏名: 木村 正人 (m953413)
論文題目: 並行オブジェクト指向プログラムに対する合成的テスト等価性
論文概要
並行オブジェクト指向プログラムの実行モデルでは、複数のオブジェクト
が並行的にメッセージを交信することで計算が進行する。
各オブジェクトはそれぞれ状態を持ち、メッセージを受理することで自分
自身の状態を変化させる。オブジェクトは状態によって、受理できるメッ
セージの種類や数が異なるので、受理されないメッセージが残ってしまう
というエラーが発生することがある。このようなエラーの静的な検出は、
メッセージの到着順序の非決定性のために、逐次的なオブジェクト指向プ
ログラムの場合に比べてより難しい問題となっている。
本研究の目的は、並行オブジェクト指向プログラムの実行の際にオブジェ
クトに送信されたメッセージがすべて受理されるかどうかを静的に検査す
る手法を開発することである。
本研究では、まずメッセージに対するオブジェクトの振舞いを定式化する。
その際、並行オブジェクト計算に対して、（同様に並行計算の非決定性を
扱っている）プロセス代数の概念であるテスト原理['88 Heennessy]を導入
して、オブジェクト集合OとメッセージのマルチセットMに対して以下
の値を返す関数Result(M,O)を与える。
Result(M,O)=
{Ｔ} すべてのメッセージを必ず受理できるとき
{Ｔ,⊥} すべてのメッセージを受理することもあるとき
{⊥} すべてのメッセージを受理することはないとき
並行オブジェクト指向プログラムは、オブジェクト集合に対してメッセー
ジのマルチセットを送信することで計算が始まるので、この関数を用いて
プログラムのエラー検出を行なうことができる。
次に、これを用いて、テスト等価性、すなわち、メッセージに対する振舞
いが同じであるというオブジェクト間の等価関係を定義し、テスト等価性
は和集合演算に対して合同性を持つことを証明する。この結果は、テスト
等価性がオブジェクト集合の等価性に拡張できることを意味する。そして、
拡張されたテスト等価性は、メッセージに対する振舞いが等しいという意
味での並行オブジェクト指向プログラムの等価性、及び、その検証技法に
基礎を与える。
また、オブジェクト指向言語において一般的な概念であるクラスの概念
を本論文で提案する意味論に基づいて定式化する。
目次に戻る