不変表明の生成支援機能をもつプログラム検証システム

淡 誠一郎  山口 高平  角所 収   慶一  

誌名
電子情報通信学会論文誌 D   Vol.J70-D   No.8   pp.1487-1497
発行日: 1987/08/25
Online ISSN: 
DOI: 
Print ISSN: 0913-5713
論文種別: 論文
専門分野: ソフトウェア技法
キーワード: 


本文: PDF(914.3KB)>>
論文を購入




あらまし: 
プログラムの自動検証システムはソフトウェア開発支援環境において重要な構成要素とみなされている.プログラム検証にはループの不変表明を含めた詳細な仕様が必要であり,これを完全に準備することは人間にとって非常に大きな負担であるため,その支援環境が望まれる.そこで,筆者らは不変表明の生成に関する理論的考察,更には不変表明の生成支援機能をもつプログラム検証システムの構成を行ってきた.理論的考察については既に報告済みであり,本稿では本システムのインプリメンテーションについて述べ,これまでの成果をまとめる.本システムは,プログラムの入力から仕様獲得(不変表明生成),検証条件生成,そして検証条件の証明までを含めた総合的なプログラム検証システムである.不変表明の生成支援機能としては,差分方程式法の実行,記号実行によるプログラム変数や経路条件のトレースおよびトレース情報からの帰納推論による不変表明の提案機能などを実現している.実行例を通してこれらの機能を説明し,計算機により不変表明の生成およびその支援が可能であることを示す.また,本システムは証明系も含めて実現されているため,従来のプログラム検証システムより現実的であり,発展性にも富む.