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

DOI

書誌事項

タイトル別名
  • An Inference Method of Quasi-Weakest Preconditions by Minimal Unsatisfiable Core Enumeration

この論文をさがす

説明

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

収録刊行物

詳細情報 詳細情報について

  • CRID
    1390282679714440448
  • NII論文ID
    130004892253
  • DOI
    10.11309/jssst.30.2_207
  • ISSN
    02896540
  • 本文言語コード
    ja
  • データソース種別
    • JaLC
    • CiNii Articles
  • 抄録ライセンスフラグ
    使用不可

問題の指摘

ページトップへ