1995 Fiscal Year Annual Research Report
書換え計算の可視化に基づくプログラミング環境の実現
| Project/Area Number |
07558037
|
|---|
| Research Category |
Grant-in-Aid for Developmental Scientific Research (B)
|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
坂部 俊樹 名古屋大学, 工学部, 教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
河口 信夫 名古屋大学, 工学部, 助手 (10273286)
馮 速 名古屋大学, 工学部, 助手 (90262881)
結縁 祥治 名古屋大学, 工学部, 助手 (70230612)
稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
|
|---|
| Keywords | 視覚化 / 書換え計算 / 項書換え系 / 実時間並行計算 / 検証 / 代数的仕様 / 帰納的定理 / 被覆集合帰納法 |
|---|
| Research Abstract |
本年度の研究では以下の項目に上げる成果を上げることができた。
(1)書換え計算の視覚化:
書換えが計算の基本ステップである項書換え系の解析・検証・変換などの操作を直観的に支援するための手法として、項書換え系の(a)項、(b)計算、(c)操作、(d)情報の視覚化を提案した。(a)項の視覚化は項の構造の直観的理解を支援するため、部分木の省略や正規形の抽象化を含み、色や形で関数記号に関する種々の情報をわかりやすくした木表現で項を表す。(b)計算の視覚化は計算の動的な振舞いを理解するために、項の視覚化にもとづいて項書換え系の計算過程を表す。(c)操作の視覚化は視覚化された項や計算の操作を視覚的に直接実現し、(d)情報の視覚化は計算から得られる様々な数値情報をグラフなどを用いて視覚的情報にする。本研究では、これらの視覚化をグラフィカルユーザインタフェースを持つ視覚的項書換え支援環境TERSEとして実現した。
(2)並行計算の解析の視覚化:
この研究では、Hehnerによって提案されている通信プロセスの述語的意味論を、実時間制約をもつ通信プロセスの枠組に拡張し、述語的意味に基づく次のような検証法を提案した。プロセスPの述語的意味を表す論理式『P』は,それに対する入力を表す論理式とその出力を表す論理式とに分割することができる。この点に着目し,『P』をそれと論理的等価な標準形に変換し,その構造に従って,証明全体を小さく簡単な部分に分割して行う。本研究は、このような検証の課程を視覚的支援を目的としているが、本年度では、視覚的支援手法の検討には至らなかった。
(3)代数的仕様検証の視覚的支援:
代数的仕様が所望の性質を持っているかを調べるときに使われる構造帰納法やその拡張である被覆集合帰納法を自動化するための研究の一貫として、従来の被覆集合帰納法の拡張を行ない、真に能力の高い新しい被覆集合帰納法を提案した。この研究を進める段階で、(1)の項書換え系の操作の支援システムのテストバ-ジョンを使い、視覚的支援が有効であることを確認している。
|
-
[Publications] Nobuo Kawaguchi: "TERSE:A Visual Environment for Supporting Analysis,Verification and Transformation of Term Rewriting Systems" To appear in AMAST'96. (1996)
-
[Publications] 篠原加奈子: "Predicative Verification of Real-time Communicating Processes" コンピュテーション研究会(平成8年3月発表予定). (1996)
-
[Publications] 河口信夫: "項書換え系の解析・検証・変換のための視覚的支援手法" コンピュータソフトウェア. 13. 23-36 (1996)
-
[Publications] 河口信夫: "関数型プログラミング言語StandardMLを用いた項書換え計算の視覚化の実現" 電気学会論文誌. 116-C. 103-110 (1996)
-
[Publications] 結縁祥治: "Predicative Specification of Real-time Communicating Processes" ソフトウェア科学会全国大会. 12. 181-184 (1995)
-
[Publications] 大塚正人: "被覆集合を用いた帰納的定理証明法の改良" 日本ソフトウェア科学会第12回大会論文集. 65-68 (1995)
