| 研究課題/領域番号 |
20K11743
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
西崎 真也 東京工業大学, 学術国際情報センター, 教授 (90263615)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2023年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2022年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2021年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2020年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
|
|---|
| キーワード | 関数プログラミング / プログラミング言語理論 / call/cc / 制御捕獲 / 継続 / プログラム理論 / プログラミング言語 / 大域脱出 / 関数型プログラミング言語 / 型システム / ラムダ計算 / dynamic-wind / 制御捕捉 / 関数型言語 / 一級継続 / 例外処理 / 一級環境 / 制御構造 |
|---|
| 研究開始時の研究の概要 |
制御捕獲）は制御の流れを強制的に捕獲するしくみであり，Javaのfinallyブロック，Schemeのdynamic-windが代表的である。 そして，例外処理機構は，大域脱出 と制御捕獲により構成されている。この制御捕獲については理論的側面において未解明である。 本研究では，これまでの大域脱出・一級継続の研究結果を基盤として，制御捕獲の計算モデ ルを提案する。関数型言語の計算モデルであるラムダ計算を始めとして，様々なプログラミングパラダイムに対しても研究を進める。さらにその計算モデルを基盤として，制御捕獲機能を有する例外処理機構に対するソフトウェア検証手法と確立する。
|
| 研究実績の概要 |
研究課題「制御捕獲のモデル化と応用」では、新たな計算モデルの開発とソフトウェア検証手法の確立に焦点を当てている。ここでいう「制御捕獲」とはプログラムの制御流を捕獲する機構である。例えば、JavaのfinallyブロックやSchemeのdynamic-windがそれにあたる。本研究課題では、ラムダ計算を基盤とした新しい計算モデルを構築している。このモデルは関数型言語だけでなく、命令形言語やオブジェクト指向言語にも適用可能であると考えられている。例外処理や大域脱出の数学的形式化を通じて、制御捕獲の理論的理解を深めることを目指している。
前年度までの研究成果を踏まえ、計算モデルの再検討とソフトウェア検証手法の充実を行った。さらに、制御捕獲機能を備えた言語の例外処理機構に対する新たなソフトウェア検証手法を開発をおこなっている。この手法はプログラムの信頼性と安全性を向上させることを目的としており、特に複雑な入出力処理や例外処理が絡む場面での有効性が期待されると考えられる。
本研究の研究成果により、プログラミング言語理論における制御捕獲の新たな理論的理解がなされるであろう。そして、制御捕獲を含まない言語への導入指針が得られ、ソフトウェア検証の方法論の進展にも寄与すると考えられる。2023年度においては特に、catch-and-throwとunwind-protectのしくみ、及び、call/ccとdynamic-windの仕組みに関して、計算モデルの基盤の精密化をおこなった。そして、それをもととして、ソフトウェア検証手法の検討を行った。これが2023年度の重要な研究実績である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
コロナ禍が終わり順調に研究は進捗している。
|
| 今後の研究の推進方策 |
制御捕獲のモデル化と応用に関する今後の研究推進方策として、以下の具体的なステップを提案する。まず、制御捕獲のしくみに関して、これまでの計算モデルを総括的にまとめることが重要である。このプロセスでは、ラムダ計算を基にした現行のモデルを精緻化し、さらにその理論的枠組みを強化する。この段階で、関数型、命令形、オブジェクト指向言語の各パラダイムにおける制御捕獲機構の振る舞いと効果を明確に分析し、それぞれの言語特性に応じたモデルの適合性を評価する。
次に、ソフトウェア検証手法に関しては、開発したモデルを用いて検証プロセスの効率化と精度向上を図る。具体的には、新しい検証手法を制御捕獲機能を持つ言語の例外処理機構に適用し、その有効性を実際のソフトウェア開発プロジェクトで試験する。この試験を通じて、手法の実用性と拡張性を検証し、必要に応じてモデルや手法の改善を行う。
以上の研究推進方策は、制御捕獲の計算モデルとソフトウェア検証手法の両方において、より広範な理解と応用を目指すものである。このアプローチにより、プログラミング言語理論の進展とともに、ソフトウェア開発の現場での安全性と信頼性を大きく向上させることが期待される。
|
