拡張Farkas補題の部分適用による非線形ループ不変式生成を用いたプログラム検証

摘要

ループ不変式を生成するための手法として，与えたテンプレートと事前条件と事後条件から得られる検証式をFarkas補題に基づき変換する手法が研究されている．Farkas補題に基づく変換では線形な多項式の不等式のみを原始論理式として含む論理式を等価変換する．それを変数や関数適用項の積を単項式とする多項式上に拡張した拡張Farkas補題が提案され，非線形なループ不変式を生成できる場合があることが示された．しかし，拡張Farkas補題を用いて生成したループ不変式がプログラム検証に有効かどうかについては議論されていない．本稿では，プロラム検証における拡張Farkas補題に基づくループ不変式の生成法の有効性を評価し，拡張Farkas補題を有効に利用する検証手法を提案する．具体的には，未知係数を含む複数の検証式の一部を拡張Farkas補題により変換し，それを充足する未知係数の割り当てを残りの検証式の未知係数に代入した後に恒真性を判定する．