Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定

今井 健男, 酒井 政裕, 萩谷 昌己「Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定」, ソフトウェア工学の基礎XVIII 日本ソフトウェア科学会FOSE 2011, pp. 187-196, 近代科学社, 2011年11月.

Takeo Imai. Masahiro Sakai, Masami Hagiya, An Inference Method of Quasi-Weakest Preconditions by Minimal Unsatisfiable Core Enumeration. In proceedings of 18th Workshop on Foundation of Software Engineering (FOSE2011), pp. 187-196, Nov. 2011.

あらまし / Abstract

本稿では,プログラムの事前条件推定を行う新たな手法を提案する.本手法では,プログラムのテキストから生成した述語の集合とプログラムに相当する論理式,および事後条件の否定の連言を作り,その Minimal Unsatisfiable Core(MUC)から事前条件を求める.MUCは一般的に複数存在するが,本手法ではまずMUCを列挙し,その中から事前条件として適格で,かつ最も弱い条件を選択する.こうして得られる事前条件は理想的な最弱条件ではないが,与えられた述語群の組み合わせの中で最も弱いという点で,我々はこれを「準最弱」な事前条件と呼ぶ. 我々は,C言語向け有界検査ツールCForgeを援用し,上記手法を実現するツールPRUCEを試作した.その上で,教科書的なアルゴリズムを実装するC言語関数9個に適用し,人手で記述した事前条件との比較による評価を行った.

Links: