代数的言語で記述した抽象的順序機械型プログラムの設計検証の自動化

概要

論文の詳細を見る
本論文では,順序機械型プログラムの設計の正しさの形式的な証明を,半自動で行うための証明手順を提案する.証明を実際上可能とするために,要求仕様から始めて逐次,抽象的な一動作(遷移)をより具体的な動作の系列で展開(詳細化)していく階層的設計法を採用する.詳細化の度に,展開に用いた系列が元の遷移の動作を正しく実現していることを証明する.提案する証明手順は,制限された記述スタイルのもとで書かれた仕様に対し,構造的帰納法の各段階ごとに,その段階を証明するための式を不変表明などから作り,その式の成立を加減算と比較演算から成る整数上の論理式(プレスプルガー文)の恒真性判定手続きを用いて示す,というものである.従来は,項書き換えや場合分けなどの手法を検証者が複雑に組み合わせて証明していたため,証明に時間がかかり自動化も困難であった.しかし,提案する証明手順は単純なため自動化が容易であり,また,本論文で対象とするプレスプルガー文の恒真性は短時間で判定できるため高速である.提案する証明手順に基づく検証支援系を実際に作成した.その支援系は,検証者が基本述語・関数に関する補題のインスタンスや不変表明を与えれば,プレスブルガーの合成やその真偽判定を自動で行う.本支援系を用いて,マックスソートプログラムの証明をCPU時間十数分程度で行えた.そこの証明では,式中の変数・演算子等の総出現数が1300以上の,大きな幾つかのプレスブルガー文の真偽を判定しなければならなかったが,いずれも数秒程度で判定できた.
一般社団法人情報処理学会の論文
1995-10-15

代数的言語で記述した抽象的順序機械型プログラムの設計検証の自動化

スポンサーリンク

概要

著者

関連論文

スポンサーリンク