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

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

例として現在 Agda に対応させたもの \cite{agda2-hoare}の Command と証明のためのルールを使って Hoare Logic を実装した。
\ref{agda-hoare} は Agda上での Hoare Logic の構築子である。

例として Code \ref{c-while} のようなプログラムを記述した。

\begin{lstlisting}[caption=while Loop Program,label=c-while]
  n = 10;
  i = 0;

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

$Env$ は Code \ref{c-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。

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

Cond は Hoare Logic の Condition で、 Env を受け取って　Bool 値を返す関数となっている。

Agda のデータで定義されている Comm は Hoare Logic での Command を表す。

Skip は何も変更しない Command で、 Abort はプログラムを中断する Command である。

PComm は PrimComm を受けて Command を返す型で定義されており、 変数を代入するときに使われる。

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

If は Cond と Comm を2つ受け取り、 Cond が true か false かで 実行する Comm を変える Command である。

While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。

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

 Code \ref{agda-hoare-prog}は Code \ref{c-while}で書いた While Loop を Hoare Logic での Comm で記述したものである。
ここでの $\$$は $()$の対応を合わせる 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 は Command をならべているだけである。
この Comm を Agda 上で実行するため、  Code \ref{agda-hoare-interpret} のような interpreter を記述した。


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

 Code \ref{agda-hoare-interpret}は 初期状態の Env と 実行する Command の並びを受けとって、実行後の Env を返すものとなっている。

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

 Code \ref{agda-hoare-run}のように interpret に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価してやると$record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。


\section{Agda 上での Hoare Logic の部分正当性}
ここでは先程例とした \ref{?} の部分正当性の検証を行う。

 Code \ref{agda-hoare-rule} は Agda 上での Hoare Logic での Command の検証である。
HTProof では Condition と Command もう一つ Condition を受け取って、 Set を返す Agda のデータとして表現されている。

PrimRule は Code \ref{axiom-taut} の Axiom という関数を使い、事前条件が成り立っている時、
実行後に事後条件が成り立つならば、 PComm で変数に値を代入できることを保証している。

SkipRule は Condition を受け取ってそのままの Condition を返すことを保証する。

AbortRule は PreContition を受け取って、Abort を実行して終わるルールである。

WeakeningRule は \ref{axiom-taut} の Tautology という関数を使って通常の逐次処理から、
WhileRule のみに適応されるループ不変変数に移行する際のルールである。

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

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

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

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

Code \ref{agda-hoare-rule}を使って Code \ref{agda-while}の whileProgram の仕様を構成する。

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

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

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

それぞれの Rule の中にそこで証明する必要のある補題が lemma で埋められている。
lemma1 から lemma5 の証明は幅を取ってしまうため、 全体は付録に載せる。

これらの lemma は HTProof の Rule に沿って必要なものを記述されており、
lemma1 では PreCondition と PostCondition が存在するときの代入の保証、
lemma2 では While Loop に入る前の Condition からループ不変条件への変換の証明、
lemma3 では While Loop 内での PComm の代入の証明、
lemma4 では While Loop を抜けたときの Condition の整合性、
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 は Code \ref{agda-hoare-prog}の program と似た形をとっている。
Hoare　Logic では Comannd に対応する証明規則があるため、仕様はプログラムに対応している。


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

\ref{agda-hoare-satisfies} は Hoare Logic 上での部分正当性を確かめるための関数である。
 SemComm では Comm を受け取って成り立つ関係を返す。
 Satisfies では Pre Condition と Command、 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}

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

\ref{agda-hoare-soundness} の Soundness では HTProof を受け取り、 Satisfies に合った証明を返す。
Soundness では HTProof に記述されている Rule でパターンマッチを行い、対応する証明を適応している。

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

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


\begin{lstlisting}[caption=?,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}

\ref{agda-hoare-prim-proof} は \ref{agda-hoare-prog} の program の Hoare Logic での証明である。
この証明では初期状態$initCond$と実行するコマンド群$program$を受け取り終了状態として $termCond$ が 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}


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