| Project/Area Number |
19K20245
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
森口 草介 東京工業大学, 情報理工学院, 助教 (60733409)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2020: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2019: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | 形式検証 / メタプログラミング / 関数リアクティブプログラミング / 型システム / プログラム意味論 / プログラム検証 / 対話的証明支援系 |
|---|
| Outline of Research at the Start |
本研究では、ソースコードを入出力の対象とするプログラムの検証手法を提案し、検証システムが実現できることを実証する。プログラムが意図通りに動作することを確かめるプログラム検証手法が多く提案されているが、検証するプログラムが利用するデータは数値が主である。本研究の対象とするプログラムは、他のプログラムの構築を助けたり、プログラムの分析をするものであり、本研究での検証により一般に開発されるプログラムの信頼性の向上が期待できる。
|
| Outline of Annual Research Achievements |
本年は目立った進捗はないが、RAの学生とともにライブラリの構築を行った。このライブラリは現状クローズドソースであるが、発表成果の公開とともにオープンにする予定である。
本ライブラリは、主に関数リアクティブプログラミング言語におけるメタプログラミングを実現するために、二つのプログラムを表現し、一方が生成したプログラムでもう一方の実行プログラムを置き換える仕組みを表現している。
この仕組みはプログラムとして考えたときにはそれほど自明な挙動ではないが、本研究課題の提案する手法ではメタレベル（検証するシステム）がそれを担保するため、比較的高レベルな範囲で検証が可能である。また、それぞれのプログラムの挙動の記述自体ではメタレベルでの操作を必要としないため、元としている関数リアクティブプログラミング言語の意味論のみを利用し、特別なメタレベルでの意味論を必要としていない。この点で、本研究課題の手法が活用されている。
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
研究担当者が行っているもう一方の課題の進捗を主として行ったため。
|
| Strategy for Future Research Activity |
これまでの成果を元に、論文発表を行う。また、構築したライブラリの公開のためにリファクタリングを行う。
|
Report
(4 results)
Research Products
(10 results)
