Mercurial > hg > Papers > 2018 > ryokka-thesis

comparison final_main/chapter5.tex @ 4:12204a2c2eda

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add .pdf and some section.
author ryokka
date Sun, 18 Feb 2018 21:43:41 +0900
parents 2155c6ff589f
children eafc166804f3
comparison
equal deleted inserted replaced
3:2155c6ff589f 4:12204a2c2eda
1 \chapter{Agda による CbC の証明} 1 \chapter{Agda による CbC の証明}
2 2
3 前章では Agda で CodeGear や DataGear の定義を示した。また、 CbC のコード 3 前章では Agda で CodeGear や DataGear の定義を示した。また、 CbC のコード
4 を Agda にマッピングし等価なコードを生成できることを示した。 4 を Agda にマッピングし等価なコードを生成できることを示した。
5 本章では前章で作成した Interface の Stack や Tree のコードを使い Agda で 5 本章では前章で生成した Interface の Stack や Tree のコードを使い Agda で
6 Interface を経由したコードでの証明が可能であることを示す。 6 Interface を経由したコードでの証明が可能であることを示す。
7 7
8 % Hoare Logic ベースで証明をすすめる〜みたいなとこをどっかにいれたい。 8 % Hoare Logic ベースで証明をすすめる〜みたいなとこをどっかにいれたい。
9 % ↑ 上は Tree のコードが証明できないことを示して、その次の章に Hoare Logic でこ 9 % ↑ 上は Tree のコードが証明できないことを示して、その次の章に Hoare Logic でこ
10 % んな感じにするとできるのでは？っていう感じにしよ 10 % んな感じにするとできるのでは？っていう感じにしよ
11 11
12 \section{Agda による Interface 部分を含めた Stack の部分的な証明} 12 \section{Agda による Interface 部分を含めた Stack の部分的な証明}
13 \label{agda-interface-stack}
13 14
14 % Stack の仕様記述 15 % Stack の仕様記述
16 ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。
15 17
16 Stack 18 Stack の処理として様々な性質が存在する。例えば、
17 19
18 この証明では任意の Stack に2回 push したあと2回 pop すると push したものと同じものが受け取れる 20 \begin{itemize}
19 ことを証明している。 21 \item Stack に push した値は存在する
22 \item Stack に push した値は取り出すことができる
23 \item Stack に push した値を pop した時、その値は Stack から消える
24 \item どのような状態の Stack に値を push しても中に入っているデータの順序は変わらない
25 \item どのような状態の Stack でも、値を push した後 pop した値は直前に入れた値と一致する
26 \end{itemize}
20 27
21 stackInSomeState 型は中身の分からない抽象的な Stack を作成している。リスト 28 などの性質がある。
22 \ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を2回 29
23 行い、 pop2 をして取れたデータは push したデータと同じものになることを証明してい 30 本セクションでは「どのような状態の Stack でも、値を push した後 pop した値は直前
24 る。 31 に入れた値と一致する」という性質を証明する。
32
33 % この証明では任意の Stack に2回 push したあと2回 pop すると push したものと同じ
34 % ものが受け取れることを 証明している。
35
36 まず始めに不定状態の Stack を定義する。ソースコード~\ref{src:agda-in-some-state}
37 の line1~2 で定義している stackInSomeState が不定状態の Stack である。
38 stackInSomeState 型は中身の分からない抽象的な Stack を作成している。ソースコー
39 ド~\ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を
40 2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明してい
41 る。
42
43 \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義とpush->push->pop2 の証明]{src/AgdaStackSomeState.agda.replaced}
44
25 % Agda でも継続を使った書き方で Interface 部分の実装を示した。 45 % Agda でも継続を使った書き方で Interface 部分の実装を示した。
26
27 \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義と
28 push->push->pop2 の証明]{src/AgdaStackSomeState.agda.replaced}
29 46
30 この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー 47 この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー
31 タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が 48 タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が
32 Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として 49 Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として
33 型に書かれている。 50 型に書かれている。
34 51
52 % この辺ちょっと怪しい感じ
35 この関数本体で返ってくる値は$ x \equiv x1 と y \equiv y1$　のため record でまと 53 この関数本体で返ってくる値は$ x \equiv x1 と y \equiv y1$　のため record でまと
36 めて refl で推論が通る。 54 めて refl で推論が通る。
37 これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも 55 これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも
38 のを受け取れることが証明できた。 56 のを受け取れることが証明できた。
39 57
40 58
41 % \lstinputlisting[label=src:agda-Test, caption=]{src/AgdaStackTest.agda.replaced} 59 % \lstinputlisting[label=src:agda-Test, caption=]{src/AgdaStackTest.agda.replaced}
42 60
43 \section{Agda による Interface 部分を含めた Tree の部分的な証明} 61 \section{Agda による Interface 部分を含めた Binary Tree の部分的な証明と課題}
62 ここでは Binary Tree の性質の一部に対して証明を行う。
63 Binary Tree の性質として挙げられるのは次のようなものである
64 % 上の２つはデータ構造として最低限守られるべき部分ではあるがとりあえず書いてる
65
66 \begin{itemize}
67 \item Tree に対して Node を Put することができる。
68 \item Tree に Put された Node は Delete されるまでなくならない。
69 \item Tree に 存在する Node とその子の関係は必ず「右の子 > Node」かつ「Node > 左の子」の関係になっている。
70 \item どのような状態の Tree に値を put しても Node と子の関係は保たれる
71 \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。
72 \end{itemize}
73
74 ここで証明する性質は
75
76 ${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。
44 77
45 78
79 \lstinputlisting[label=src:agda-tree-proof, caption=Tree Interface の証
80 明]{src/AgdaTreeProof.agda.replaced}
81
82 この Tree の証明では、不定状態の redBlackInSomeState 型を作成し、その状態の Tree
83 に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの
84 である。
85 しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した
86 Node が存在するのか、 Get した Node と Put した Node が合同なのか等の様々な補
87 題を証明し、全てが成り立つ必要がある。今回この証明では Put した Node と Get した
88 Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合
89 同であることを示すことが困難であった。
90
91 そのため、今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を
92 行おうと考えている。
46 93
47 \section{Hoare Logic} 94 \section{Hoare Logic}
95 \label{hoare-logic}
48 96
49 Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正 97 Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正
50 しさを推論する手法である。P を前状態(Precondition) 、C を処理(Command) 、 Q を 98 しさを推論する手法である。P を前状態(PreCondition) 、C を処理(Command) 、 Q を
51 後状態(Postcondition) とし、$\{P\} \ C \ \{Q\}$ のように考えたとき、 99 後状態(PostCondition) とし、$\{P\} \ C \ \{Q\}$ のように考えたとき、
52 プログラムは前状態を満たした後、処理を行い状態が後状態に変化する、といった形になる。 100 プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といっ
101 た形で考える事ができる。
53 102
54 このとき、後状態から前状態を推論することが〜... 103 このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい
104 動きをすることを証明することができる。
105 この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると
106 PreCondition が CodeGear に入力として与えられる Input DataGear、Command が
107 CodeGear、 PostCondition を Output DataGear として当てはめることができると考えて
108 いる。
55 109
56 Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。 110
57 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。 111 今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ、
112 幾つかの実装を証明していく。
113
114 % Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
115 % 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。
58 116
59 %% 117 %%
60 % 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導 118 % 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導
61 % 入した。 119 % 入した。
62 %% 120 %%
63