| 研究概要 |
本年度の研究では以下の項目に上げる成果を上げることができた。
(1)書換え計算の視覚化:
書換えが計算の基本ステップである項書換え系の解析・検証・変換などの操作を直観的に支援するための手法として、項書換え系の(a)項、(b)計算、(c)操作、(d)情報の視覚化を提案した。(a)項の視覚化は項の構造の直観的理解を支援するため、部分木の省略や正規形の抽象化を含み、色や形で関数記号に関する種々の情報をわかりやすくした木表現で項を表す。(b)計算の視覚化は計算の動的な振舞いを理解するために、項の視覚化にもとづいて項書換え系の計算過程を表す。(c)操作の視覚化は視覚化された項や計算の操作を視覚的に直接実現し、(d)情報の視覚化は計算から得られる様々な数値情報をグラフなどを用いて視覚的情報にする。本研究では、これらの視覚化をグラフィカルユーザインタフェースを持つ視覚的項書換え支援環境TERSEとして実現した。
(2)並行計算の解析の視覚化:
この研究では、Hehnerによって提案されている通信プロセスの述語的意味論を、実時間制約をもつ通信プロセスの枠組に拡張し、述語的意味に基づく次のような検証法を提案した。プロセスPの述語的意味を表す論理式『P』は,それに対する入力を表す論理式とその出力を表す論理式とに分割することができる。この点に着目し,『P』をそれと論理的等価な標準形に変換し,その構造に従って,証明全体を小さく簡単な部分に分割して行う。本研究は、このような検証の課程を視覚的支援を目的としているが、本年度では、視覚的支援手法の検討には至らなかった。
(3)代数的仕様検証の視覚的支援:
代数的仕様が所望の性質を持っているかを調べるときに使われる構造帰納法やその拡張である被覆集合帰納法を自動化するための研究の一貫として、従来の被覆集合帰納法の拡張を行ない、真に能力の高い新しい被覆集合帰納法を提案した。この研究を進める段階で、(1)の項書換え系の操作の支援システムのテストバ-ジョンを使い、視覚的支援が有効であることを確認している。
|
