2013 Fiscal Year Annual Research Report
信頼性の高いコード生成のためのプログラミング言語の実現
| Project/Area Number |
25280020
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
浅井 健一 お茶の水女子大学, 人間文化創成科学研究科, 准教授 (10262156)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 助教 (80569575)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | ディペンダブルコンピューティング / プログラミング言語 / プログラム生成 / ソフトウェア検証 |
|---|
| Research Abstract |
コード生成法は、一般的なプログラムから、特定の環境やパラメータに応じたプログラムを生成することにより、プログラムの実行性能を高める手法であり、本研究の目的は、コード生成法の信頼性を高めることである。初年度となる平成２５年度の主な成果は以下の３つである。
（１）効率的コード生成においては、純粋な関数型プログラムの範囲に留まらず、計算エフェクトを発生する仕組みを利用する必要があるが、その場合、生成されたコードが自由変数を持たないこと（安全性）を保証するのは困難な課題であった。本年度の研究では、Hasekll上のコード生成構成子ライブラリの形で、任意のモナディックな計算エフェクトを許しつつ、生成コードが一切の自由変数を持たない言語系を構築し、実装を与えることに成功した。ただし、このライブラリの安全性の厳密な証明は、今後の課題である。
（２）ＣＳＰは、計算結果をコードの中に埋め込む機能であり、実用的なコード生成言語には必須である。従来理論におけるＣＳＰの定式化は、非常に複雑な計算規則で与えられており、コード生成言語の実装とも対応していないという問題があった。今年度の研究では、ＣＳＰの自然かつ簡潔な定式化を与えることに成功した。これは、ＣＳＰの理解を深めるのに役立つとともに、今後のコード生成言語の設計における基本的な指針を与えると考えている。
（３）形式検証は、紙と鉛筆による証明に代わり、コンピュータが証明をチェックするものであり、人間の思い込みによる誤りを防ぐことができ、証明の信頼性を向上させる。本年度の研究では、コード生成の一種である型主導の部分計算プログラムに対して、その正当性を定理証明システムを用いて形式検証した。
|
| 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 |
研究計画の２年目は、初年度に得られた成果を有機的に統合し、１つのコード生成言語に対する信頼性向上の方策を得ることに力を注ぐ。このため、３研究機関に所属している研究メンバーが一堂に会して集中的に議論するミーティングを何度かもつとともに、大学院生等を含めたメンバー間の相互訪問の機会を増やすこととする。
|
| Expenditure Plans for the Next FY Research Funding |
本研究経費で雇用予定であった研究員の着任が遅れたこと、これに伴い、研究員が使用する機材も平成２６年度予算で購入することになったことの２つの理由により、予算の一部を平成２６年度に残すこととなったため。
研究員は平成２６年３月に着任しており、平成２５年度の剰余分は人件費および物件費として、平成２６年度に支出する予定である。
|
