ソースコードを操作するプログラムの検証技法の研究

2022 Fiscal Year Research-status Report

• Project/Area Number: 19K20245
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: 森口 草介 東京工業大学, 情報理工学院, 助教 (60733409)
• Project Period (FY): 2019-04-01 – 2024-03-31
• Keywords: 形式検証 / メタプログラミング

Outline of Annual Research Achievements

本年は目立った進捗はないが、RAの学生とともにライブラリの構築を行った。このライブラリは現状クローズドソースであるが、発表成果の公開とともにオープンにする予定である。
本ライブラリは、主に関数リアクティブプログラミング言語におけるメタプログラミングを実現するために、二つのプログラムを表現し、一方が生成したプログラムでもう一方の実行プログラムを置き換える仕組みを表現している。
この仕組みはプログラムとして考えたときにはそれほど自明な挙動ではないが、本研究課題の提案する手法ではメタレベル（検証するシステム）がそれを担保するため、比較的高レベルな範囲で検証が可能である。また、それぞれのプログラムの挙動の記述自体ではメタレベルでの操作を必要としないため、元としている関数リアクティブプログラミング言語の意味論のみを利用し、特別なメタレベルでの意味論を必要としていない。この点で、本研究課題の手法が活用されている。

Current Status of Research Progress

4: Progress in research has been delayed.

Reason

研究担当者が行っているもう一方の課題の進捗を主として行ったため。

Strategy for Future Research Activity

これまでの成果を元に、論文発表を行う。また、構築したライブラリの公開のためにリファクタリングを行う。

Causes of Carryover

本年度は外部発表を行わなかったため、論文誌の掲載費用や学会への参加費用の使用額が想定より大きく下がったことによる。
今年度はこれらの費用に対する支出が主であるが、半年程度学生にRAを依頼し、共に論文のまとめに入る予定である。