文献

J-GLOBAL ID：201402229303530834   整理番号：13A1961820

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

An Inference Method of Quasi-Weakest Preconditions by Minimal Unsatisfiable Core Enumeration

著者 (4件)： 今井健男 (株式会社東芝研究開発センター) ,  今井健男 (東京大学情報理工学系研究科) ,  酒井政裕 (株式会社東芝研究開発センター) ,  萩谷昌己 (東京大学情報理工学系研究科)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 30  号： 2  ページ： 2.207-2.226 (J-STAGE)  発行年： 2013年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

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

シソーラス用語： C言語 ,  *計算機コード ,  データ ,  式 ,  信頼性 ,  *前処理 ,  条件 ,  *推定 ,  ソフトウェア
準シソーラス用語： テキストデータ ,  *プログラムコード ,  *事前処理 ,  論理式

分類 (2件)： 計算機利用技術一般  (JE01000C) ,  その他の計算機利用技術  (JE14000C)

タイトルに関連する用語 (1件)： 推定