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

操纵源代码的程序验证技术研究

• 批准号: 19K20245
• 负责人: 森口 草介
• 金额: $ 2.25万
• 依托单位: Tokyo Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Early-Career Scientists
• 财政年份: 2019
• 资助国家: 日本
• 起止时间: 2019-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-19K20245/
• 关键词: 形式検証; メタプログラミング; 関数リアクティブプログラミング; 型システム; プログラム意味論; プログラム検証; 対話的証明支援系

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

This year's event is scheduled to be held in Beijing. The status quo of the project is discussed in detail below. The main content of this article is: 1. The main content of this article is: 1. This paper presents a proposal for the research topic of the present study, which is based on the analysis of the results of the study and the comparison of the results. The description of the movement of the language itself is necessary for the operation of the language, especially for the meaning of the language. This paper discusses the application of the methods of this research topic.

项目成果

小規模組込みシステム向けFRP言語のための再帰データ型

用于小型嵌入式系统的 FRP 语言的递归数据类型

• 发表时间: 2021
• 作者: 横山陽彦;森口草介;渡部卓雄
• 通讯作者: 渡部卓雄

小規模組込みシステム向けFRP言語における周期的タスクの記述方式

小型嵌入式系统FRP语言周期性任务描述方法

• 发表时间: 2021
• 作者: 辻裕太;森口草介;渡部卓雄
• 通讯作者: 渡部卓雄

関数リアクティブプログラミングにおける時変値の初期値の自動決定

函数式反应式编程中时变值初始值的自动确定

• 发表时间: 2021
• 作者: 白鳥佑弥;森口草介;渡部卓雄
• 通讯作者: 渡部卓雄

Functional Reactive Programming for Embedded Systems with GPGPUs

使用 GPGPU 的嵌入式系统的函数式反应式编程

• 发表时间: 2021
• 作者: Yoshitaka Sakurai;Sosuke Moriguchi;Takuo Watanabe
• 通讯作者: Takuo Watanabe

関数リアクティブプログラミング言語のための時間制約付きイベントの記述方式

函数反应式编程语言的时间约束事件描述方法。

• 发表时间: 2021
• 作者: 堀紗知子;森口草介;渡部卓雄
• 通讯作者: 渡部卓雄