フォーマルメソッドとオブジェクト指向技術はソフトウエアの生産性と品質を向上させる2つの主要な技術であり、1970年代初頭からの長い歴史を持つ。オブジェクト指向技術はプログラムの構成法や対象問題のモデリング技法を中心とし、実用的な見地からのフィードバックを得た結果、産業界で不可欠な技術となっている。一方、フォーマルメソッドは、基礎的な研究の段階にあり、未だ、日常のソフトウエア開発で用いられる段階に至っていない。両者を融合することで、より良い開発技術を実現できる可能性がある。

　オブジェクト指向技術の中心概念はオブジェクトであるが、広範な技術を含む複合性に特徴がある。情報隠蔽、多相性、継承、というオブジェクト指向パラダイムの基本概念をベースに、オブジェクト指向フレームワークやコンポーネントと呼ぶ再利用アーキテクチャならびにオブジェクト指向分析設計方法論を含み、産業界で重要な位置を占めるに至った。ここで、オブジェクト指向フレームワークは複数の構成オブジェクトが協調して一連の機能を提供する部品である。情報隠蔽、多相性、継承、という基本機構を組み合わせることで実現可能となるので、オブジェクト指向ソフトウエアの特徴をよくあらわしている。プログラムの構造的な側面に主眼を置くことで高い再利用性を実現する基本的な技術であるため産業界での重要性が大きい。

　フォーマルメソッドの一分野である代数仕様技術は、データ抽象概念を基礎とし、ソフトウエアシステムを代数としてモデル化する。データ抽象とオブジェクトは共に1960年代に考案されたプログラミング言語SIMULAが源にある。また、代数仕様技術は指標(シグネチャ)と呼ぶ概念によって、ソフトウエアコンポーネントのインタフェースを厳密に表現する手法を提供した。指標を用いると、オブジェクトの外部からみた性質を規定することができる。以上より、フォーマルメソッドとオブジェクト指向技術を融合するアプローチとして代数仕様技術が有力である。しかし、代数仕様技術は、理論的な側面や言語設計の基礎的な研究が中心であり、実用的な言語や仕様作成支援ツールが少ない。Z記法やVDMならびにBメソッド等と比較して、適用実績に欠けるため産業界での実用性が疑問視されているという問題がある。

　本稿では、Futatsugiによる代数仕様言語CafeOBJ/CAFE環境を用いて、実用的なオブジェクト指向ソフトウエア開発に代数仕様技術を適用する研究を報告する。代数仕様技術を実用化する上での3つの課題に対して4つの方向から具体的に議論する(第3章〜第6章)。すなわち、(a)広範な設計モデルを表現することが可能か、(b)大規模仕様を得る際のモジュール分割ガイドラインは何か、(c)既存開発技術と融合した開発プロセス/管理はどうあるべきか?、という3つの課題を考察する。

　第2章では、既存研究を概観することで本研究の背景をまとめ、オブジェクト指向フレームワーク開発に代数仕様技術を適用することの重要性を述べる。

　第3章では、CafeOBJを用いたオブジェクト仕様表現の基礎技術として、MeseguerによるMaude並行オブジェクトモデルの実現方法を述べる。次いで、MaudeモデルとCardelliとGordonによるAmbient Calculusとを統合する方法を提案する。これにより、協調動作を行なうなど強く関連する複数のオブジェクトをまとめて操作対象とすることがはじめて可能になる。応用として、複数オブジェクトが共有する資源の排他制御や、移動分散ソフトウエアのアーキテクチャ仕様記述が容易になることを示す。課題(a)に関連すると同時に、以降の仕様作成で必要となる基本的な表現手法を与える。

　第4章では、CafeOBJによるオブジェクト仕様表現とシナリオ中心モデリング技法とを融合する手法を提案する。シナリオ中心モデリングでは、システム全体が持つ機能を分析して構成オブジェクトの抽出を行なった後、構成オブジェクト間の相互作用をもとに個々のオブジェクト機能を求める。本研究では、このモデリング技法とCafeOBJのギャップを埋める中間的な設計記法GILOを提案する。GILOの導入によりはじめて、実行可能なCafeOBJ記述を得る系統的な手法が明確になる。中規模問題への適用例として、「酒屋在庫管理問題」を対象とするケーススタディを行ない、モデリングからGILOを経て系統的にCafeOBJ記述を得る過程を具体的に示す。課題(a)(b)(c)に関連する。

　第5章では、標準勧告文書へのCafeOBJ適用手法を考察する。ITU-T等の標準勧告は整合性や厳密さが要求されることから、フォーマルメソッドの重要な適用分野の一つであった。本研究では、ITU-TとOMGが共同で策定したODPトレーダ文書記載の仕様をCafeOBJで記述する。種々の観点からツールによる解析が可能なため、ODPトレーダ仕様の理解を助けることができる。また、ODPトレーダ仕様は多様な性質からなるため、従来は複数の異なる仕様言語を用いる必要があると考えられていた。本研究では、単独の言語CafeOBJで、その多様さをカバーできることをはじめて示した。課題(a)(b)に関連する。

