\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\}\]
といった形で表される。
この3つ組は Hoare Triple と呼ばれる。

Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。

Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
これらを満たし、事前条件から事後条件を導けることを検証することで 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/を減らす、
疑似プログラムである。

このプログラムでの状態は、初めの $n = 10$、 $i = 0$ を代入する条件、
while loop 中に成り立っている条件を $n + i = 10$、
while loop が終了したとき成り立っている条件を $i = 10$
としている。

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/Comm/を \verb/Seq/ でつないでいき、最終的な状態にたどり着くと値を返して止まる。


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

比較しやすいように \coderef{c-while} を \coderef{c-while2} に再掲した。

\begin{lstlisting}[caption= while Loop (再掲),label=c-while2]
n = 10;
i = 0;

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

\lstinputlisting[caption= \coderef{c-while2} と対応した 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}
この program は Comm 型のデータで作られた構文木と考えられる。

この構文木を解釈し、 Agda 上で実行するには、 \coderef{agda-hoare-interpret} の \verb/interpret/ 関数を用いる。

\lstinputlisting[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret]{src/agda-hoare-interpret.agda.replaced}

\verb/interpret/は 初期状態の \verb/Env/ と 実行する コマンド の並びを受けとって、実行後の \verb/Env/ を返す関数である。
この関数に初期の環境である \verb/Env/ と実行するコマンド \verb/Comm/ を渡すとコマンドに対応した処理を行い、実行後の環境が \verb/Env/ として返ってくる。
Agda には Termnation Checker\cite{Abel98foetus} が付いており、停止性が明確でないとエラーを出す。
\verb/interpret/ は明確に停止する条件がないため、 Agda でのコンパイル時にエラーが出る。

今回は停止条件を考えないために \verb/{-# TERMINATING #-}/ タグを付けることでエラーを抑制している。

\coderef{agda-hoare-run}のように \verb/interpret/ に \verb/vari = 0 , varn = 10/ の \verb/record/ を渡し、\coderef{agda-hoare-prog} で記述した program を代入した。
\begin{lstlisting}[caption=Agda での Hoare Logic の実行 ,label=agda-hoare-run]
test : Env
test =  interpret ( record { vari = 0  ; varn = 10 } ) program
\end{lstlisting}

実際にこの \verb/test/ 関数の評価を行うと \verb/record {vari = 10 ; varn = 0 }/ の \verb/Env/ が値として返る。
これにより、program として記述したコマンドベースのプログラムが Agda 上で実行できていることが分かる。


\section{while program の仕様記述}
先程記述した \coderef{agda-hoare-prog} の  \verb/program/ ではコマンドベースの実行のみで事前、事後条件が存在していなかった。
ここではコマンドの事前、事後条件を接続した形で \verb/program/を記述していく。
事前条件や事後条件が接続された
Hoare Logic ではコマンドに対応した仕様が存在しており、それらを組み合わせた形で
仕様を記述する必要がある。
この仕様を記述する際、事前の条件から必ず事後の条件が導かれている必要がある。

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

\verb/PrimRule/ は 事前条件 と PrimComm、 事後条件、
\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}

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

\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/ の証明は概要のみを示し、全体は付録\coderef{prim-proof}に載せることにする。

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

\lstinputlisting[caption=while loop の検証用記述,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}

Hoare Logic ではコマンドに対応した仕様が存在するため、 \verb/proof1/ は\coderef{agda-hoare-prog}の program に近い記述になる。


\section{Hoare Logic の健全性}
\coderef{agda-hoare-while} では Agda での Hoare Logic を用いた仕様の構成を行った。
ここでは、\coderef{agda-hoare-while} で構成した仕様が健全であるか検証する。

ここでの健全性はコマンドの仕様である HTProof がすべてつながっていて、
事前条件が成り立っているとき、コマンドが停止すると事後条件が成り立つことと、
コマンドは条件を意図した通りに遷移させることができることの両方を検証することで、
その両方が検証できたとき、この実行は正しいというものである。

\coderef{agda-hoare-satisfies} の \verb/SemComm/ では各 Comm で成り立つ関係を返す。
Hoare Logic のすべてのコマンドの事前条件から事後条件への遷移が記述されており、
\verb/Satisfies/ では 事前条件 と コマンド、 事後条件 を受け取って、
\verb/Comm/ がでの実行が \verb/SemComm/ を満たすことを示している。

詳しい記述は、現在の Agda に直した Hoare Logic の定義\cite{agda2-hoare} の RelOp.agda に記述されている。

\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/ のコードは量が多いため部分的に省略し、全文は現在の Agda に直した Hoare Logic の定義\cite{agda2-hoare} の Soundness.agda を確認してほしい。

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

\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/PrimSoundness/ に入力として渡すことで満たすことができる。
\coderef{agda-hoare-prim-proof} で、 Agda 上の Hoare Logic を用いた \verb/while program/ を検証することができた。
ここで書かれた健全性の検証の全体は付録の\coderef{prim-proof} に載せる。