| 研究課題/領域番号 |
22K17875
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2022年度)
|
| 配分額 *注記 |
4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2024年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2023年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2022年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | プログラミング言語 / 型システム / 計算効果 / 時相的検証 / 形式検証 |
|---|
| 研究開始時の研究の概要 |
高信頼ソフトウェアの実現には状態管理が必要な様々な機能群（計算効果）に対応したプログラム検証技術が必要となる．本研究課題では計算効果の正しい使い方を表わす時相的性質と，プログラムの状態に関する状態依存的性質を検証するための新たな型システムについて研究を行う．これらの性質を検証することで，プログラムが計算効果を正しく使用しているか，プログラムが計算効果の正しい状態を保持しているかが検証可能となる．
|
| 研究実績の概要 |
2022年度は限定継続演算子を利用するプログラムの時相的性質を検証するための手法について研究を行った。限定継続演算子は限定継続と呼ばれる、一種のプログラム文脈を値として取り出すことのできる命令で、これを利用することで例外、バックトラック、ジェネレーターなどの、計算効果を引き起こす様々なプログラミング機能が実装できることが知られている。そのためこの命令を扱えるような検証手法を与えることで、上記に挙げたプログラミング機能を利用するプログラムの性質を検証することが可能となる。2022年度はshift0/resetと呼ばれる限定継続演算子に対し、時相的性質を検証するための型理論を構築し、検証手法実装への足がかりを掴んだ。
また今回の手法を応用することで、エフェクトハンドラと呼ばれる別種の限定継続演算子に対して依存篩型による正確な検証を可能にする型理論を構築することにも成功した。
さらに限定演算子の利用を前提とした時相的検証の研究を通して、より一般的な再帰型を用いるプログラムを対象とした時相的検証に関する知見を得ることができた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
本年度では当初の計画通り、限定継続演算子を対象とした時相的性質の検証のための型理論が構築できた。またその際のアイディアが、時相的検証のみならず篩型によるプログラムの正確な安全性検証にも利用できる点、さらにはより一般的な再帰型を利用するプログラムに対する時相的検証を行うための知見を得た点は、当初想定していた以上の進展である。
|
| 今後の研究の推進方策 |
今後の研究ではこれまでに構築した型理論を基にしたプログラム検証手法の実装や、状態に依存する性質を検証するための型理論の構築に取り組む。
|
