| 研究概要 |
種々の実用プログラムが順序機械型プログラムとして記述できる.本研究では主に,代数的手法を用いた順序機械型プログラムの階層的設計の正しさの証明(設計検証)の計算機支援環境を考案する.代数的言語の使用により,検証は項書換え等の単純な手法の組合せで行えるが,従来は,種々の手法を人間が複雑に組合せて適用しており,自動化が困難であった.
1.本研究では,仕様記述スタイルに制限を設けて,検証を自動化できる検証手順を考案した,記述スタイルの制限により,証明対象式を(恒真性判定可能な)加減算を含む整数上の理論式に帰着でき,一定の検証手段の組合せ方で検証を行える.この記述スタイルでは,整数配列等を用いても論理式の恒真性判定が可能となり,実用上有効である.
2.構造的帰納法を用いる場合,証明に必要な補題の選定や代入を検証者が検証過程を管理しながら行うのは非常に繁雑である.そこで以下のように計算機支援の方法を定めた.構造的帰納法では,必要な言明を着目する状態に与えるが,この際,図表示された状態遷移図上で言明を与えられるようにGUIを設計した.証明に必要な補題の選定や代入に関しては,計算機が候補を自動的に選出し,検証者が最終的に指定する.そのもとで支援系は必要な証明対象式を自動生成し,証明に行う.また,証明過程を管理し,言明の変更に対して再度証明すべき個所を表示する.
3.少ない労力で検証可能であることを実証するため,GUIを用いて上記2.に基づく機能を与える検証支援系を作成した.
4.本支援系を用いて,マックスソートプログラムの設計検証を,試行錯誤を含め2日程度で行った.その証明では式長が1000トークン程度の論理式の恒真性判定が必要であるが、恒真性を高速に判定する方法を考案したことにより,数秒程度で判定できた.
5.これらの結果,本検証手順及び支援系が有効であることが分かった.記述クラスの拡張およびそれらの検証法を考案すること等が今後の課題である.
|
