能動関数によるアサーション検証設計(<特集>続・システム検証の科学技術,サイバー増大号)

概要

論文の詳細を見る
規模の大きな,制御フローの複雑なプログラムを充分にテストすることは容易ではない.プログラム実行時の動作の正しさを調べるには,実行時点での性質や条件を示す表明(アサーション)を挿入する方法が知られている.本論文では,Hoareの記法P{Q}Rに基づいて,事前条件(P)に対して,事前チェック(Pre-check NP),および,事後条件(R)に対して,事後チェック(post-check 〜R)するプログラムの設計法を提案する.また,そのようなチェック機能を,能動関数(active function)を用いた形で設計・実現する方法について述べる.能動関数は,自ら起動する条件を持った関数で,指示された時,点で条件の値が真(true)になると,関数の本体を実行する.このような設計法によって,実行の正しさを保証するだけでなく,ソフトウェアの仕様の変更に柔軟に対応して,安定した状態を保つプログラムの構成を目指している.なお,能動関数を用いたプログラムを効率良く実行するには,それに適合したハードウエアの支援が不可欠である.
2005-07-26