Mercurial > hg > Papers > 2019 > oshiro-thesis

comparison final_main/chapter5.tex @ 33:c9142e57399f default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
uodate maintex
author e155702
date Thu, 21 Feb 2019 09:46:47 +0900
parents 83f997abf3b5
children
comparison
equal deleted inserted replaced
32:e2ec8297e712 33:c9142e57399f
1 \chapter{Agda による CbC の証明} 1 \chapter{}
2
3 前章では Agda で CodeGear や DataGear の定義を示した。また、 CbC のコード
4 を Agda にマッピングし等価なコードを生成できることを示した。
5 本章では前章で生成した Interface の Stack や Tree のコードを使い Agda で
6 Interface を経由したコードでの証明が可能であることを示す。
7
8 % Hoare Logic ベースで証明をすすめる〜みたいなとこをどっかにいれたい。
9 % ↑ 上は Tree のコードが証明できないことを示して、その次の章に Hoare Logic でこ
10 % んな感じにするとできるのでは？っていう感じにしよ
11
12 \section{Agda による Interface 部分を含めた Stack の部分的な証明}
13 \label{src:agda-interface-stack}
14
15 % Stack の仕様記述
16 ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。
17
18 Stack の処理として様々な性質が存在する。例えば、
19
20 \begin{itemize}
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}
27
28 などの性質がある。
29
30 本セクションでは「どのような状態の Stack でも、値を push した後 pop した値は直前
31 に入れた値と一致する」という性質を証明する。
32
33
34 % この証明では任意の Stack に2回 push したあと2回 pop すると push したものと同じ
35 % ものが受け取れることを 証明している。
36
37 まず始めに不定状態の Stack を定義する。ソースコード~\ref{src:agda-in-some-state}
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
45 % Agda でも継続を使った書き方で Interface 部分の実装を示した。
46
47 この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー
48 タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が
49 Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として
50 型に書かれている。
51
52 % この辺ちょっと怪しい感じ
53 この関数本体で返ってくる値は$ x \equiv x1 と y \equiv y1$　のため record でまと
54 めて refl で推論が通る。
55 これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも
56 のを受け取れることが証明できた。
57
58
59 % \lstinputlisting[label=src:agda-Test, caption=]{src/AgdaStackTest.agda.replaced}
60
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 ${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。
77
78 \lstinputlisting[label=src:agda-tree-proof, caption=Tree Interface の証
79 明]{src/AgdaTreeProof.agda.replaced}
80
81 この Tree の証明では、不定状態の Tree を redBlackInSomeState で作成し、その状態の Tree
82 に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの
83 である。
84
85 しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した
86 Node が存在するのか、などの条件や、 Get した Node と Put した Node が合同なのか、
87 key の値が等しい場合の eq は合同と同義であるのか等の様々な補題を証明する必要が
88 あった。今回この証明では Put した Node と Get した
89 Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合
90 同であることを示すことが困難であった。
91
92 今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を
93 行おうと考えている。
94
95 \section{Hoare Logic}
96 \label{hoare-logic}
97
98 Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正
99 しさを推論する手法である。図\ref{fig:hoare}のように、 P を前状態(Pre Condition)
100 、C を処理(Command) 、 Q を後状態(Post Condition) とし、$\{P\} \ C \ \{Q\}$ のように考えたとき、
101 プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といった形で考える事ができる。
102
103 \begin{figure}[htpb]
104 \begin{center}
105 \scalebox{0.6}[0.6]{\includegraphics{fig/hoare-logic.pdf}}
106 \end{center}
107 \caption{hoare logicの流れ}
108 \label{fig:hoare}
109 \end{figure}
110
111
112 このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい
113 動きをすることを証明することができる。
114
115 この Hoare Logic の前状態、処理、後状態を CodeGear、 input/output の DataGear が表
116 \ref{fig:cbc-hoare} のように表せるのではないか考えている。
117
118 \begin{figure}[htpb]
119 \begin{center}
120 \scalebox{0.8}[0.8]{\includegraphics{fig/cbc-hoare.pdf}}
121 \end{center}
122 \caption{cbc と hoare logic}
123 \label{fig:cbc-hoare}
124 \end{figure}
125
126 この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると
127 Pre Condition が CodeGear に入力として与えられる Input DataGear、Command が
128 CodeGear、 Post Condition を Output DataGear として当てはめることができると考えて
129 いる。
130
131 今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ Agda に
132 当てはめ、幾つかの実装を証明していく。
133
134 % Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
135 % 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。
136 %%
137 % 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導
138 % 入した。
139 %%