| 研究課題/領域番号 |
08680367
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
林 晋 神戸大学, 工学部, 教授 (40156443)
|
|---|
| 研究期間 (年度) |
1996 – 1997
|
| 研究課題ステータス |
完了 (1997年度)
|
| 配分額 *注記 |
1,800千円 (直接経費: 1,800千円)
1997年度: 400千円 (直接経費: 400千円)
1996年度: 1,400千円 (直接経費: 1,400千円)
|
|---|
| キーワード | プログラム検証 / プログラム合成 / 形式的方法 / 形式的技法 / 構成的プログラミング / 最適化 / 形式的仕様記述 |
|---|
| 研究概要 |
本研究の当初計画では、型のない関数型言語にもとづくPX systemそのものにBerardiの方法を適用する予定であったが、これはうまく行かなかった。それは、もともと、型理論に基づく方法を型の無い理論に強引に適用しようという計画であったので、本来無理があったのかもしれない。
そのため、第1年度より計画を変更し、PX systemの抜本的な再設計・再構築という道を選んだ。すなわち、Berardiの方法がそのまま適用できるように、PX自体をその基礎論理システムから再構築したのである。
この計画変更により、プログラム抽出部分と最適化部分を完全に独立したモジュールとしてもつシステムを構築することが可能となり、PX systemのad hocな最適化の置換えと拡張という最終目標は、当初計画以上の成果を得ることができた。
また、本研究の研究途上、林は構成的プログラミングの全く新しい応用である"証明アニメーション"という構想を提唱した。このアイデアは、構成的プログラミンという大きなコンテキストのなかで得られたものであり、本研究の具体的研究計画の枠組みを越えるものである。
しかし、このアイデアは本研究の具体的成果の一つとして得られたものであり、また、長期的展望にたてば、本来の研究計画の達成より、この新知見の方が遥かに大きな影響力を持つと予想される。
|
