| 研究概要 |
本研究は,バグのない安全なソフトウェアを構築するための環境を実現するために,論理学の手法を用いてソフトウェアの安全性を形式的に議論・検証するための言語体系であるロジカル・フレームワークを提案し,それに基くソフトウェア構築環境を実装することを目的とする.とくに,議論対象の階層を取り扱うためのメタ変数の概念に関する理論研究を行ない,これをロジカル・フレームワークに反映させることにより,ソフトウェア自身だけではなく,そのソフトウェアに関するメタな議論を行なうための論理体系に関する議論も,同一のフレームワークで行なうことが可能になることが期待される.以上を達成するために,以下の計画に沿って研究を行なった.
(1)我々が既に提案していたロジカル・フレームワークである自然枠組(Natural Framework,NF)をもとに,計算と論理が自然に融合するように拡張を行なう.プログラムとその安全性を検証する論理とを同じ枠組で記述し議論できるようにするために,メタ変数の概念に関する理論的研究を行ない,得られた知見を自然枠組に反映させる.
(2)自然枠組の実装に適したプログラム言語を設計し実装する.このプログラム言語を利用して自然枠組を実装し,証明検査のインターフェイスや半自動化などの機能を設計し実装する.その上で,これらの枠組を利用したソフトウェア構築のための環境を設計し,実装する.
|
