TOP > 研究報告検索 > メタレベル・プログラミングの信頼性

メタレベル・プログラミングの信頼性

研究報告コード R070000219
整理番号 R070000219
掲載日 2008年4月11日
研究者
  • 亀山 幸義
研究者所属機関
報告名称 メタレベル・プログラミングの信頼性
報告概要 コンピュータ上でプログラムを実行するとき、プログラムのコード自身のほかに、環境や制御などの情報を利用します。環境は、変数とその値の対応であり、制御はプログラムカウンタ、すなわち、次に実行するプログラム中の番地の情報です。環境や制御は、通常のプログラム言語では、プログラムから直接操作可能な対象物ではなく、直接操作ができないレベル(メタレベル)にあるもの、すなわち、メタレベルの概念です。メタレベル概念をプログラムの中から直接操作する機能、つまり、『メタレベル機構』を使うことにより、従来は極めて複雑な記述が必要だったプログラムを、簡潔にわかりやすく記述できることが知られており、研究されてきました。しかし、プログラム言語の安易な拡張は信頼性を損ねる可能性があります。たとえば、メタレベル機構より更に強力なものとして、プログラムの『自己反映』があります。これは、インタープリタなどの言語処理系をプログラムの中から変更できるため、「どんな計算でも出来る」機構となっており、静的な解析や検証をすることが困難です。本研究は、メタレベル機構による高機能性・高記述性を、高信頼性と両立させた形で利用できるようにすることを目標としました。ここでポイントとなるのは、考察の対象とするメタレベル機構を、通常のプログラム言語の意味論に即した概念に対応するもののみに限定することです。このような概念は、自己反映計算のような無制限の拡張と異なり、拡張した言語の意味を、元の言語の意味から構築できると言う利点があります。本研究では、このように、意味論の助けを借りて、形式的体系によるモデリングと、それに対する検証方法の確立を行うことを日的としました。本研究では、応用上重要なメタレベル機構として、精細な制御を実現する限定継続(delimited continuation)とその発展形、および、メタ変数と文脈を取り上げて、この目的を達成するための研究を行いました。
画像

※ 画像をクリックすると拡大します。

R070000219_01SUM.gif R070000219_02SUM.gif
研究分野
  • システムプログラミング一般
関連発表論文 (1) Yukiyoshi Kameyama, Peter J. Stuckey (editors), FLOPS 2004 Proceedings, Lecture Notes in Computer Science Volume 2998, Springer, 307 pages, April, 2004.
(2) Yukiyoshi Kameyama, Masahiko Sato,“Strong Normalizability of the Non-deterministic Catch/Throw Calculi”, Theoretical Computer Sciencc 272(1-2), pp. 223-245, 2002.
(3) Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama,“A Simply Typed Context Calculus with First-Class Environments”, Journal of Functional and Logic Programming 2002(4) , pp. 1-41, 2002.
(4) Azza A. Taha, Masahiko Sato, Yukiyoshi Kameyama, “A Second Order Context Calculus”, コンピュータソフトウェア 19 : 3, pp. 2-19, 2002.
(5) 中島一,亀山幸義,「抽象化と精密化による実時間モデル検査の改善」,情報処理学会論文誌:プロウグラミング Vol. 45, No.SIG12 (PRO23), pp. 11-24, 2004.
(6) Yukiyoshi Kameyama, Masahito Hasegawa,“A Sound and Complete Axiomatization for Delimited Continuations”, Proc. Eighth ACM International Conference on Functional Programming (ICFP'03), pp. 177-188, 2003.
(7) Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama, Atsushi Igarashi,“Calculi of Meta-Variables”, Proc. 17th International Workshop on Computer Science Logic (CSL'03) , Lecture Notes in Computer Science Volume 2803, pp. 484-497, 2003.
(8) Yukiyoshi Kameyama,“Axiomatizing Higher-Level Delimited Continuations”, Proc. Fourth ACM-SIGPLAN Continuation Workshop (CW'04), pp. 49-53, 2004.
(9) Yukiyoshi Kameyama,“Axioms for Delimited Continuations in the CPS Hierarchy”, Proc. Annual Conference of the European Association for Computer Science Logic (CSL'04), Lecture Notes in Computer Science Volume 3210, pp. 442-457, 2004.
(10) Yukiyoshi Kameyama, “Dynamic Control Operators in Type Theory”, Second Asian Workshop on Programming Languages and Systems, Daejon, Korea, Dec., 2001.
(11) Yukiyoshi Kameyama,“Partial Continuation and CPS-Translation”, Workshop on Foundation of Software, Hangzhou, China, Sep., 2003.
(12) 亀山幸義,中島一,『ケーススタディ:モデル検査と定理証明を用いた信号制御システムの検証』,システム検証の科学技術シンポジウム,産業技術総合研究所システム検証研究ラボ,2004年2月.
研究制度
  • 戦略的創造研究推進事業 さきがけタイプ(旧若手個人研究推進事業を含む)/機能と構成
研究報告資料
  • 亀山 幸義. メタレベル・プログラミングの信頼性. 個人型研究(さきがけタイプ)情報・知能分野 研究報告会 先進情報システムとその構成に向けて 「機能と構成」領域 講演要旨集 第Ⅱ期研究者(研究期間2001-2004), 2004. p.23 - 31.

PAGE TOP