|
最近の計算機システムの並列化・分散化の急速な進行に伴って、並列プログラムの生産性と信頼性を向上させるための研究が益々、重要となってきている。本研究では、記述性に優れた並列処理言語を設計し、また数学理論に裏付けられた、並列プログラムの検証技術を確立することを目的として、平成2年度からその基礎研究を進めてきた。本年金は、まず、前年度に与えた表示的意味記述を改善する研究を行った。すなわち、その表示的意味記述の操作的な面を除去するために、goto文などの意味記述に用いられてきた接続法の概念に着目し、この概念を用いて、より抽象度が高く、了解性の高い表示的意味記述に書き改めた。このことにより、逐次型のプログラミング言語の表示的意味記述の自然な拡張として、並列処理言語の意味記述を与えることに成功した。次に、この表示的意味記述の枠組の中で、並列プログラムの諸性質を導き、これらの性質を公理とする、プログラムの正当性検証システムについて考察を行った。この検証システムに関する研究は次年度も引き続き行う予定である。また、公理的意味記述及び述語的意味記述についても基礎研究を行った。さらに、本年度に与えた表示的意味記述が適切であることを検証するために、操作的意味記述を定義し、この両者の意味記述の対応関係を明らかにし、その十分な抽象性(full abstractness)について考察を行った。この研究課題は次年度の研究テ-マであったが、本年度からの研究開始が適当であると判断して行ったものである。なお、この操作的意味に基づくインタプリタの作製及び正当性に関する議論は当初の計画通り平成4年度に行う予定である。
|
