| 研究概要 |
本研究は等式論理における検証法の確立し,さらに,一般のソフトウェアを代数的手法を用いて等式論理に自動的に変換することにより,これらの検証への応用を図るものである.本研究により、以下の結果が得られた。
(1)停止順序を満たす等式を通常の項書換え規則とみなし,これを満たさない等式は集合としての書換え規則とみなす項集合書換え系の形式的定義を与えた.
(2)項集合書換え系においては,通常の項書換え系におけるE合同上の書換えよりも若干緩い条件で停止性を持つ。
(3)停止的かつ左線形な項集合書換え系はその危険対が合流するならば合流性を持つ。
(4)項集合書換え系における完備化のための推論規則を与えた。
(5)項集合書換え系を試作し、効率的な実現について検討した。
(6)結合律と交換律による商の上の書換え系の停止性について検討した。
(7)優先順位付き項書換え系の定義を行ない,その等式論理に基づく意味論を与えた.これにより,関数型プログラムを等式論理に変換して検証するための基礎が得られた.
|
