Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/hoare.tex @ 9:95a5f8e76944

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix cbc_agda, cbc_hoare and Conclusion.tex
author ryokka
date Fri, 07 Feb 2020 21:40:26 +0900
parents b8ff2bd1a5af
children 831316a767e8
comparison
equal deleted inserted replaced
8:b8ff2bd1a5af 9:95a5f8e76944
3 Floyd-Hoare Logic \cite{10.1145/363235.363259}(以下 Hoare Logic) とは 3 Floyd-Hoare Logic \cite{10.1145/363235.363259}(以下 Hoare Logic) とは
4 C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。 4 C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
5 Hoare Logic では事前条件が成り立つとき、何らかの計算(以下コマンド)を実行した後に 5 Hoare Logic では事前条件が成り立つとき、何らかの計算(以下コマンド)を実行した後に
6 事後条件が成り立つことを検証する。 6 事後条件が成り立つことを検証する。
7 事前条件を P 、 何らかの計算を C 、 事後条件を Q としたとき、 7 事前条件を P 、 何らかの計算を C 、 事後条件を Q としたとき、
8 ${P} C {Q}$ といった形で表される。 8 $\{P\}\ C \ \{Q\}$ といった形で表される。
9 Hoare Logic ではプログラムの部分的な正当性を検証することができ、 9 Hoare Logic ではプログラムの部分的な正当性を検証することができ、
10 事後条件のあとに別の コマンド をつなげてプログラムを構築することで、 10 事後条件のあとに別の コマンド をつなげてプログラムを構築することで、
11 シンプルな計算に対する検証することができる。 11 シンプルな計算に対する検証することができる。
12 12
13 本章は Agda で実装された Hoare Logic について解説し、 13 本章は Agda で実装された Hoare Logic について解説し、
15 15
16 16
17 \section{Hoare Logic} 17 \section{Hoare Logic}
18 現在 Agda 上での Hoare Logic は初期の Agda で実装されたもの \cite{agda-alpa}とそれを現在の Agda に対応させたもの \cite{agda2-hoare}が存在している。 18 現在 Agda 上での Hoare Logic は初期の Agda で実装されたもの \cite{agda-alpa}とそれを現在の Agda に対応させたもの \cite{agda2-hoare}が存在している。
19 19
20 ここでは現在 Agda に対応させたもの \cite{agda2-hoare}の コマンド と証明のためのルールを使用する。 20 ここでは現在 Agda に対応した Hoare Logic を使用する。
21 21
22 例として \coderef{c-while} のようなプログラムを記述した。 22 例として \coderef{c-while} のようなプログラムを記述した。
23 23 これは変数 \verb/n/ と \verb/i/ を持ち、\verb/n/が 0　より大きいとき、\verb/i/を増やし \verb/n/を減らす、
24 疑似プログラムである。
25 このプログラムを Hoare Logic 上で同様のプログラムを作成し、検証を行う。
24 \begin{lstlisting}[caption=while Loop Program,label=c-while] 26 \begin{lstlisting}[caption=while Loop Program,label=c-while]
25 n = 10; 27 n = 10;
26 i = 0; 28 i = 0;
27 29
28 while (n > 0) { 30 while (n > 0) {
29 i++; 31 i++;
30 n--; 32 n--;
31 } 33 }
32 \end{lstlisting} 34 \end{lstlisting}
33
34 35
35 36
36 \coderef{agda-hoare} は Agda 上での Hoare Logic の構築子である。 37 \coderef{agda-hoare} は Agda 上での Hoare Logic の構築子である。
37 \verb/Env/ は \coderef{c-while}の \verb/n/、 \verb/i/ といった変数をレコード型でまとめたもので、\verb/n/と\verb/i/それぞれが型として Agda 上での自然数の型である $\mathbb{N}$ を持つ。 38 \verb/Env/ は \coderef{c-while}の \verb/n/、 \verb/i/ といった変数をレコード型でまとめたもので、\verb/n/と\verb/i/それぞれが型として Agda 上での自然数の型である $\mathbb{N}$ を持つ。
38 39
87 %% $ While (λ env → lt zero (varn env ) ) 88 %% $ While (λ env → lt zero (varn env ) )
88 %% (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) 89 %% (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
89 %% $ PComm (λ env → record env {varn = ((varn env) - 1)} )) 90 %% $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
90 %% \end{lstlisting} 91 %% \end{lstlisting}
91 92
92 この Comm を Agda 上で実行するため、 \coderef{agda-hoare-interpret} のような関数を作成した。 93 この Comm を Agda 上で実行するため、 \coderef{agda-hoare-interpret} の \verb/interpret/ 関数を作成した。
93 94
94 95
95 \lstinputlisting[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret]{src/agda-hoare-interpret.agda.replaced} 96 \lstinputlisting[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret]{src/agda-hoare-interpret.agda.replaced}
96 %% \begin{lstlisting}[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret] 97 %% \begin{lstlisting}[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret]
97 %% {-# TERMINATING #-} 98 %% {-# TERMINATING #-}
109 %% \end{lstlisting} 110 %% \end{lstlisting}
110 111
111 \coderef{agda-hoare-interpret}は 初期状態の \verb/Env/ と 実行する コマンド の並びを受けとって、実行後の \verb/Env/ を返すものとなっている。 112 \coderef{agda-hoare-interpret}は 初期状態の \verb/Env/ と 実行する コマンド の並びを受けとって、実行後の \verb/Env/ を返すものとなっている。
112 \verb/interpret/ 関数は停止性を考慮していないため、 \verb/{-# TERMINATING #-}/ タグを付けている。 113 \verb/interpret/ 関数は停止性を考慮していないため、 \verb/{-# TERMINATING #-}/ タグを付けている。
113 114
114 \coderef{agda-hoare-run}のように \verb/interpret/ に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価すると $record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。 115 \coderef{agda-hoare-run}のように \verb/interpret/ に \verb/vari = 0 , varn = 0/ の \verb/record/ を渡し、 実行する \verb/Comm/ を渡して 評価すると \verb/record { varn = 0 ; vari = 10 }/ のような \verb/Env/ が返ってくる。
115 \verb/interpret/ で実行される コマンド は \coderef{agda-hoare-prog} で記述した While Loop するコマンドである 116 \verb/interpret/ で実行される コマンド は \coderef{agda-hoare-prog} で記述した While Loop するコマンドである
116 117
117 \begin{lstlisting}[caption=Agda での Hoare Logic の実行 ,label=agda-hoare-run] 118 \begin{lstlisting}[caption=Agda での Hoare Logic の実行 ,label=agda-hoare-run]
118 test : Env 119 test : Env
119 test = interpret ( record { vari = 0 ; varn = 0 } ) program 120 test = interpret ( record { vari = 0 ; varn = 0 } ) program
120
121 -- record { varn = 0 ; vari = 10 } 121 -- record { varn = 0 ; vari = 10 }
122 \end{lstlisting} 122 \end{lstlisting}
123 123
124 124
125 \section{While Program の部分正当性} 125 \section{While Program の部分正当性}
126 ここでは先程記述した \coderef{agda-hoare-prog} の部分正当性の検証を行う。 126 ここでは先程記述した \coderef{agda-hoare-prog} の部分正当性の検証を行う。
127 127
128 \coderef{agda-hoare-rule} で書かれている \verb/HTProof/ は Agda 上での Hoare Logic でのコマンドを検証するための命題をまとめたものである。 128 \coderef{hoare-rule} の \verb/HTProof/ は Agda 上での Hoare Logic でのコマンドに対応した性質を型としてまとめたものである。
129 \verb/HTProof/ では Pre-Condition とコマンド、Post-Condition を受け取って、 Set を返す Agda のデータとして表現されている。 129 \verb/HTProof/ では Pre-Condition とコマンド、Post-Condition を受け取って定義される Agda のデータである。
130 \coderef{agda-hoare} のコマンドで定義された \verb/Skip/、 \verb/Abort/、 \verb/PComm/、
131 \verb/Seq/、\verb/If/、\verb/While/、に対応した証明のための命題が存在している。
130 132
131 \verb/PrimRule/ は Pre-Condition と PrimComm、 Post-Condition、 133 \verb/PrimRule/ は Pre-Condition と PrimComm、 Post-Condition、
132 \coderef{axiom-taut} の \verb/Axiom/ 関数をが成り立つという命題を引数として受け取る。 134 \coderef{axiom-taut} の \verb/Axiom/ を引数として \verb/PComm/の入った \verb/HTProof/ を返す。
133 135
134 \verb/SkipRule/ は Condition を受け取ってそのままの Condition を返す。 136 \verb/SkipRule/ は Condition を受け取ってそのままの Condition を返す HTProof を返す。
135 137
136 \verb/AbortRule/ は PreContition を受け取って、Abort を実行して終わるルールである。 138 \verb/AbortRule/ は Pre-Contition を受け取って、\verb/Abort/ を実行する HTProof を返す。
137 139
138 \verb/WeakeningRule/ は \ref{axiom-taut} の Tautology という関数を使って通常の逐次処理から、 140 \verb/WeakeningRule/ は通常の Condition から制約を緩める際にに使用される。
139 \verb/WhileRule/ のみに適応されるループ不変変数に移行する際のルールである。 141 \ref{axiom-taut} の \verb/Tautology/ を使って Condition が同じであることを
140 142
141 \verb/SeqRule/ は3つの Condition と 2つの コマンド を受け取り、これらのプログラムの逐次的な実行を保証する。 143 \verb/SeqRule/ は3つの Condition と 2つの コマンド を受け取り、これらのプログラムの逐次的な実行を保証する。
142 144
143 IfRule は分岐に用いられ、3つの Condition と 2つの コマンド を受け取り、判定の Condition が成り立っているかいないかで実行する コマンド を変えるルールである。 145 \verb/IfRule/ は分岐に用いられ、3つの Condition と 2つの コマンド を受け取り、判定の Condition が成り立っているかいないかで実行する コマンド を変えるルールである。
144 この時、どちらかの コマンド が実行されることを保証している。 146 この時、どちらかの コマンド が実行されることを保証している。
145 147
146 WhileRule はループに用いられ、1つの コマンド と２つの Condition を受け取り、事前条件が成り立っている間、 コマンド を繰り返すことを保証している。 148 \verb/WhileRule/ はループに用いられ、1つの コマンド と２つの Condition を受け取り、事前条件が成り立っている間、 コマンド を繰り返すことを保証している。
147 149
148 \lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced} 150 \lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced}
149 151
150 152
151 153
177 %% WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> 179 %% WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
178 %% HTProof (bInv /\ b) cm bInv -> 180 %% HTProof (bInv /\ b) cm bInv ->
179 %% HTProof bInv (While b cm) (bInv /\ neg b) 181 %% HTProof bInv (While b cm) (bInv /\ neg b)
180 %% \end{lstlisting} 182 %% \end{lstlisting}
181 183
182 Code \ref{agda-hoare-rule}を使って Code \ref{agda-while}の whileProgram の仕様を構成する。 184 \coderef{hoare-rule}を使って \coderef{c-while}の WhileProgram の仕様を構成する。
183 185
184 \lstinputlisting[caption=Agda での Hoare Locig の構成,label=hoare-rule]{src/agda-hoare-rule.agda.replaced} 186 \lstinputlisting[caption=Agda での Hoare Locig の構成,label=hoare-rule]{src/agda-hoare-rule.agda.replaced}
185 187
186 全体の仕様は Code \ref{agda-hoare-while}の proof1 の様になる。 188 全体の仕様は Code \ref{agda-hoare-while}の \verb/proof1/ の様になる。
187 proof1 では型で initCond、 Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、 189 \verb/proof1/ では型で initCond、 Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、
188 initCond から program を実行し termCond に行き着く Hoare Logic の証明になる。 190 \verb/initCond/ から \verb/program/ を実行し \verb/termCond/ に行き着く Hoare Logic の証明になる。
189 191
190 それぞれの Condition は Rule の後に記述されている {} に囲まれた部分で、 192 それぞれの Condition は Rule の後に記述されている \verb/{}/ に囲まれた部分で、
191 initCondのみ無条件で true を返す Condition になっている。 193 \verb/initCond/のみ無条件で \verb/true/ を返す Condition になっている。
192 194
193 それぞれの Rule の中にそこで証明する必要のある補題が lemma で埋められている。 195 それぞれの Rule の中にそこで証明する必要のある補題が \verb/lemma/ で埋められている。
194 lemma1 から lemma5 の証明は幅を取ってしまうため、 全体は付録に載せる。 196 \verb/lemma1/ から \verb/lemma5/ の証明は概要のみを示し、全体は付録に載せる。
195 197
196 これらの lemma は HTProof の Rule に沿って必要なものを記述されており、 198 これらの lemma は HTProof の Rule に沿って必要なものを記述されており、
197 lemma1 では PreCondition と PostCondition が存在するときの代入の保証、 199 \verb/lemma1/ では PreCondition と PostCondition が存在するときの代入の保証、
198 lemma2 では While Loop に入る前の Condition からループ不変条件への変換の証明、 200 \verb/lemma2/ では While Loop に入る前の Condition からループ不変条件への変換の証明、
199 lemma3 では While Loop 内での PComm の代入の証明、 201 \verb/lemma3/ では While Loop 内での PComm の代入の証明、
200 lemma4 では While Loop を抜けたときの Condition の整合性、 202 \verb/lemma4/ では While Loop を抜けたときの Condition の整合性、
201 lemma5 では While Loop を抜けた後のループ不変条件からCondition への変換と termCond への移行の整合性を保証している。 203 \verb/lemma5/ では While Loop を抜けた後のループ不変条件からCondition への変換と termCond への移行の整合性を保証している。
202
203 204
204 \lstinputlisting[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]{src/agda-hoare-while.agda.replaced} 205 \lstinputlisting[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]{src/agda-hoare-while.agda.replaced}
205 %% \begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while] 206 %% \begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]
206 %% proof1 : HTProof initCond program termCond 207 %% proof1 : HTProof initCond program termCond
207 %% proof1 = 208 %% proof1 =
211 %% WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} 212 %% WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
212 %% $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) 213 %% $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 )
213 %% $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 214 %% $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5
214 %% \end{lstlisting} 215 %% \end{lstlisting}
215 216
216 proof1 は Code \ref{agda-hoare-prog}の program と似た形をとっている。 217 proof1 は\coderef{agda-hoare-prog}の program と似た形をとっている。
217 Hoare　Logic では Comannd に対応する証明規則があるため、仕様はプログラムに対応している。 218 Hoare　Logic では Comannd に対応する証明規則があるため、仕様はプログラムに対応している。
218 219
219 220
220 \section{Hoare Logic での健全性} 221 \section{Hoare Logic での健全性}
221 \ref{agda-hoare-while} では Agda での Hoare Logic を用いた仕様の構成を行った。 222 \coderef{agda-hoare-while} では Agda での Hoare Logic を用いた仕様の構成を行った。
222 この仕様が実際に正しく動作するかどうか(健全性)を証明する必要がある。 223 この仕様で実際に正しく動作するかどうか(健全性)を検証する必要がある。
223 224
224 \ref{agda-hoare-satisfies} は Hoare Logic 上での部分正当性を確かめるための関数である。 225 \coderef{agda-hoare-satisfies} は Hoare Logic 上での部分正当性を確かめるための関数である。
225 SemComm では Comm を受け取って成り立つ関係を返す。 226 \verb/SemComm/ では Comm を受け取って成り立つ関係を返す。
226 Satisfies では Pre Condition と コマンド、 Post Condition を受け取って、 227 \verb/Satisfies/ では Pre Condition と コマンド、 Post Condition を受け取って、
227 Pre Condition から Post Condition を正しく導けるという仕様を返す。 228 Pre Condition から Post Condition を正しく導けるという仕様を返す。
228 229
229 \lstinputlisting[caption= State Sequence の部分正当性,label=agda-hoare-satisfies]{src/agda-hoare-satisfies.agda.replaced} 230 \lstinputlisting[caption= State Sequence の部分正当性,label=agda-hoare-satisfies]{src/agda-hoare-satisfies.agda.replaced}
230 231
231 %% \begin{lstlisting}[caption= State Sequence の部分正当性,label=agda-hoare-satisfies] 232 %% \begin{lstlisting}[caption= State Sequence の部分正当性,label=agda-hoare-satisfies]
256 %% SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2 257 %% SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2
257 %% \end{lstlisting} 258 %% \end{lstlisting}
258 259
259 これらの仕様を検証することでそれぞれの コマンド に対する部分正当性を示す。 260 これらの仕様を検証することでそれぞれの コマンド に対する部分正当性を示す。
260 261
261 \ref{agda-hoare-soundness} の Soundness では HTProof を受け取り、 Satisfies に合った証明を返す。 262 \coderef{agda-hoare-soundness} の \verb/Soundness/ では \verb/HTProof/ を受け取り、 \verb/Satisfies/ に合った証明を返す。
262 Soundness では HTProof に記述されている Rule でパターンマッチを行い、対応する証明を適応している。 263 \verb/Soundness/ では \verb/HTProof/ に記述されている Rule でパターンマッチを行い、対応する証明を適応している。
264 \verb/Soundness/ のコードは量が多いため部分的に省略し、全文は付録に載せることにする。
263 265
264 \lstinputlisting[caption=Agda での Hoare Logic の健全性,label=agda-hoare-soundness]{src/agda-hoare-soundness.agda.replaced} 266 \lstinputlisting[caption=Agda での Hoare Logic の健全性,label=agda-hoare-soundness]{src/agda-hoare-soundness.agda.replaced}
265 %% ↑ ながすぎて無理説ある
266 267
267 %% \begin{lstlisting}[caption=Agda での Hoare Logic の健全性,label=agda-hoare-soundness] 268 %% \begin{lstlisting}[caption=Agda での Hoare Logic の健全性,label=agda-hoare-soundness]
268 %% Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> 269 %% Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
269 %% HTProof bPre cm bPost -> Satisfies bPre cm bPost 270 %% HTProof bPre cm bPost -> Satisfies bPre cm bPost
270 %% Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2 271 %% Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
383 %% in hyp s20 ss2 t23 (proj₂ t22) 384 %% in hyp s20 ss2 t23 (proj₂ t22)
384 %% t20 : SemCond bInv s2 × SemCond (neg b) s2 385 %% t20 : SemCond bInv s2 × SemCond (neg b) s2
385 %% t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17 386 %% t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17
386 %% \end{lstlisting} 387 %% \end{lstlisting}
387 388
388 \ref{agda-hoare-prim-soundness} は HTProof で記述された仕様を、実際に構成可能な仕様を満たしているかを確認する Satisfies を返す。 389 \coderef{agda-hoare-prim-soundness} は \verb/HTProof/ で記述された仕様を、実際に満たすことが可能であることを \verb/Satisfies/ が返す。
389 照明部分では HTProof で構成された使用を受け取り、 Soundness が対応した証明を返すようになっている。 390 証明部分では \verb/HTProof/ で構成された使用を受け取り、 \verb/Soundness/ が対応した証明を返すようになっている。
390 391
391 392
392 \begin{lstlisting}[caption=?,label=agda-hoare-prim-soundness] 393 \begin{lstlisting}[caption=HTProof の Soundness への適用,label=agda-hoare-prim-soundness]
393 PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> 394 PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
394 HTProof bPre cm bPost -> Satisfies bPre cm bPost 395 HTProof bPre cm bPost -> Satisfies bPre cm bPost
395 PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht 396 PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht
396 \end{lstlisting} 397 \end{lstlisting}
397 398
398 \ref{agda-hoare-prim-proof} は \ref{agda-hoare-prog} の program の Hoare Logic での証明である。 399
399 この証明では初期状態$initCond$と実行するコマンド群$program$を受け取り終了状態として $termCond$ が true であることを示す。 400 \coderef{agda-hoare-prim-proof} では \coderef{agda-hoare-prog} の \verb/program/ の Hoare Logic での命題である。
401 この証明では初期状態\verb/initCond/と実行するコマンド群\verb/program/を受け取り終了状態として \verb/termCond/ が \verb/true/ であることを示す。
400 402
401 \begin{lstlisting}[caption=while program の健全性,label=agda-hoare-prim-proof] 403 \begin{lstlisting}[caption=while program の健全性,label=agda-hoare-prim-proof]
402 proofOfProgram : (c10 : $mathbb{N}$) → (input output : Env ) 404 proofOfProgram : (c10 : $mathbb{N}$) → (input output : Env )
403 → initCond input ≡ true 405 → initCond input ≡ true
404 → (SemComm (program c10) input output) 406 → (SemComm (program c10) input output)
405 → termCond {c10} output ≡ true 407 → termCond {c10} output ≡ true
406 proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem 408 proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem
407 \end{lstlisting} 409 \end{lstlisting}
408 410
409 411 この証明は実際に構築した仕様である \verb/proof1/ を \verb/\verb/PrimSoundness/ に入力として渡すことで満たすことができる。
410 この証明は実際に構築した仕様である $proof1$ を $PrimSoundness$ に入力することで満たすことができる。 412 ここまで記述することで Agda 上の Hoare Logic を用いた \verb/while program/ を検証することができた。
411 ここまで記述することで Agda 上の Hoare Logic を用いた while program を検証することができた。