\chapter{Hoare Logic}
\label{c:hoare}
Floyd-Hoare Logic \cite{10.1145/363235.363259}(以下 Hoare Logic) とは
C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
Hoare Logic では事前条件が成り立つとき、何らかの計算(以下コマンド)を実行した後に
事後条件が成り立つことを検証する。
事前条件を P 、 何らかの計算を C 、 事後条件を Q としたとき、
$\{P\}\ C \ \{Q\}$ といった形で表される。
Hoare Logic ではプログラムの部分的な正当性を検証することができ、
事後条件のあとに別の コマンド をつなげてプログラムを構築することで、
シンプルな計算に対する検証することができる。

本章は Agda で実装された Hoare Logic について解説し、
実際に Hoare Logic を用いた検証を行う。


\section{Hoare Logic}
現在 Agda 上での Hoare Logic は初期の Agda で実装されたもの \cite{agda-alpa}とそれを現在の Agda に対応させたもの \cite{agda2-hoare}が存在している。

ここでは現在 Agda に対応した Hoare Logic を使用する。

例として \coderef{c-while} のようなプログラムを記述した。
これは変数 \verb/n/ と \verb/i/ を持ち、\verb/n/が 0　より大きいとき、\verb/i/を増やし \verb/n/を減らす、
疑似プログラムである。
このプログラムを Hoare Logic 上で同様のプログラムを作成し、検証を行う。
\begin{lstlisting}[caption=while Loop Program,label=c-while]
n = 10;
i = 0;

while (n > 0) {
  i++;
  n--;
}
\end{lstlisting}


\coderef{agda-hoare} は Agda 上での Hoare Logic の構築子である。
\verb/Env/ は \coderef{c-while}の \verb/n/、 \verb/i/ といった変数をレコード型でまとめたもので、\verb/n/と\verb/i/それぞれが型として Agda 上での自然数の型である $\mathbb{N}$ を持つ。

\verb/PrimComm/ は Primitive Command で、 \verb/n/、\verb/i/ といった変数に 代入するときに使用される関数である。

\verb/Cond/ は Hoare Logic の 条件で、 \verb/Env/ を受け取って　\verb/Bool/ 値、\verb/true/ か \verb/false/ を返す関数となっている。


Agda のデータで定義されている \verb/Comm/ は Hoare Logic での コマンド を表す。

\verb/Skip/ は何も変更しない コマンド で、 \verb/Abort/ はプログラムを中断する コマンド である。

\verb/PComm/ は PrimComm を受けて コマンド を返す型で定義されており、 変数を代入するときに使われる。

\verb/Seq/ は Sequence で コマンド を2つ受けて コマンド を返す型で定義されている。
これは、ある コマンド から コマンド に移り、その結果を次の コマンド に渡す型になっている。

\verb/If/ は \verb/Cond/ と \verb/Comm/ を2つ受け取り、 \verb/Cond/ が \verb/true/ か \verb/false/ かで 実行する \verb/Comm/ を変える コマンド である。

\verb/While/ は \verb/Cond/ と \verb/Comm/ を受け取り、 \verb/Cond/ の中身が \verb/True/ である間、 \verb/Comm/ を繰り返す コマンド である。

\begin{lstlisting}[caption=Agda での Hoare Logic の構成,label=agda-hoare]
PrimComm : Set
PrimComm = Env → Env

Cond : Set
Cond = (Env → Bool) 

data Comm : Set where
  Skip  : Comm
  Abort : Comm
  PComm : PrimComm -> Comm
  Seq   : Comm -> Comm -> Comm
  If    : Cond -> Comm -> Comm -> Comm
  While : Cond -> Comm -> Comm
\end{lstlisting}

Agda 上の Hoare Logic で使われるプログラムは \verb/Comm/ 型の関数となる。
プログラムの処理を \verb/Seq/ でつないでいき、最終的な状態にたどり着くと値を返して止まる。
%%  Code \ref{agda-hoare-simpl} は 変数 $i$、 $n$ に代入を行うプログラムである。
%% これは Seq で PComm を2つ繋げた形になる。

 \coderef{agda-hoare-prog}は \coderef{c-while}で書いた While Loop を Hoare Logic でのコマンドで記述したものである。
ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。

