2016 Fiscal Year Research-status Report
文脈移動変換と高階書き換え理論に基づくプログラム検証法の研究
| Project/Area Number |
16K00091
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 書き換えシステム / プログラム検証 |
|---|
| Outline of Annual Research Achievements |
書き換えシステムに基づくプログラム検証手法を開発することを目的として研究を進めた。本年度の主な成果は、以下の通りである。
(1) 束縛変数を伴う書き換えシステムに基づく検証手法を開発するにあたって重要となる合流性に関して、以下の成果を得た。名目書き換えシステムについて研究代表者らの先行研究で得られていた合流性の判定基準を、危険対が存在する場合を含むいくつかのクラスに対する基準に拡張した。拡張された判定基準を合流性自動証明システムに実装し、さまざまな具体例による合流性判定の実験を行うことにより、その有効性を確認した。また、この合流性自動証明システムにおいて危険対生成と交差性判定の際に使用されている同変名目単一化の手続きを、推論規則の形で整理した。これらの理論的洞察と実証実験において得られた合流性や危険対に関する知見は、従来の書き換えシステムに基づく定理証明手法である完備化や帰納的定理証明手法である書き換え帰納法および潜在帰納法を、束縛変数を伴う書き換えシステムに基づく手法へ拡張するにあたって重要になると考えられる。
(2) 末尾再帰プログラムの性質の検証を容易にすることを目的としたプログラム変換である文脈移動変換については、以下の成果が得られた。十分完全性をもたない書き換えシステムに対する変換の正当性を定式化し、正当性が保証されるための条件を明らかにした。ここで取り扱った十分完全性をもたない書き換えシステムは、入力によって実行時エラーを発生する可能性があるプログラムに対応するため、本成果はそのようなプログラムに対する検証手法を開発するにあたって重要になると考えられる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
名目書き換えシステムにおける合流性の判定基準と危険対の交差性判定手続きについて、おおむね計画通りに研究を進めることができ、検証手法を開発するために有用と考えられるさまざまな知見が得られたため。
|
| Strategy for Future Research Activity |
束縛変数を伴う書き換えシステムに関して、名目書き換えシステム以外の関連する体系についても調査を進め、それぞれの体系の関係とそれらの体系に基づく検証手法の有効性を明らかにする。
|
| Causes of Carryover |
受領額と支出額の差引額は874円となり、ほぼ予定通りに使用された。
|
| Expenditure Plan for Carryover Budget |
物品購入費の補充にあてる。
|
-
-
-
-
[Presentation] ACPH: System Description for CoCo 20162016
Author(s)
Kouta Onozawa, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
Organizer
The 5th International Workshop on Confluence (IWC 2016)
Place of Presentation
Obergurgl University Center, Austria
Year and Date
2016-09-08 – 2016-09-09
Int'l Joint Research
-
