2008 Fiscal Year Annual Research Report
ソフトウェア再利用性向上のための型理論に関する研究
| Project/Area Number |
18700026
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
五十嵐 淳 Kyoto University, 情報学研究科, 准教授 (40323456)
|
|---|
| Keywords | ソフトウェア / 安全性 / オブジェクト指向言語 / 型システム / 再利用性 / 軽量族多相 / 漸進的型付け |
|---|
| Research Abstract |
本研究では, オブジェクト指向プログラミング言語のための, 再利用性の向上をサポートする型システム技術を確立することを目指している.本年度の研究成果は以下のとおりである.
1. 軽量族多相の型理論的分析 : 昨年度行った軽量族多相の型理論分析に関する考察を深め, 雑誌論文としての出版を行った.
2. ThisTypeの理論の実用的側面からの発展 : ThisTypeはオブジェクトが自分自身のインターフェースを指すために使われる型概念であり, 軽量族多相と深い関係がある.しかしThisType, 軽量族多相ともに, オブジェクト指向言語の特徴であるdynamic dispatchと相性が悪く, 部分型を生かしたプログラミングを妨げている, という問題が指摘されてきた.我々は, この問題に対し, 型理論的な考察に基き, local exactization, nonheritable methodという言語機構による解決を提案した.提案機構を定式化し, 安全性の数学的証明を行った.
3. 漸進的型付けの枠組みの研究 : プログラム実行時に型エラーを検査する動的型付けと, プログラム実行前に型エラーを検査する静的型付けはそれぞれに長所・短所がある.我々はSiekとTahaによる, 両者の長所を活かすための漸進的型付け(gradual typing)の枠組みをJavaのようなオブジェクト指向言語に適用するための基盤理論を研究し, 動的型付け・静的型付けされるコードの混在を許しながらも, 実行時エラーは静的型付けされた部分からは発生しない, という型システムの構築に成功した.これは, 動的型付けされたコードを安全に再利用するための枠組みとして利用可能である.ただし, ジェネリクスを含む言語に関しては今後の検討課題として残つた.
|
