形式的体系の 定理証.pptVIP

形式的体系の定理証明支援系上での実現法 2006年10月31日 木下佳樹 高橋孝一 田辺良則 湯浅能史 産業技術総合研究所 システム検証研究センター 自動検証と対話型検証 自動検証 検証すべき問題を，有限個の空間の探索問題に落とす． 代表例: モデル検査 適用できる範囲に限りはあるが，「ボタン一つで」答が出る． 対話型検証 検証すべき問題を数学的に定式化． 定理証明器による支援 高い専門的知識が要求されるが，適用できる範囲は広い． 2つの混合 定理証明支援系によるプログラム検証 「プログラムの正しさ」を (数学の) 定理として表現し，定理を数学的に証明する． このチュートリアルでは，「ホア論理」 (Hoare logic) と呼ばれる体系を用いる． 証明は，計算機上で実行する． 人間の誤りが混入し得ない． 証明を支援するシステム 証明の入力を支援する． 入力した証明の正しさを確認する． このチュートリアルでは，Agdaというシステムを使用する． 本チュートリアルでは 以下を，例によって紹介する． ホア論理． ホア論理とは何か． どのようなことが示せるか． 定理証明支援系Agda． Agda上での証明，とはどのようなものか． 検証対象をAgda上で表現する手順はどのようになるか． はじめにホア論理定理証明支援系Agdaホア論理のAgdaでの符号化ホア論理の健全性まとめ はじめにホア論理定理証明支援系Agdaホア論理のAgdaでの符号化ホア論理の健全性まとめ 対象プログラム例 正の整数a,bを入力として，aをbで割った商qと余りrを出力するプログラム ホア論理による証明例 対象: whileプログラム b∈B: 「条件式」 p∈P: 「基本命令」 c∈C: whileプログラム c ::= p | skip | abort | c ; c | if b then c else c fi | while b do c od 条件式と基本命令 条件式の例: a = 5 a != b a = b+7 a + b c 基本命令の例 a := b a := b - 3 b := (a + b) - 5 ホア三つ組 ホア三つ組 { b1 } c { b2 } b1, b2∈B : 条件式 c ∈ C : whileプログラム 直観的な意味: b1 が成立しているときに c を実行して，cが停止すれば b2 が成立する． 例1: { x = 5 } x := x + 1 { x 0 } 例2: { x = 2 } if x = 1 then y := 3 else z := 3 fi { x z } 例3:{ a 0 ∧ b 0 } q:=0; r:=a;　while r=b do　r:=r-b;　q:=q+1　od { a = bq+r ∧ 0 = r b } ホア論理: 公理 {b} skip {b} (b∈B) {b} abort {false} (b∈B) 基本命令については，  {b} p {b} (b,b∈B, p∈P)の形の公理 の集合が与えられているものとする． 基本命令に関する公理の例 基本命令が算術式の代入の場合  (変数v) := (算術式e) 条件式 b に対し，次を公理とする． { b [v ← e] } v := e { b } 例: { y+1 + y = 5 } x := y+1 { x + y = 5 } ホア論理: 推論規則 推論規則の妥当性 仮定 b1かつb が成り立つとき， c1 を実行して停止すれば b2 が成り立つ． b1かつ bでない とき，c2 を実行して停止すれば b2 が成り立つ． 結論 b1 が成り立つとき， if b then c1 else c2 fiを実行して停止すれば b2 が成り立つ． 推論規則の妥当性 仮定 b1かつb が成り立つとき， c を実行して停止すれば b1 が成り立つ．(b1 は 不変式 と呼ばれる) 結論 b1 が成り立つとき， while b do c odを実行し