| 研究課題/領域番号 |
20K11743
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
西崎 真也 東京工業大学, 学術国際情報センター, 教授 (90263615)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| キーワード | 関数プログラミング / プログラミング言語理論 / call/cc / 制御捕獲 / 継続 |
|---|
| 研究実績の概要 |
研究課題「制御捕獲のモデル化と応用」では、新たな計算モデルの開発とソフトウェア検証手法の確立に焦点を当てている。ここでいう「制御捕獲」とはプログラムの制御流を捕獲する機構である。例えば、JavaのfinallyブロックやSchemeのdynamic-windがそれにあたる。本研究課題では、ラムダ計算を基盤とした新しい計算モデルを構築している。このモデルは関数型言語だけでなく、命令形言語やオブジェクト指向言語にも適用可能であると考えられている。例外処理や大域脱出の数学的形式化を通じて、制御捕獲の理論的理解を深めることを目指している。
前年度までの研究成果を踏まえ、計算モデルの再検討とソフトウェア検証手法の充実を行った。さらに、制御捕獲機能を備えた言語の例外処理機構に対する新たなソフトウェア検証手法を開発をおこなっている。この手法はプログラムの信頼性と安全性を向上させることを目的としており、特に複雑な入出力処理や例外処理が絡む場面での有効性が期待されると考えられる。
本研究の研究成果により、プログラミング言語理論における制御捕獲の新たな理論的理解がなされるであろう。そして、制御捕獲を含まない言語への導入指針が得られ、ソフトウェア検証の方法論の進展にも寄与すると考えられる。2023年度においては特に、catch-and-throwとunwind-protectのしくみ、及び、call/ccとdynamic-windの仕組みに関して、計算モデルの基盤の精密化をおこなった。そして、それをもととして、ソフトウェア検証手法の検討を行った。これが2023年度の重要な研究実績である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
コロナ禍が終わり順調に研究は進捗している。
|
| 今後の研究の推進方策 |
制御捕獲のモデル化と応用に関する今後の研究推進方策として、以下の具体的なステップを提案する。まず、制御捕獲のしくみに関して、これまでの計算モデルを総括的にまとめることが重要である。このプロセスでは、ラムダ計算を基にした現行のモデルを精緻化し、さらにその理論的枠組みを強化する。この段階で、関数型、命令形、オブジェクト指向言語の各パラダイムにおける制御捕獲機構の振る舞いと効果を明確に分析し、それぞれの言語特性に応じたモデルの適合性を評価する。
次に、ソフトウェア検証手法に関しては、開発したモデルを用いて検証プロセスの効率化と精度向上を図る。具体的には、新しい検証手法を制御捕獲機能を持つ言語の例外処理機構に適用し、その有効性を実際のソフトウェア開発プロジェクトで試験する。この試験を通じて、手法の実用性と拡張性を検証し、必要に応じてモデルや手法の改善を行う。
以上の研究推進方策は、制御捕獲の計算モデルとソフトウェア検証手法の両方において、より広範な理解と応用を目指すものである。このアプローチにより、プログラミング言語理論の進展とともに、ソフトウェア開発の現場での安全性と信頼性を大きく向上させることが期待される。
|
| 次年度使用額が生じた理由 |
次年度使用額が生じた理由としては、新型コロナウイルス感染症の影響が挙げられる。特に研究成果の発表や実装作業において顕著であった。世界的なパンデミックの影響により、国際会議の開催が中止またはオンライン形式に移行されることが多く、対面での研究成果の交流が困難となった。また、研究機関や実験施設の閉鎖、移動制限により、計画していた研究活動がスケジュール通りに進行できなかったことが、使用額の繰り越しにつながった。
次年度の使用計画については、これらの遅延が解消される見込みである。まず、国際会議への参加や研究成果の発表機会を再度確保することに予算を充てる計画である。さらに、研究実施のための新たな機材購入や追加的なデータ収集にも資金を投じる予定である。これにより、コロナ禍で停滞した研究の進捗を加速させ、計画していた成果を確実に達成することが目標である。
|
