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

Abstract

本稿では，プログラムの事前条件推定を行う新たな手法を提案する．本手法では，プログラムのテキストから生成した述語の集合とプログラムに相当する論理式，および事後条件の否定の連言を作り，そのMinimal Unsatisfiable Core（MUC）から事前条件を求める．MUC は一般的に複数存在するが，本手法ではまずMUC を列挙し，その中から事前条件として適格で，かつ最も弱い条件を選択する．こうして得られる事前条件は理想的な最弱条件ではないが，与えられた述語群の組み合わせの中で最も弱いという点で，我々はこれを「準最弱」な事前条件と呼ぶ． 我々は，C 言語向け有界検査ツールCForge を援用し，上記手法を実現するツールSMUCE を試作した．その上で，教科書的なアルゴリズムを実装するC 言語関数9 個に，2 種類の事後条件と共に適用し，人手で求めた事前条件との比較による評価を行った．結果，延べ18 個中10 個において，人手で求めた事前条件と同等か，より弱い条件が推定され，提案手法が原理上，実用的な事前条件を推定できることが確認できた． In this article, we propose a novel method to infer preconditions of a program. This method firstly generates a set of predicates from the program text, converts the program code into a logical formula, negates the postcondition given by the user, and conjuncts them all into a formula. Then, our method enumearates (possibly multiple) minimal unsatisfiable cores (or MUC) of the conjunctive formula. Our technique finally extracts proper preconditions from the MUCs. We call them as ” quasi-weakest” preconditions in that each of the precondition is the weakest among all the conjunctions of the predicates. We prototyped a tool named SMUCE that realizes the proposed method using CForge, a bounded verifier for C code. Thereafter, we applied the tool to nine C functions implementing textbook algorithms with two postconditions, and compared the generated preconditions with manually-specified ones. The result showed that SMUCE extracted equivalent, or even weaker preconditions than manually-specified ones from ten of the total of 18 programs, indicating the proposed method can infer applicative preconditions in principle.