発展的ソフトウェアの理論に関する研究

1998 年度 実績報告書

• 研究課題/領域番号: 09245102
• 研究種目: 特定領域研究(A)
• 研究機関: 東北大学
• 研究代表者: 伊藤 貴康 東北大学, 大学院・情報科学研究科, 教授 (80124551)
• 研究分担者: 萩谷 昌己 東京大学, 大学院・理学研究科, 教授 (30156252) ; 米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286) ; 坂部 俊樹 名古屋大学, 大学院・工学研究科, 教授 (60111829) ; 井田 哲雄 筑波大学, 電子情報工学系, 教授 (70100047)
• キーワード: 発展的ソフトウェア / 発展的プログラミング機構 / ソフトウェア仕様記述 / 論理・関数型プログラミング / 書換え型メタ計算モデル / 実時間論理 / 検証系 / 検証情報

研究概要

発展的ソフトウェアの理論に関して、平成9年度の研究成果を踏まえて、次のような研究を行い、所期の研究成果を得た。
1. 発展的プログラミング機構の研究(担当:伊藤貴康):プログラム粒度に基づく適応的機構の理論を用いてプログラムの発展的改良を行える視覚的プログラミングツールPaiVisualizerを設計・試作すると共に、場所と時間の概念を導入した分散プログラミング言語をJAVAを基にして設計し、場所の概念を備えたJAVA言語については処理系の試作と評価も行った。
2. ソフトウェア仕様作成プロセス理論の研究(担当:井田哲雄):発展機構を取り入れた論理型・関数型プログラミングの理論研究を行い、等式付き書き換え系の停止性、条件付き遅延ナローイング計算系の合流性・完全性の結果を得た。また、制約解消機能を備えた関数論理型プログラミングシステムを作成した。
3. 書き換え型計算に基づく発展的ソフトウェアの基礎研究(担当:坂部俊樹):MRC(Meta-term Rewriting Calculus)の理論研究を行い、MRCの合流性定理を与えた。また、代数的仕様検証のための線形文脈帰納法を与えた。MRCの実行と解析を行う環境を動的弁別ネットを用いたMRCインタプリタを試作した。
4. 実時間環境のための発展的ソフトウェアの理論の研究(担当:米崎直樹):実時間が記述可能な新しい論理体系RTL-Qを構成し、その弱完全性を証明した。また、仕様からの適切な情報を推論する論理体系を与えた。実時間ソフトウェアの検証の立場から、欠陥仕様からの修正部分の抽出、仕様の分類とその判定法、グラフを用いた充足可能性判定のアルゴリズム等についての成果を得た。
5. 検証系の検証と検証情報の発展(担当:萩谷昌己):検証を行うソフトウェアである検証系について研究を行い、グラフ探索とモデル検査のアルゴリズムの与え、また、JAVAバイトコード検証系の検証法を与えた。検証情報の発展のための帰納的定義法とその抽象化、発展を支援するユーザインタフェースなどの研究を行い、理論的成果と共にシステム作成も行った。

研究成果

• [文献書誌] 三森哲、伊藤貴康: "PaiLispプログラミングのための視覚的ツールの試み" 情報処理学会プログラミング研究会資料. PRO18. (1998)
• [文献書誌] Takayasu Ito,Shin-ichi Kawamoto,Masayoshi Umehara: "A Multi-Threaded Implementation of PaiLisp Interpreter and Compiler Using the Steal-Help Evaluation Strategy" Advanced Lisp Technology in Japan,Information Processing Society of Japan,Gorden and Breach Press. (1998)
• [文献書誌] 大崎人士、Aart Middeldorp、井田哲雄: "等式付き書き換え系における多ソート不変性" コンピュータソフトウェア. Vol.16(1). 33-45 (1999)
• [文献書誌] Hirotaka Ohkubo,Masahiko Eba,Toshiki,Sakebe,Yasuyoshi Inagaki: "On Extracting Algebraic Specifications from Object-Oriented Programs with Polymorphic Types" Proceedings of The CafeOBJ Symposium. (1998)
• [文献書誌] 吉浦紀晃、米崎直樹: "証明力を拡張した適切さの理論ER" 人工知能学会誌. Vol.13(6). 981-989 (1998)
• [文献書誌] 森亮靖、友石正彦、米崎直樹: "時相論理によるリアクティブシステム仕様の実現可能に関する分類" コンピュータソフトウェア. Vol.15(3). 25-37 (1998)
• [文献書誌] Masami Hagiya,Akihiko Tozawa: "On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines" Lecture Notes in Computer Science,Springer-Verlag. Vol.1503. 17-32 (1998)
• [文献書誌] Mitsuharu Yamamoto,Koichi Takahashi,Masami Hagiya,Shin-ya Nishizaki: "Formalization of Graph Search Algorithms and its Applications" Lecture Notes in Computer Science,Springer-Verlag. Vol.1479. 479-496 (1998)