Hoare Logic
MenuHoare Logic はコマンドベースのプログラムの検証手法。
関数型プログラムは関数で記述するが、Hoare Logic は手続型の記述を使う。
プログラムの記述
プログラムの文(statement)は、変数や外部の状態を変更する。そして、次の文に続く。ここでは
record Env : Set (succ Zero) where
field
varn : ℕ
vari : ℕ
open Env
という形で環境を定義しよう。これは、持ち歩くので一種の DI Container になる。
関数型プログラムでは大域変数は変更できないので使えない。
文は、これらに対する変更を行う関数になる。
Env → Env
しかし、これでは次に続かない。次の文に変更した環境を渡すことにして、それも記述する。
Statement : Set
Statement = {t : Set} → Env → (Env → t ) → t
ここで t は、あまり意味はない。
満たして欲しい性質
もちろん、論理式で記述する。Env の論理関係式になるが、もちろん、関数の入力を使っても良い。
Cond : Set (Suc Zero)
Cond = Env → Set
Pre and Post Condition
Statement の前後で、条件が変わる。前に付くのは入力条件。出力条件は、次(継続あるいは Continuation)に記述する。
PreCond → Statement → PostCond
と書きたいが、
StatementWithCond : Cond → Cond → Set
StatementWithCond preCond postCond = {t : Set} → (e : Env ) → ( preCond e ) → ((e : Env ) → (postCond e ) → t ) → t
という感じになる。
簡単な例題
変数の初期設定は
Env → Env
なので、例えば、
λ e → record e { varn = 10 ; vari = 0 }
の様になる。
whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t
whileTest c10 next = next (record {varn = c10 ; vari = 0 } )
これには Pre/Post Condition がない。
コマンドの接続とループ
簡単なループを考えてみる。
{-# TERMINATING #-}
whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
whileLoop env next with lt 0 (varn env)
whileLoop env next | false = next env
whileLoop env next | true =
whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
このプログラムは実際に走らせることができる。
test1 : Env
test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
t に λ env1 → env1 を入れることにより実際に値を取り出すことができる。
proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
proof1 = refl
具体的な値を入れて、正しい結果になるかどうかを調べることもできる。これは普通のプログラム言語の assert に対応する。
不変条件
ループでは、入力の条件と出力の条件を一致させる。そのためには少し工夫がいる。ここでは n + i = c10 を使う。
whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env → t) → t
whileLoop' env proof next with ( suc zero ≤? (varn env) )
whileLoop' env proof next | no p = next env
whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next
where
env1 = record env {varn = (varn env) - 1 ; vari = (vari env) + 1}
proof3 : (suc zero ≤ (varn env)) → varn env1 + vari env1 ≡ c10
proof3 = ?
停止性
まず、ループを継続に分解する。
whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10)
→ (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) -- next with PostCondition
→ (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
すると、{-# TERMINATING #-} を落とせる。(実際の証明は割と長い)
これで、Invariant が保存されることがわかる。
この時に、Invariant から ℕ への関数があって、必ず、whileLoopSeg で減ってることがわかれば、loop は停止する。これは証明できる。
TerminatingLoopS : {l m n : Level} {t : Set l} (Index : Set m) → {Invraiant : Index → Set n } → ( reduce : Index → ℕ)
→ (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t)
→ (r : Index) → (p : Invraiant r) → t
TerminatingLoopS {_} {_} {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r)
... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) )
... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where
TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t
TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1))
TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j)
... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )
ここで、
loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t
これが、Invariant を保存して、reduce が必ず減るというループの Segment (断片)を表している。
これを使って、whileLoopSeg を呼び出せば、停止性を含む証明が完成する。
whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤
whileTestSpec1 _ _ x = tt
proofGearsTermS : {c10 : ℕ } → ⊤
proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 →
TerminatingLoopS Env (λ env → varn env)
(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 ))