| 研究課題/領域番号 |
08458067
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
濱口 毅 名古屋大学, 工学研究科, 助手 (90273284)
|
|---|
| 研究分担者 |
河口 信夫 名古屋大学, 工学研究科, 助手 (10273286)
結縁 祥治 名古屋大学, 工学研究科, 助手 (70230612)
阿草 清滋 名古屋大学, 工学研究科, 教授 (90026360)
稲垣 康善 名古屋大学, 工学研究科, 教授 (10023079)
坂部 俊樹 名古屋大学, 工学研究科, 教授 (60111829)
馮 速 名古屋大学, 工学部, 助手 (90262881)
|
|---|
| 研究期間 (年度) |
1996 – 1997
|
| 研究課題ステータス |
完了 (1997年度)
|
| 配分額 *注記 |
7,800千円 (直接経費: 7,800千円)
1997年度: 1,200千円 (直接経費: 1,200千円)
1996年度: 6,600千円 (直接経費: 6,600千円)
|
|---|
| キーワード | メタ計算 / 書換え計算 / 項書換え系 / 並行計算 / 検証 / 代数的仕様 / 帰納的定理 / 被覆集合帰納法 |
|---|
| 研究概要 |
プログラムが仕様の通りの働きをするかどうかを検証する技術は、ソフトウェアの信頼性向上のために重要である。しかしながら、プログラムの検証を完全に自動的に行うことは不可能であり、対話的にプログラム検証を行うシステムが望まれる。
このような検証システムを開発するに際して、仕様記述言語、プログラム言語、検証システム利用言語、システム記述言語を同一の言語にすることによって次のようなメリットが生じる。仕様の通りに働くプログラムを作成し、それを検証するプログラマ、検証システムの開発者ともに1種類の言語を習得するだけでよい。言語がそれぞれ異なればプログラマは3種類、検証システム開発者は4種類の言語を習得しなければならないのに比べて大きな利点である。
ソフトウェアの仕様記述、実現、検証ならびに検証システム開発のすべての過程を1種類の言語で行えるような言語(メタ言語と呼ぶことにする)には、それぞれの言語として望まれる性質が備わっているべきである。特に、検証システム開発言語としては、検証の基礎となる明確な論理や、プログラムや仕様を操作する機能(すなわち、メタ計算の機能)が備わっていること、また、検証過程の対話的コントロールの実現などが容易であることが必要である。
そこで、8年度、9年度の2年間にわたって、動的項書換え系の合流性、関数型計算戦略が正規化戦略となる書換えのクラス、重なりを持つ項書換え系の計算戦略、項書換え系の並列計算機における効率的実行、について検討し、いくつかの成果を得ることができた。
|
