|
本年度の研究成果は以下の通りである．
(1) Java ジェネリクスの中核部分に対する漸進的型付けの理論の構築．これまで型システムの構築と，その型システムの安全性の証明，そして型検査アルゴリズムの構築に取り組んできた．昨年度までの研究で，ほぼこれらの課題をクリアしていたが型検査で使われる部分型検査手続きの停止性が課題として残されていた．本年度，この停止性を証明し，型検査手続きが実際アルゴリズムであることを証明できた．これによって，漸進的型付け拡張を言語処理系に組込むための基盤理論が整ったといえる．
(2) Java の漸進的型付け拡張の実装の研究．特殊な仮想機械命令を使わない方式を使って(1)の課題が解決されなくても実装できる部分について実装を行った．対象は OpenJDK コンパイラで，ジェネリクスの関わらない部分についてはコンパイラの局所的な変更で実現できることがわかった．理論でカバーした範囲全ての実装は今後の課題として残された．
(3) 多相的契約言語に関する研究．前年度までの研究では，既に提案されていた体系を不動点演算子で拡張し，その性質を調べていたが，記述できるプログラムの種類に著しい制限が課した下であれば，よい性質が拡張後も保たれることがわかっていた．本年度は，この制限をなくすために体系の定式化を最初から見直し，参考としていたPittsの研究で使われていたA正規形を捨てることで制限が取りはらえることがわかった．このため体系定義が煩雑になるという問題があったが，最終的には拡張前のよい性質が拡張後も成立することが証明できた．この結果は，契約の動的検査であるキャストのうち，対象の型と検査の型が部分型関係にあるものはプログラムの挙動に影響を与えずに除去できる，というものである．
|