\lstinputlisting[caption= Hoare Logic のプログラム ,label=agda-hoare-prog]{src/agda-hoare-prog.agda.replaced}
%% \begin{lstlisting}[caption= Hoare Logic のプログラム ,label=agda-hoare-prog] %% ,mathescape=false
%% program : Comm
%% program = 
%%     Seq ( PComm (λ env → record env {varn = 10}))
%%     $ Seq ( PComm (λ env → record env {vari = 0}))
%%     $ While (λ env → lt zero (varn env ) )
%%       (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
%%         $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
%% \end{lstlisting}

この Comm を Agda 上で実行するため、 \coderef{agda-hoare-interpret} の \verb/interpret/ 関数を作成した。


\lstinputlisting[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret]{src/agda-hoare-interpret.agda.replaced}
%% \begin{lstlisting}[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret]
%% {-# TERMINATING #-}
%% interpret : Env → Comm → Env
%% interpret env Skip = env
%% interpret env Abort = env
%% interpret env (PComm x) = x env
%% interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
%% interpret env (If x then else) with x env
%% ... | true = interpret env then
%% ... | false = interpret env else
%% interpret env (While x comm) with x env
%% ... | true = interpret (interpret env comm) (While x comm)
%% ... | false = env
%% \end{lstlisting}

\coderef{agda-hoare-interpret}は 初期状態の \verb/Env/ と 実行する コマンド の並びを受けとって、実行後の \verb/Env/ を返すものとなっている。
\verb/interpret/ 関数は停止性を考慮していないため、 \verb/{-# TERMINATING #-}/ タグを付けている。

\coderef{agda-hoare-run}のように \verb/interpret/ に \verb/vari = 0 , varn = 0/ の \verb/record/ を渡し、 実行する \verb/Comm/ を渡して 評価すると \verb/record { varn = 0 ; vari = 10 }/ のような \verb/Env/ が返ってくる。
\verb/interpret/ で実行される コマンド は  \coderef{agda-hoare-prog} で記述した While Loop するコマンドである

\begin{lstlisting}[caption=Agda での Hoare Logic の実行 ,label=agda-hoare-run]
test : Env
test =  interpret ( record { vari = 0  ; varn = 0 } ) program
-- record { varn = 0 ; vari = 10 }
\end{lstlisting}


\section{While Program の部分正当性}
ここでは先程記述した \coderef{agda-hoare-prog} の部分正当性の検証を行う。

\coderef{hoare-rule} の \verb/HTProof/ は Agda 上での Hoare Logic でのコマンドに対応した性質を型としてまとめたものである。
\verb/HTProof/ では Pre-Condition とコマンド、Post-Condition を受け取って定義される Agda のデータである。
\coderef{agda-hoare} のコマンドで定義された \verb/Skip/、 \verb/Abort/、 \verb/PComm/、
\verb/Seq/、\verb/If/、\verb/While/、に対応した証明のための命題が存在している。

\verb/PrimRule/ は Pre-Condition と PrimComm、 Post-Condition、
\coderef{axiom-taut} の \verb/Axiom/ を引数として \verb/PComm/の入った \verb/HTProof/ を返す。

\verb/SkipRule/ は Condition を受け取ってそのままの Condition を返す HTProof を返す。

\verb/AbortRule/ は Pre-Contition を受け取って、\verb/Abort/ を実行する HTProof を返す。

\verb/WeakeningRule/ は通常の Condition から制約を緩める際にに使用される。
\ref{axiom-taut} の \verb/Tautology/ を使って Condition が同じであることを

\verb/SeqRule/ は3つの Condition と 2つの コマンド を受け取り、これらのプログラムの逐次的な実行を保証する。

\verb/IfRule/ は分岐に用いられ、3つの Condition と 2つの コマンド を受け取り、判定の Condition が成り立っているかいないかで実行する コマンド を変えるルールである。
この時、どちらかの コマンド が実行されることを保証している。

\verb/WhileRule/ はループに用いられ、1つの コマンド と２つの Condition を受け取り、事前条件が成り立っている間、 コマンド を繰り返すことを保証している。

\lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced}



%% \begin{lstlisting}[caption=Agda での Hoare Logic の構成,label=agda-hoare-rule]
%% data HTProof : Cond -> Comm -> Cond -> Set where
%%   PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
%%              (pr : Axiom bPre pcm bPost) ->
%%              HTProof bPre (PComm pcm) bPost
%%   SkipRule : (b : Cond) -> HTProof b Skip b
%%   AbortRule : (bPre : Cond) -> (bPost : Cond) ->
%%               HTProof bPre Abort bPost
%%   WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
%%                 {bPost' : Cond} -> {bPost : Cond} ->
%%                 Tautology bPre bPre' ->
%%                 HTProof bPre' cm bPost' ->
%%                 Tautology bPost' bPost ->
%%                 HTProof bPre cm bPost
%%   SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
%%             {cm2 : Comm} -> {bPost : Cond} ->
%%             HTProof bPre cm1 bMid ->
%%             HTProof bMid cm2 bPost ->
%%             HTProof bPre (Seq cm1 cm2) bPost
%%   IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
%%            {bPre : Cond} -> {bPost : Cond} ->
%%            {b : Cond} ->
%%            HTProof (bPre /\ b) cmThen bPost ->
%%            HTProof (bPre /\ neg b) cmElse bPost ->
%%            HTProof bPre (If b cmThen cmElse) bPost
%%   WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
%%               HTProof (bInv /\ b) cm bInv ->
%%               HTProof bInv (While b cm) (bInv /\ neg b)
%% \end{lstlisting}

\coderef{hoare-rule}を使って \coderef{c-while}の WhileProgram の仕様を構成する。

\lstinputlisting[caption=Agda での Hoare Locig の構成,label=hoare-rule]{src/agda-hoare-rule.agda.replaced}

全体の仕様は  Code \ref{agda-hoare-while}の \verb/proof1/ の様になる。
\verb/proof1/ では型で initCond、  Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、
\verb/initCond/ から \verb/program/ を実行し \verb/termCond/ に行き着く Hoare Logic の証明になる。

それぞれの Condition は Rule の後に記述されている \verb/{}/ に囲まれた部分で、
\verb/initCond/のみ無条件で \verb/true/ を返す Condition になっている。

それぞれの Rule の中にそこで証明する必要のある補題が \verb/lemma/ で埋められている。
\verb/lemma1/ から \verb/lemma5/ の証明は概要のみを示し、全体は付録に載せる。

これらの lemma は HTProof の Rule に沿って必要なものを記述されており、
\verb/lemma1/ では PreCondition と PostCondition が存在するときの代入の保証、
\verb/lemma2/ では While Loop に入る前の Condition からループ不変条件への変換の証明、
\verb/lemma3/ では While Loop 内での PComm の代入の証明、
\verb/lemma4/ では While Loop を抜けたときの Condition の整合性、
\verb/lemma5/ では While Loop を抜けた後のループ不変条件からCondition への変換と termCond への移行の整合性を保証している。

\lstinputlisting[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]{src/agda-hoare-while.agda.replaced}
%% \begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]  
%% proof1 : HTProof initCond program termCond
%% proof1 =
%%       SeqRule {λ e → true} ( PrimRule empty-case )
%%     $ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
%%     $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
%%             WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
%%             $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
%%                      $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
%% \end{lstlisting}

proof1 は\coderef{agda-hoare-prog}の program と似た形をとっている。
Hoare　Logic では Comannd に対応する証明規則があるため、仕様はプログラムに対応している。


\section{Hoare Logic での健全性}
\coderef{agda-hoare-while} では Agda での Hoare Logic を用いた仕様の構成を行った。
この仕様で実際に正しく動作するかどうか(健全性)を検証する必要がある。

\coderef{agda-hoare-satisfies} は Hoare Logic 上での部分正当性を確かめるための関数である。
 \verb/SemComm/ では Comm を受け取って成り立つ関係を返す。
 \verb/Satisfies/ では Pre Condition と コマンド、 Post Condition を受け取って、
 Pre Condition から Post Condition を正しく導けるという仕様を返す。

\lstinputlisting[caption= State Sequence の部分正当性,label=agda-hoare-satisfies]{src/agda-hoare-satisfies.agda.replaced}

%% \begin{lstlisting}[caption= State Sequence の部分正当性,label=agda-hoare-satisfies]
%% SemComm : Comm -> Rel State (Level.zero)
%% SemComm Skip = RelOpState.deltaGlob
%% SemComm Abort = RelOpState.emptyRel
%% SemComm (PComm pc) = PrimSemComm pc
%% SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
%% SemComm (If b c1 c2)
%%   = RelOpState.union
%%       (RelOpState.comp (RelOpState.delta (SemCond b))
%%                        (SemComm c1))
%%       (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
%%                        (SemComm c2))
%% SemComm (While b c)
%%   = RelOpState.unionInf
%%       (λ (n : $mathbb{N}$) ->
%%         RelOpState.comp (RelOpState.repeat
%%                            n
%%                            (RelOpState.comp
%%                              (RelOpState.delta (SemCond b))
%%                              (SemComm c)))
%%                          (RelOpState.delta (NotP (SemCond b))))

%% Satisfies : Cond -> Comm -> Cond -> Set
%% Satisfies bPre cm bPost
%%   = (s1 : State) -> (s2 : State) ->
%%       SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2
%% \end{lstlisting}

これらの仕様を検証することでそれぞれの コマンド に対する部分正当性を示す。

\coderef{agda-hoare-soundness} の \verb/Soundness/ では \verb/HTProof/ を受け取り、 \verb/Satisfies/ に合った証明を返す。
\verb/Soundness/ では \verb/HTProof/ に記述されている Rule でパターンマッチを行い、対応する証明を適応している。
\verb/Soundness/ のコードは量が多いため部分的に省略し、全文は付録に載せることにする。

\lstinputlisting[caption=Agda での Hoare Logic の健全性,label=agda-hoare-soundness]{src/agda-hoare-soundness.agda.replaced}

%% \begin{lstlisting}[caption=Agda での Hoare Logic の健全性,label=agda-hoare-soundness]
%% Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
%%             HTProof bPre cm bPost -> Satisfies bPre cm bPost
%% Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
%%   = axiomValid bPre cm bPost pr s1 s2 q1 q2
%% Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2
%%   = substId1 State {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1
%% Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
%% Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost)
%%           s1 s2 q1 q2
%%   = let hyp : Satisfies bPre' cm bPost'
%%         hyp = Soundness pr
%%         r1 : SemCond bPre' s1
%%         r1 = tautValid bPre bPre' tautPre s1 q1
%%         r2 : SemCond bPost' s2
%%         r2 = hyp s1 s2 r1 q2
%%     in tautValid bPost' bPost tautPost s2 r2
%% Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
%%            s1 s2 q1 q2
%%   = let hyp1 : Satisfies bPre cm1 bMid
%%         hyp1 = Soundness pr1
%%         hyp2 : Satisfies bMid cm2 bPost
%%         hyp2 = Soundness pr2
%%         sMid : State
%%         sMid = proj₁ q2
%%         r1 : SemComm cm1 s1 sMid × SemComm cm2 sMid s2
%%         r1 = proj₂ q2
%%         r2 : SemComm cm1 s1 sMid
%%         r2 = proj₁ r1
%%         r3 : SemComm cm2 sMid s2
%%         r3 = proj₂ r1
%%         r4 : SemCond bMid sMid
%%         r4 = hyp1 s1 sMid q1 r2
%%     in hyp2 sMid s2 r4 r3
%% Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
%%           s1 s2 q1 q2
%%   = let hypThen : Satisfies (bPre /\ b) cmThen bPost
%%         hypThen = Soundness pThen
%%         hypElse : Satisfies (bPre /\ neg b) cmElse bPost
%%         hypElse = Soundness pElse
%%         rThen : RelOpState.comp
%%                   (RelOpState.delta (SemCond b))
%%                   (SemComm cmThen) s1 s2 ->
%%                 SemCond bPost s2
%%         rThen = λ h ->
%%                   let t1 : SemCond b s1 × SemComm cmThen s1 s2
%%                       t1 = (proj₂ (RelOpState.deltaRestPre
%%                                      (SemCond b)
%%                                      (SemComm cmThen) s1 s2)) h
%%                       t2 : SemCond (bPre /\ b) s1
%%                       t2 = (proj₂ (respAnd bPre b s1))
%%                            (q1 , proj₁ t1)
%%                   in hypThen s1 s2 t2 (proj₂ t1)
%%         rElse : RelOpState.comp
%%                   (RelOpState.delta (NotP (SemCond b)))
%%                   (SemComm cmElse) s1 s2 ->
%%                 SemCond bPost s2
%%         rElse = λ h ->
%%                   let t10 : (NotP (SemCond b) s1) ×
%%                             (SemComm cmElse s1 s2)
%%                       t10 = proj₂ (RelOpState.deltaRestPre
%%                                     (NotP (SemCond b)) (SemComm cmElse) s1 s2)
%%                             h
%%                       t6 : SemCond (neg b) s1
%%                       t6 = proj₂ (respNeg b s1) (proj₁ t10)
%%                       t7 : SemComm cmElse s1 s2
%%                       t7 = proj₂ t10
%%                       t8 : SemCond (bPre /\ neg b) s1
%%                       t8 = proj₂ (respAnd bPre (neg b) s1)
%%                            (q1 , t6)
%%                   in hypElse s1 s2 t8 t7
%%     in when rThen rElse q2
%% Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
%%   = proj₂ (respAnd bInv (neg b) s2) t20
%%     where
%%       hyp : Satisfies (bInv /\ b) cm' bInv
%%       hyp = Soundness pr
%%       n : $mathbb{N}$
%%       n = proj₁ q2
%%       Rel1 : $mathbb{N}$ -> Rel State (Level.zero)
%%       Rel1 = λ m ->
%%                RelOpState.repeat
%%                  m
%%                  (RelOpState.comp (RelOpState.delta (SemCond b))
%%                                   (SemComm cm'))
%%       t1 : RelOpState.comp
%%              (Rel1 n)
%%              (RelOpState.delta (NotP (SemCond b))) s1 s2
%%       t1 = proj₂ q2
%%       t15 : (Rel1 n s1 s2) × (NotP (SemCond b) s2)
%%       t15 = proj₂ (RelOpState.deltaRestPost
%%                     (NotP (SemCond b)) (Rel1 n) s1 s2)
%%               t1
%%       t16 : Rel1 n s1 s2
%%       t16 = proj₁ t15
%%       t17 : NotP (SemCond b) s2
%%       t17 = proj₂ t15
%%       lem1 : (m : $mathbb{N}$) -> (ss2 : State) -> Rel1 m s1 ss2 ->
%%              SemCond bInv ss2
%%       lem1 $mathbb{N}$.zero ss2 h
%%         = substId1 State (proj₂ h) (SemCond bInv) q1
%%       lem1 ($mathbb{N}$.suc n) ss2 h
%%         = let hyp2 : (z : State) -> Rel1 n s1 z ->
%%                      SemCond bInv z
%%               hyp2 = lem1 n
%%               s20 : State
%%               s20 = proj₁ h
%%               t21 : Rel1 n s1 s20
%%               t21 = proj₁ (proj₂ h)
%%               t22 : (SemCond b s20) × (SemComm cm' s20 ss2)
%%               t22 = proj₂ (RelOpState.deltaRestPre
%%                             (SemCond b) (SemComm cm') s20 ss2)
%%                     (proj₂ (proj₂ h))
%%               t23 : SemCond (bInv /\ b) s20
%%               t23 = proj₂ (respAnd bInv b s20)
%%                     (hyp2 s20 t21 , proj₁ t22)
%%           in hyp s20 ss2 t23 (proj₂ t22)
%%       t20 : SemCond bInv s2 × SemCond (neg b) s2
%%       t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17
%% \end{lstlisting}

\coderef{agda-hoare-prim-soundness} は \verb/HTProof/ で記述された仕様を、実際に満たすことが可能であることを \verb/Satisfies/ が返す。
証明部分では \verb/HTProof/ で構成された使用を受け取り、 \verb/Soundness/ が対応した証明を返すようになっている。


\begin{lstlisting}[caption=HTProof の Soundness への適用,label=agda-hoare-prim-soundness]
PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
            HTProof bPre cm bPost -> Satisfies bPre cm bPost
PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht
\end{lstlisting}


\coderef{agda-hoare-prim-proof} では \coderef{agda-hoare-prog} の \verb/program/ の Hoare Logic での命題である。
この証明では初期状態\verb/initCond/と実行するコマンド群\verb/program/を受け取り終了状態として \verb/termCond/ が \verb/true/ であることを示す。

\begin{lstlisting}[caption=while program の健全性,label=agda-hoare-prim-proof]
proofOfProgram : (c10 : $mathbb{N}$) → (input output : Env )
  → initCond input ≡ true
  → (SemComm (program c10) input output)
  → termCond {c10} output ≡ true
proofOfProgram c10 input output ic sem  = PrimSoundness (proof1 c10) input output ic sem
\end{lstlisting}

この証明は実際に構築した仕様である \verb/proof1/ を \verb/\verb/PrimSoundness/ に入力として渡すことで満たすことができる。
ここまで記述することで Agda 上の Hoare Logic を用いた \verb/while program/ を検証することができた。