　第6章では、ODPトレーダサーバをオブジェクト指向フレームワーク技術で構築する開発過程でCafeOBJを用いる方法を提案する。本ケーススタディは、ODPトレーダサーバの分析段階からJavaを用いたプログラム開発段階までの開発ライフサイクル全体を扱う。代数仕様技術とオブジェクト指向フレームワーク構築を統一的に議論したはじめての試みである。そのために、トレーダサーバの本質的な設計モデルを導く問題依存の設計技法を提案する。本設計技法では、複雑なODPトレーダ機能を高い独立性を持つ複数の設計アスペクトに分割し、各々の設計アスペクトの結果モデルをCafeOBJで記述する。その結果、設計結果モデル記述をCafeOBJ/CAFE環境を用いて解析することが可能になり、設計品質の向上に寄与する。その後、設計結果モデル記述を入力仕様として、既存のオブジェクト指向設計やデザインパターンを用いることでJavaを用いたオブジェクト指向フレームワークを構築する。また、開発過程モデルや開発管理といった日常開発業務で重要となる側面とフォーマルメソッドの関係について、CafeOBJを用いた本開発事例をもとにして具体的に議論する。課題(a)(b)(c)に関連する。

　最後に、本研究の成果をまとめ、今後の研究課題を報告する。

　本論文では,オブジェクト指向ソフトウエアの系統的な開発方法について,フォーマルメソッドのひとつである代数仕様技術を用いた新しい枠組みを提示している.

　フォーマルメソッドとオブジェクト指向技術は,ソフトウエアの生産性と品質を向上させる2つの主要な技術であり,1970年代初頭から独立に発展してきた.両者を融合することで,フォーマルメソッドが持つ厳密さや系統性と,オブジェクト指向技術が示す実用性の双方の長所を合わせ持つ設計技術を確立する研究が,注目を集めている.しかし,形式仕様言語の設計や検証を伴う段階的な詳細化技術の開発といった理論的な研究が多く,オブジェクト指向技術が持つ多様さを考慮したソフトウエア工学の観点からの実用的な研究が遅れているという現状がある.

　本研究では,二木による代数仕様言語CafeOBJ/CAFE環境を用いて,実用的なオブジェクト指向ソフトウエア開発に代数仕様技術を適用する系統的な開発方法を提案している.これは論文提出者が企業でのソフトウエア開発経験に基づいて工夫したものであり,産業界における代数仕様技術利用に先鞭をつける実践的な成果となっている.

　本論文の第1章では,上述の研究の動機や目的を述べている.第2章では,研究動向を概観し,オブジェクト指向フレームワーク開発に代数仕様技術を適用することの重要性を述べている.

　第3章では,CafeOBJを用いたオブジェクト仕様表現の基本技術として,MeseguerによるMaude並行オブジェクトモデルのCafeOBJによる実現方法を簡潔に述べている.さらに,MaudeモデルとCardelliとGordonによるAmbient Calculusとを統合する方法を提案している.この方法により,オブジェクト指向フレームワークの構成オブジェクトのように強く関連する複数のオブジェクトを,まとめて操作対象とすることが可能となる.本章の結果は,以降の章で仕様記述を行う際に用いられる表現手段を与えるものである.

　第4章では,CafeOBJによるオブジェクト仕様表現とシナリオ中心モデリング技法とを融合する一手法を,提案している.特に,シナリオの考え方とCafeOBJのギャップを埋める中間的な設計記法GILOを提案した点に,新規性がある.中規模問題への適用例として,「酒屋在庫管理問題」を対象とするケーススタディを行い,モデリングからGILOを経て系統的にCafeOBJ記述を得る過程を具体的に述べて,提案手法の有効性を示している.

　第5章では,標準勧告文書へのCafeOBJ適用手法を述べている.ITU-T等の標準勧告は整合性や厳密さが要求されることから,フォーマルメソッドの重要な適用分野の一つであるが,代数仕様技術の適用例はこれまで報告されていない.本研究では,分散サービスとして実用上重要なODPトレーダ文書記載の仕様を,CafeOBJで記述している.ODPトレーダ仕様は多様な性質を規定しているため,従来はその記述に複数の異なる仕様言語を用いる必要があると考えられていた.本研究は,単一言語でその多様さをカバーできることを初めて示し,標準勧告文書の記述や分析にCafeOBJが有効であることを実証した点に新規性がある.

　第6章では,CafeOBJを用いた問題依存の設計技法として設計アスペクトに基づく方法を提案し,ODPトレーダサーバ構築にその設計技法を適用した結果を示す.開発上流工程で,モジュラリテイの高い6つの設計アスペクトからなるグローバルデザインを作成し,デザイン記述をCafeOBJを用いたオブジェクト指向代数仕様として表現する.その結果,デザイン記述をCAFE環境を用いて解析することが可能になり,設計品質の向上がもたらされる.その後,デザイン記述を入力仕様とし,さらにデザインパターン等の既存技術を用いることで,Java言語によるオブジェクト指向フレームワークを構築している.これは代数仕様技術を,プログラム作成までのオブジェクト指向開発過程全体に結びつけて統一的に議論した初めての試みであり,さらに開発管理といった実用上考慮すべき点にも言及していることは評価できる.

　第7章では,本研究の成果と残された課題について総括している.

　代数仕様技術は,産業界で重要なオブジェクト指向技術との親近性を指摘されながら,長く理論的な側面や言語設計に関する基礎的な研究が中心であった.そのため,他のフォーマルメソッドと比較して,ソフトウエア工学の観点から実用的な技術になり得るのかという疑問を持たれていた.本研究で示した開発手法は,理論的な側面に偏りがちであった代数仕様技術研究に一石を投じるものであり,学問上貢献するところが大きい.よって,本論文は博士(学術)の学位論文として相応しいものであると審査委員会は認め,合格と判定する.