手続きを含む命令型プログラムを検証するための証明戦術

アイテムタイプ

学位論文 / Thesis or Dissertation

言語

日本語

著者

小島裕登

著者（ヨミ）

コジマヒロト

抄録

近年，プログラムの大規模化・複雑化に伴い，プログラムの安全性は様々な分野でますます重要となっている．プログラムの安全性を検証する方法には，動的テストやモデル検査，定理証明がある．動的テストやモデル検査と比べて定理証明は数学的帰納法を用いて，全ての入力について検査できる強みがある．しかし，実際のプログラムの検証には定理証明はあまり用いられていない．なぜなら，定理証明を用いて大規模なプログラムの正しさを検証する場合，人の手による証明だけでは膨大な時間コストが必要なためである．そのため，定理証明の実用化には自動証明が必要不可欠である．しかし，大規模で複雑なプログラムの検証の完全な自動化はほぼ不可能であり，人の手による証明は避けられない．そこで，人の手による証明の負担をできる限り削減する部分的な自動証明が期待される．
定理証明を用いて命令型言語のプログラムを検証する研究がされている．論理体系としてHoare 論理などが用いられる．Hoare 論理を用いたプログラムの検証では，事前条件と事後条件，ループ不変条件から代入文のような部分的プログラムの検証条件を求めることで証明を行う．その検証条件を自動生成する場合，最弱事前条件を用いるのが一般的である．しかし，手続き呼び出し文を含む場合，最弱事前条件で手続き呼び出し文の検証条件を生成するのは容易ではない．
そこで本研究では，Hoare 論理を用いて手続きを含む命令型プログラムの検証するための証明戦術を提案する．さらに，定理証明支援器Coq を用いて自動証明を行う戦術を開発する．本手法は，非再帰手続きのプログラムの正当性を証明する場合は，最弱事前条件を用いて検証条件を自動的に生成する．また，再帰手続きのプログラムの正当性を証明する場合は，最弱事前条件と最強事後条件を組み合わせる事で検証条件を自動的に生成する．本手法の戦術を用いることで，元のプログラムの事前条件と事後条件，ループ不変条件から，検証条件を自動的に生成できる．自動生成する際に検証条件に関する表明の正当性を追加で検証する必要がある．しかし，表明の正当性についてはCoq で用意されている定理を用いることができるので容易に証明できる．本手法は，Hoare 論理によるプログラムの正当性の問題を，検証条件に関する表明の正当性の問題に帰着させる．また，検証条件に関する表明についても簡易的な正当性の検証を自動化するタクティクを開発した.

内容記述

三重大学大学院工学研究科博士前期課程情報工学専攻コンピュータソフトウェア研究室
31p

発行年

2021-03

フォーマット

application/pdf

著者版フラグ

publisher

出版者

三重大学

出版者（ヨミ）

ミエダイガク

修士論文指導教員

山田俊行

資源タイプ（三重大）

Master's Thesis / 修士論文

WEKO

Language

インデックスツリー