\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/を減らす、
疑似プログラムである。

このプログラムでの状態は、初めの $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-while-2]
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}
この Comm を Agda 上で実行するため、 \coderef{agda-hoare-interpret} の \verb/interpret/ 関数を作成した。

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

\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}


\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}

\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/ を検証することができた。