| 研究概要 |
プログラムの仕様記述,仕様の証明,検証,合成を統一的に扱える環境の実現を目指して研究を行った。このために、直観主義論理に基づく構成的論理体系をQJと、その部分体系としての関数的論理型プログラミング言語Qutyの設計を行った。Qutyは以下のような特徴を持つ言語である。
1.論理記号¬,Λ,V,ヨを言語の基本要素として持つ。これらの論理記号の意味は、直観主義論理における対応する論理記号の意味と一致する。したがって、論理的に自然なプログラムを容易に書くことができる。2.関数型を含む豊富なデータ型を持つ。これにより高い型のデータを扱う関数的プログラムを自然に書くことができる。3.プログラムの実行は並列に行われる。共有変数およびストリームを用いた並列プログラミングが可能。
QJは型を持つ構成的論理体系であり、QJの項がQutyのプログラムと一致するように設計した。したがって、プログラムの仕様記述,仕様の証明,プログラムの検証等をすべてQJの中で行うことができる。またQutyの操作的意味の整合性を論理体系QJの中で形式的に示すことができた。このことはまた、Qutyでの計算がQJでの証明に対応し、プログラムの中で使われる論理記号の意味かそれらが本来持っている論理的意味と一致することを示している。計算機上のシステム作成に関しては、簡単な実験を行うに留まったが、理論的には十分な成果を上げることが出来た。
|
