| 研究課題/領域番号 |
16K00091
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| 研究分担者 |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| キーワード | 書き換えシステム / プログラム検証 |
|---|
| 研究実績の概要 |
書き換えシステムに基づくプログラム検証手法を開発することを目的として研究を進めた。本年度の主な成果は、以下の通りである。
(1) 束縛変数を伴う書き換えシステムに基づく検証手法を開発するにあたって重要となる合流性に関して、以下の成果を得た。名目書き換えシステムについて研究代表者らの先行研究で得られていた合流性の判定基準を、危険対が存在する場合を含むいくつかのクラスに対する基準に拡張した。拡張された判定基準を合流性自動証明システムに実装し、さまざまな具体例による合流性判定の実験を行うことにより、その有効性を確認した。また、この合流性自動証明システムにおいて危険対生成と交差性判定の際に使用されている同変名目単一化の手続きを、推論規則の形で整理した。これらの理論的洞察と実証実験において得られた合流性や危険対に関する知見は、従来の書き換えシステムに基づく定理証明手法である完備化や帰納的定理証明手法である書き換え帰納法および潜在帰納法を、束縛変数を伴う書き換えシステムに基づく手法へ拡張するにあたって重要になると考えられる。
(2) 末尾再帰プログラムの性質の検証を容易にすることを目的としたプログラム変換である文脈移動変換については、以下の成果が得られた。十分完全性をもたない書き換えシステムに対する変換の正当性を定式化し、正当性が保証されるための条件を明らかにした。ここで取り扱った十分完全性をもたない書き換えシステムは、入力によって実行時エラーを発生する可能性があるプログラムに対応するため、本成果はそのようなプログラムに対する検証手法を開発するにあたって重要になると考えられる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
名目書き換えシステムにおける合流性の判定基準と危険対の交差性判定手続きについて、おおむね計画通りに研究を進めることができ、検証手法を開発するために有用と考えられるさまざまな知見が得られたため。
|
| 今後の研究の推進方策 |
束縛変数を伴う書き換えシステムに関して、名目書き換えシステム以外の関連する体系についても調査を進め、それぞれの体系の関係とそれらの体系に基づく検証手法の有効性を明らかにする。
|
| 次年度使用額が生じた理由 |
受領額と支出額の差引額は874円となり、ほぼ予定通りに使用された。
|
| 次年度使用額の使用計画 |
物品購入費の補充にあてる。
|
