ログイン
言語:

WEKO3

  • トップ
  • ランキング
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

  1. 40 大学院工学研究科・工学部
  2. 40D 学位論文
  3. 修士論文
  4. 2020年度

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

http://hdl.handle.net/10076/00019869
http://hdl.handle.net/10076/00019869
4979f96a-46a1-4e09-b357-675a0133566f
名前 / ファイル ライセンス アクション
2020ME0179.pdf 2020ME0179 (142.3 kB)
Item type 学位論文 / Thesis or Dissertation(1)
公開日 2021-09-21
タイトル
タイトル 手続きを含む命令型プログラムを検証するための証明戦術
言語 ja
言語
言語 jpn
資源タイプ
資源タイプ識別子 http://purl.org/coar/resource_type/c_46ec
資源タイプ thesis
著者 小島, 裕登

× 小島, 裕登

ja 小島, 裕登

ja-Kana コジマ, ヒロト

Search repository
抄録
内容記述タイプ Abstract
内容記述 近年,プログラムの大規模化・複雑化に伴い,プログラムの安全性は様々な分野でますます重要となっている.プログラムの安全性を検証する方法には,動的テストやモデル検査,定理証明がある.動的テストやモデル検査と比べて定理証明は数学的帰納法を用いて,全ての入力について検査できる強みがある.しかし,実際のプログラムの検証には定理証明はあまり用いられていない.なぜなら,定理証明を用いて大規模なプログラムの正しさを検証する場合,人の手による証明だけでは膨大な時間コストが必要なためである.そのため,定理証明の実用化には自動証明が必要不可欠である.しかし,大規模で複雑なプログラムの検証の完全な自動化はほぼ不可能であり,人の手による証明は避けられない.そこで,人の手による証明の負担をできる限り削減する部分的な自動証明が期待される.
定理証明を用いて命令型言語のプログラムを検証する研究がされている.論理体系としてHoare 論理などが用いられる.Hoare 論理を用いたプログラムの検証では,事前条件と事後条件,ループ不変条件から代入文のような部分的プログラムの検証条件を求めることで証明を行う.その検証条件を自動生成する場合,最弱事前条件を用いるのが一般的である.しかし,手続き呼び出し文を含む場合,最弱事前条件で手続き呼び出し文の検証条件を生成するのは容易ではない.
そこで本研究では,Hoare 論理を用いて手続きを含む命令型プログラムの検証するための証明戦術を提案する.さらに,定理証明支援器Coq を用いて自動証明を行う戦術を開発する.本手法は,非再帰手続きのプログラムの正当性を証明する場合は,最弱事前条件を用いて検証条件を自動的に生成する.また,再帰手続きのプログラムの正当性を証明する場合は,最弱事前条件と最強事後条件を組み合わせる事で検証条件を自動的に生成する.本手法の戦術を用いることで,元のプログラムの事前条件と事後条件,ループ不変条件から,検証条件を自動的に生成できる.自動生成する際に検証条件に関する表明の正当性を追加で検証する必要がある.しかし,表明の正当性についてはCoq で用意されている定理を用いることができるので容易に証明できる.本手法は,Hoare 論理によるプログラムの正当性の問題を,検証条件に関する表明の正当性の問題に帰着させる.また,検証条件に関する表明についても簡易的な正当性の検証を自動化するタクティクを開発した.
内容記述
内容記述タイプ Other
内容記述 三重大学大学院 工学研究科 博士前期課程 情報工学専攻 コンピュータソフトウェア研究室
内容記述
内容記述タイプ Other
内容記述 31p
書誌情報
発行日 2021-03
フォーマット
内容記述タイプ Other
内容記述 application/pdf
著者版フラグ
出版タイプ VoR
出版タイプResource http://purl.org/coar/version/c_970fb48d4fbd8a85
出版者
出版者 三重大学
出版者(ヨミ)
値 ミエダイガク
修士論文指導教員
寄与者識別子Scheme WEKO
寄与者識別子 46660
姓名 山田, 俊行
言語 ja
資源タイプ(三重大)
値 Master's Thesis / 修士論文
戻る
0
views
See details
Views

Versions

Ver.1 2023-06-19 14:38:32.458905
Show All versions

Share

Mendeley Twitter Facebook Print Addthis

Cite as

エクスポート

OAI-PMH
  • OAI-PMH JPCOAR 2.0
  • OAI-PMH JPCOAR 1.0
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by WEKO3


Powered by WEKO3