Mercurial > hg > Papers > 2020 > ryokka-master
diff paper/hoare.tex @ 12:bf3288c36d7e
update abstract_eng
author | ryokka |
---|---|
date | Mon, 10 Feb 2020 17:26:24 +0900 |
parents | 831316a767e8 |
children | e8655e0264b8 |
line wrap: on
line diff
--- a/paper/hoare.tex Mon Feb 10 14:20:21 2020 +0900 +++ b/paper/hoare.tex Mon Feb 10 17:26:24 2020 +0900 @@ -85,19 +85,9 @@ プログラムはコマンド \verb/Comm/を \verb/Seq/ でつないでいき、最終的な状態にたどり着くと値を返して止まる。 - \coderef{agda-hoare-prog}は \coderef{c-while}で書いた While Loop を Hoare Logic でのコマンドで記述したものである。 -ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。 +\coderef{agda-hoare-prog}は \coderef{c-while}で書いた While Loop を Hoare Logic でのコマンドで記述したものである。ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。 -\lstinputlisting[caption= \coderef{c-while} と対応した 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} +比較しやすいように \coderef{c-while} を \coderef{c-while2} に再掲した。 \begin{lstlisting}[caption= while Loop (再掲),label=c-while-2] n = 10; @@ -109,24 +99,19 @@ } \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} -%% \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 #-}/ タグを付けている。 @@ -140,7 +125,6 @@ -- record { varn = 0 ; vari = 10 } \end{lstlisting} - \section{While Program の部分正当性} ここでは先程記述した \coderef{agda-hoare-prog} の部分正当性の検証を行う。 @@ -169,37 +153,6 @@ \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} @@ -284,127 +237,6 @@ \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/ が対応した証明を返すようになっている。