comparison Paper/sigos.tex @ 6:4312a27022d1

fix
author ryokka
date Mon, 23 Apr 2018 18:11:46 +0900
parents 341b4c04597f
children 06a1339fbda4
comparison
equal deleted inserted replaced
5:341b4c04597f 6:4312a27022d1
1 \documentclass[techrep]{ipsjpapers} 1 \documentclass[techrep]{ipsjpapers}
2 \usepackage[dvipdfmx]{graphicx} 2 \usepackage[dvipdfmx]{graphicx}
3 \usepackage{url} 3
4 \usepackage{listings,jlisting} 4 \usepackage{listings}
5 \usepackage{enumitem} 5 \usepackage{enumitem}
6 \usepackage{bussproofs} 6 % \usepackage{bussproofs}
7 \usepackage{amsmath}
8 \usepackage{multirow} 7 \usepackage{multirow}
9 \usepackage{here} 8 \usepackage{here}
9 \usepackage{ucs}
10 \usepackage{autofe}
11 \usepackage{fancyvrb}
12 \usepackage{ascmac}
13 \usepackage[deluxe, multi]{otf}
14 \usepackage{url}
10 \usepackage{cite} 15 \usepackage{cite}
11 \usepackage{listings} 16 \usepackage{listings}
12 \usepackage{amssymb} 17 \usepackage{amssymb}
13 %\usepackage{ucs} 18 \usepackage{amsmath}
14 %\usepackage[utf8x]{inputenc} 19 \usepackage{colonequals}
20 \usepackage[utf8x]{inputenc}
21
22 \DeclareUnicodeCharacter{8852}{$\sqcup$}
23 \DeclareUnicodeCharacter{8909}{$\simeq$}
24
25 % \uc@dclc{8852}{default}{\ensuremath{\sqcup}}
15 26
16 \lstset{ 27 \lstset{
17 language=C, 28 language=C,
18 tabsize=2, 29 tabsize=2,
19 frame=single, 30 frame=single,
36 } 47 }
37 \renewcommand{\lstlistingname}{Code} 48 \renewcommand{\lstlistingname}{Code}
38 \usepackage{caption} 49 \usepackage{caption}
39 \captionsetup[lstlisting]{font={small,tt}} 50 \captionsetup[lstlisting]{font={small,tt}}
40 51
41 \input{dummy.tex} %% Font 52 % \input{dummy.tex} %% Font
42 53
43 % ユーザが定義したマクロなど. 54 % ユーザが定義したマクロなど.
44 \makeatletter 55 \makeatletter
56 % \def<\UTF{2294}>{$\sqcup$}
45 57
46 \begin{document} 58 \begin{document}
47 59
48 % 和文表題 60 % 和文表題
49 \title{GearsOS の Agda による記述と検証} 61 \title{GearsOS の Agda による記述と検証}
88 \maketitle 100 \maketitle
89 101
90 % 本文はここから始まる 102 % 本文はここから始まる
91 103
92 % Introduce 104 % Introduce
93 % Code Gear は関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。 105 % Code Gear は関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。
94 106
95 % 研究目的 107 % 研究目的
96 108
97 % 信頼性の高いOS 109 % 信頼性の高いOS
98 110
220 ける。 232 ける。
221 また、複数の引数を取る関数の型は \verb+A -> A -> B+ のように書ける。この 233 また、複数の引数を取る関数の型は \verb+A -> A -> B+ のように書ける。この
222 時の型は \verb+A -> (A -> B)+ のように考えられる。 234 時の型は \verb+A -> (A -> B)+ のように考えられる。
223 前節に出てきた pushStack の型(Code \ref{push-stack})はこの例である。 235 前節に出てきた pushStack の型(Code \ref{push-stack})はこの例である。
224 pushStack の型の本体は Code \ref{push-stack-func}のようになる。 236 pushStack の型の本体は Code \ref{push-stack-func}のようになる。
237 Code \ref{push-stack-funk} では\verb+\+の表記が出ている。これは$\lambda$式で初め
238 の pushStack で返した stack である s1 を受け取り、次の関数へ渡している。 Agda の
239 $\lambda$式では\verb+\+の他に\verb+λ+で表記することもできる。
240 \verb++
225 241
226 \begin{lstlisting}[caption=pushStack の関数定義,label=push-stack-func] 242 \begin{lstlisting}[caption=pushStack の関数定義,label=push-stack-func]
227 pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) 243 pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
228 \end{lstlisting} 244 \end{lstlisting}
229 245
234 定義を行う際は \verb+record+ のキーワード後にレコード名、型、 \verb+where+ の後 250 定義を行う際は \verb+record+ のキーワード後にレコード名、型、 \verb+where+ の後
235 に \verb+field+ キーワードを入れ、フィールド名と型名をを列挙する。 251 に \verb+field+ キーワードを入れ、フィールド名と型名をを列挙する。
236 \verb+record+ の定義の例として Stack のデータを操作する際に必要なレコード型のデータ 252 \verb+record+ の定義の例として Stack のデータを操作する際に必要なレコード型のデータ
237 \verb+Element+ (Code \ref{element-impl})を例とする。 253 \verb+Element+ (Code \ref{element-impl})を例とする。
238 254
239 \verb+Element+ は単方向のリスト構造になっており、 \verb+datum+ に格納するデータ、 255 \verb+Element+ は単方向のリスト構造になっており、 \verb+datum+ に格納する任意の
240 \verb+next+ に次のデータを持っている。 256 型のデータ、\verb+next+ に次のElement型のデータを持っている。
241 257
242 \begin{lstlisting}[caption=Element の定義,label=element-impl] 258 \begin{lstlisting}[caption=Element の定義,label=element-impl]
243 record Element {l : Level} (a : Set l) : Set l where 259 record Element {l : Level} (a : Set l) : Set l where
244 inductive 260 inductive
245 constructor cons 261 constructor cons
246 field 262 field
247 datum : a -- `data` is reserved by Agda. 263 datum : a -- `data` is reserved by Agda.
248 next : Maybe (Element a) 264 next : Maybe (Element a)
249 \end{lstlisting} 265 \end{lstlisting}
250 266
251 % 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
252 % これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので
253
254 %% element の定義、縦棒 | の定義 267 %% element の定義、縦棒 | の定義
255 %% SingleLinkedStack の説明に必要なものだけ 268 %% SingleLinkedStack の説明に必要なものだけ
269 % パターンマッチの説明、 | の定義、説明用のあれ。
256 %% push と pop だけ書いて必要なものだけ説明する 270 %% push と pop だけ書いて必要なものだけ説明する
257 %% testStack08 を説明する。 271 %% testStack08 を説明する。
258 272
259 パターンマッチの説明、 | の定義、説明用のあれ。 273 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
260 274 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
261 \begin{lstlisting}[caption=test8,label=test8] 275 例として、 popStack の実装である popSingleLinkedStack を使う。
276
277 popSingleLinkedStack では \verb+stack+、 \verb+cs+ の2つの引数を取り、
278 \verb+with+キーワードの後に\verb+Maybe+型の\verb+top+でパターンマッチしている。
279 \verb+Maybe+型は\verb+nothing+と\verb+Just+のどちらかを返す。そのため、両方のパ
280 ターンにマッチしている必要がある。
281 パターンマッチの記述では関数名、引数、を列挙して\verb+|+の後に \verb+パターン名 =+
282 で挙動を書く場合と、 Code \ref{pattern-match}のように、\verb+... |+で関数名、引数
283 を省略して\verb+パターン名 =+で挙動を書く方法がある。
284
285 また、Agda では特定の関数内のみで利用できる関数を \verb+where+ 句で記述できる。
286 スコープは \verb+where+ 句が存在する関数内部のみであるため、名前空間が汚染させる
287 ことも無い。
288 \verb+where+ 句は利用したい関数の末尾にインデント付きで \verb+where+ キーワード
289 を記述し、改行の後インデントをして関数内部で利用する関数を定義する。
290
291 \begin{lstlisting}[caption=パターンマッチの例,label=pattern-match]
292 popSingleLinkedStack stack cs with (top stack)
293 ... | Nothing = cs stack Nothing
294 ... | Just d = cs stack1 (Just data1)
295 where
296 data1 = datum d
297 stack1 = record { top = (next d) }
298 \end{lstlisting}
299
300 pushStack と popStack を使った証明の例は Code\ref{push-pop}のようになる。
301 ここでは、stack に対し push を行なった直後に pop を行うと取れるデータは push し
302 たものと同じになるという論理式を型に書き、証明を行なった。
303
304 \begin{lstlisting}[caption=pushとpopを使った証明,label=push-pop]
305 push->pop : {l : Level } {D : Set l} (x : D ) (s : SingleLinkedStack D ) -> pushStack ( stackInSomeState s ) x ( \s1 -> popStack s1 ( \s3 x1 -> (Just x ≡ x1)))
306 push->pop {l} {D} x s = refl
307 \end{lstlisting}
308
309 証明の関数部分に出てきた\verb+refl+は左右の項が等しいことを表す$x \equiv x$を生
310 成する項であり、$x \equiv x$を証明したい場合には\verb+refl+と書く事ができる。
311
312 \begin{lstlisting}[caption=reflectionの定義,label=refl]
313 data _≡_ {a} {A : Set a} (x : A) : A → Set a where
314 refl : x ≡ x
315 \end{lstlisting}
316
317 また、Code \ref{test08}のように継続を用いて記述することで関数の中で計算途中のデー
318 タ内部を確認することができた。ここでは$\lambda$式のネストになり見づらいため、
319 \verb+()+をまとめる糖衣構文\verb+$+を使っている。\verb+$+を先頭に書くことで後ろ
320 の一行を\verb+()+でくくることができる。
321
322 Code \ref{test08} のように記述し、\verb+C-c C-n+(Compute nomal form)で関数を評価
323 すると最後に返している stack の top を確認することができる。top の中身は
324 Code\ref{test08} の中にコメントとして記述した。
325 \begin{lstlisting}[caption=継続によるテスト,label=test08]
262 testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1 326 testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
263 $ \s -> pushSingleLinkedStack s 2 327 $ \s -> pushSingleLinkedStack s 2
264 $ \s -> pushSingleLinkedStack s 3 328 $ \s -> pushSingleLinkedStack s 3
265 $ \s -> pushSingleLinkedStack s 4 329 $ \s -> pushSingleLinkedStack s 4
266 $ \s -> pushSingleLinkedStack s 5 330 $ \s -> pushSingleLinkedStack s 5
267 $ \s -> top s 331 $ \s -> top s
268 \end{lstlisting} 332
269 333 -- Just (cons 5 (Just (cons 4 (Just (cons 3 (Just (cons 2 (Just (cons 1 Nothing)))))))))
270 % パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。 334 \end{lstlisting}
271 % 例えば、Bool 型を受け取る関数で \verb+true+ の時の挙動のみを書くことはできない。 335
272 % なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。 336
273 % 例えばリスト~\ref{agda-pattern}の not は x には true しか入ることは無い。
274 % なお、マッチした値以外の挙動をまとめて書く際には \verb+_+ を用いることもできる。
275
276 % \lstinputlisting[label=agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}
277
278 % Agda にはラムダ式が存在している。ラムダ式とは関数内で生成できる無名の関数であり、
279 % \verb+\arg1 arg2 -> function body+ のように書くことができる。
280 % 例えば Bool 型の引数 \verb+b+ を取って not を適用する \verb+not-apply+ をラムダ式で書くとリスト~\ref{agda-lambda}のようになる。
281 % 関数 \verb+not-apply+ をラムダ式を使わずに定義すると \verb+not-apply-2+ になるが、この二つの関数は同一の動作をする。
282
283 % \lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda}
284
285 % Agda では特定の関数内のみで利用できる関数を \verb+where+ 句で記述できる。
286 % スコープは \verb+where+ 句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
287 % 例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb+f+ を定義するとき、 \verb+where+ を使うとリスト~\ref{agda-where} のように書ける。
288 % これは \verb+f'+ と同様の動作をする。
289 % \verb+where+ 句は利用したい関数の末尾にインデント付きで \verb+where+ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。
290
291 % \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}
292
293 % % Stackのinterface 部分を使ってrecord の説明をする
294 % Agda のデータには C における構造体に相当するレコード型も存在する。
295 % 定義を行なう際は \verb+record+キーワードの後にレコード名、型、\verb+where+ の後に \verb+field+ キーワードを入れた後、フィールド名と型名を列挙する。
296 % 例えば x と y の二つの自然数からなるレコpード \verb+Point+ を定義するとリスト~\ref{agda-record}のようになる。
297 % レコードを構築する際は \verb+record+ キーワードの後の \verb+{}+ の内部に \verb+fieldName = value+ の形で値を列挙していく。
298 % 複数の値を列挙する際は \verb+;+ で区切る。
299
300 % \lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}
301
302 % 構築されたレコードから値を取得する際には \verb+RecordName.fieldName+ という名前の関数を適用する(リスト~\ref{agda-record-proj} 内2行目) 。
303 % なお、レコードにもパターンマッチが利用できる(リスト~\ref{agda-record-proj} 内5行目)。
304 % レコード内の値は \verb+record oldRecord {field = value ; ... }+ という構文を利用し更新することができる。
305 % Point の中の x の値を5増やす関数 \verb+xPlus5+ はリスト~\ref{agda-record-proj}の 7,8行目のように書ける。
306
307 % \lstinputlisting[label=agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}
308 337
309 \section{Agda での Stack、 Binary Tree の実装} 338 \section{Agda での Stack、 Binary Tree の実装}
310 339
311 ここでは Agda での Stack 、 Tree の実装を示す。 340 ここでは Agda での Stack 、 Binary Tree の実装を示す。
312 341
313 Stack の実装を以下のソースコード\ref{stack-impl}で示す。 342 Stack の実装を以下の Code \ref{stack-impl}で示す。
314 実装は SingleLinkedStack という名前で定義されている。 343 実装は SingleLinkedStack という名前の\verb+record+で定義されている。
315 定義されている API は一部を書き、残りは省略する。
316 344
317 \lstinputlisting[label=stack-impl, caption=Agdaにおける Stack の実装の一部] {src/AgdaStackImpl.agda} 345 \lstinputlisting[label=stack-impl, caption=Agdaにおける Stack の実装の一部] {src/AgdaStackImpl.agda}
318 346
319 Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー 347 % Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー
320 タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。 348 % タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。
321 Maybe 型では値が存在する場合は Just 、 存在しない場合は Nothing を返す。 349 % Maybe 型では値が存在する場合は Just、 存在しない場合は Nothing を返す。
322
323 SingleLinkedStack 型では、この Element の top 部分のみを定義している。 350 SingleLinkedStack 型では、この Element の top 部分のみを定義している。
324 351
325 Stack に対する push 操作では stack と push する element 型の datum を受け取り、 datum 352 Stack に対する push 操作では stack と push する element 型の datum を受け取り、 datum
326 の next に現在の top を入れ、 stack の top を受け取った datum に切り替え、新しい 353 の next に現在の top を入れ、 stack の top を受け取った datum に切り替え、新しい
327 stack を返すというような実装をしている。 354 stack を返すというような実装をしている。
328 355
329 Tree の実装(以下のソースコード\ref{tree-impl})は RedBlackTree という名前で定義されている。 356 Tree の実装(以下の Code \ref{tree-impl})は Tree という\verb+record+で定義されている。
330 定義されている API は put 以後省略する。残りのの実装は付録に示す。 %~\ 357
331 358 % \lstinputlisting[label=tree-impl, caption=Agdaにおける Tree の実装]{src/AgdaTreeImpl.agda}
332 \lstinputlisting[label=tree-impl, caption=Agdaにおける Tree の実装] {src/AgdaTreeImpl.agda} 359
333 360 \begin{lstlisting}[caption=Treeの実装,label=tree-impl]
334 Node 型は key と value 、 Color と Node の rihgt 、 left の情報を持っている。 361 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
335 Tree を構成する末端の Node は leafNode 型で定義されている。 362 field
336 363 putImpl : treeImpl -> a -> (treeImpl -> t) -> t
337 RedBlackTree 型は root の Node 情報と Tree に関する計算をする際に、そこまでの 364 getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t
338 Node の経路情報を保持するための nodeStack と 比較するための compare を持っている。 365
366 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
367 field
368 tree : treeImpl
369 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
370 putTree : a -> (Tree treeImpl -> t) -> t
371 putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
372 getTree : (Tree treeImpl -> Maybe a -> t) -> t
373 getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
374
375 record Node {n : Level } (a k : Set n) : Set n where
376 inductive
377 field
378 key : k
379 value : a
380 right : Maybe (Node a k)
381 left : Maybe (Node a k)
382 color : Color {n}
383 \end{lstlisting}
384
385 Tree を構成する Node の型は \verb+Node+型で定義され key、 value、 Color、rihgt、
386 left などの情報を持っている。
387 Tree を構成する末端の Node は \verb+leafNode+ 型で定義されている。
388
389 Tree 型の実装では root の Node 情報と Tree に関する計算をする際に、そこまでの
390 Node の経路情報を保持するための Stack を持っている。
339 391
340 Tree の put 操作では tree 、 put するノードのキーと値(k1、value)を引数として受け 392 Tree の put 操作では tree 、 put するノードのキーと値(k1、value)を引数として受け
341 取り、Tree の root に Node が存在しているかどうかで場合分けしている。 393 取り、Tree の root に Node が存在しているかどうかで場合分けしている。
342 Nothing が返ってきたときは RedBlackTree 型の tree 内に定義されている root に受け 394 Nothing が返ってきたときは RedBlackTree 型の tree 内に定義されている root に受け
343 取ったキーと値を新しいノードとして追加する。 395 取ったキーと値を新しいノードとして追加する。
347 399
348 \section{Agda における Interface の実装} 400 \section{Agda における Interface の実装}
349 401
350 Agda で GearsOS のモジュール化の仕組みである interface を実装した。 402 Agda で GearsOS のモジュール化の仕組みである interface を実装した。
351 interface とは、実装と仕様を分ける記述でここでは Stack の実装を 403 interface とは、実装と仕様を分ける記述でここでは Stack の実装を
352 SingleLinkedStack 、 Stack の仕様を Stack とする。 404 SingleLinkedStack 、 Stack の仕様を Stack とした。
353 interface は record で列挙し、ソースコード~\ref{agda-interface}のように紐付けることができる。 405 interface は record で列挙し、Code~\ref{agda-interface}のように紐付けることができる。
354 Agda では型を明記する必要があるため record 内に型を記述している。 406 Agda では型を明記する必要があるため record 内に型を記述している。
355 407
356 例として Agda で実装した Stack 上の interface (ソースコード\ref{agda-interface}) 408 例として Agda で実装した Stack 上の interface ( Code \ref{agda-interface})
357 の一部を見る。 409 の一部を見る。
358 Stack の実装は SingleLinkedStack(ソースコード\ref{agda-single-linked-stack}) として書かれている。それを Stack 側からinterface を通して呼び出している。 410 Stack の実装は SingleLinkedStack( Code \ref{agda-single-linked-stack}) として書かれている。それを Stack 側からinterface を通して呼び出している。
359 411
360 ここでの interface の型は Stack の record 内にある pushStack や popStack などで、 412 ここでの interface の型は Stack の record 内にある pushStack や popStack などで、
361 実際に使われる Stack の操作は StackMethods にある push や popである。この push 413 実際に使われる Stack の操作は StackMethods にある push や popである。この push
362 や pop は SingleLinkedStack で実装されている。 414 や pop は SingleLinkedStack で実装されている。
363 415
378 化された。 430 化された。
379 431
380 % 元の push では 送り先の stack を関数に書く必要があり、異なる stack に push 432 % 元の push では 送り先の stack を関数に書く必要があり、異なる stack に push
381 % する可能性があったが、 pushStack では紐付けた Stack に push することになり 433 % する可能性があったが、 pushStack では紐付けた Stack に push することになり
382 434
383 \section{継続を使った Agda における Test , Debug}
384 Agda ではプログラムのコンパイルが通ると型の整合性が取れていることは保証できるが、必ず
385 しも期待した動作をするとは限らない。そのため、本研究中に書いたプログラムが正しい動
386 作をしているかを確認するために行なった手法を幾つか示す。
387
388 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
389 今回は実験中にソースコード\ref{agda-stack-test}のような Test を書いた。
390 この Test では Stack をターゲットにしていて、 Stack に1、 2の二つの$ \mathbb{N} $型のデー
391 タを push した後、 pop2 Interface を使って Stack に入っている 1、 2 が Stack の
392 定義である First in Last out の通りに 2、 1 の順で取り出せるかを確認するために作成した。
393
394 %\lstinputlisting[label=agda-stack-test, caption=Agdaにおけるテスト]{src/}
395
396 上の Test では、02 が 2つのデータを push し、 03 で 二つのデータを pop する pop2
397 を行っている。それらをまとめて記述したものが 04 で 2 回 push し、 2つのデータを pop する動
398 作が正しく行われていれば 04 は True を返し、 05 で記述された型通りに互いに等しくなる
399 ため 05 が refl でコンパイルが通るようになる。
400 今回は、 pop2 で取れた値を確認するため 03 の後に 031、 032 の二つの作成した。
401 032 では 03 で扱っている値が Maybe であるため、 031 のような比較をする前に値が確
402 実に存在していることを示す補題である。 032 を通すことで 031 では 2つの値があり、
403 かつ$\mathbb{N}$型である事がわかる。 031 では直接取れた値が 2、 1 の順番で入って
404 いるかを確認している。
405
406 この Test でエラーが出なかったことから、 Stack に1、2の二つのデータを pushする
407 と、 push した値が Stack 上から消えることなく push した順番に取り出せることが分
408 かる。
409
410 また、継続を用いて記述することで関数の Test を書くことで計算途中のデータ内部をチェックするこ
411 とができた。
412
413 ここでの \$ は \( \) をまとめる糖衣構文で、 \$ が書かれた一行を\(\)でくくること
414 ができる。
415 % \ref{sintax}のようなコードを
416 % \begin{lstlisting}[frame=lrbt,label=sintax,caption={ 通常の継続の
417 % コード}]
418
419 % \end{lstlisting}
420
421 % \begin{lstlisting}[frame=lrbt,label=sintax-sugar,caption={ 糖衣構文
422 % を用いた継続のコード}]
423
424 % \end{lstlisting}
425
426 ソースコード~\ref{agda-tree-debug}のように関数本体に記述してデータを返し、C-c C-n
427 (Compute normal form) で関数を評価すると関数で扱っているデータを見ることができる。
428 また、途中の計算で受ける変数名を変更し、 Return 時にその変更した変数名に変えるこ
429 とで、計算途中のデータの中身を確認することができる。評価結果はソースコード内にコメントで記述した。
430
431 \lstinputlisting[label=agda-tree-debug, caption=Agdaにおけるテスト]{src/AgdaTreeDebug.agda}
432
433 今回、この手法を用いることで複数の関数を組み合わせた findNode 関数内に異常があるこ
434 とが分かった。
435
436
437 %getRedBlackTree の関数に
438 % \lstinputlisting[label=agda-Debug, caption=Agdaにおけるデバッグ]{src/AgdaTreeDebug.agda}
439 % Tree全然載せてないけどどうしよ。。。どこに書こうかは考えておきましょう
440
441 435
442 \section{Agda による Interface 部分を含めた Stack の部分的な証明} 436 \section{Agda による Interface 部分を含めた Stack の部分的な証明}
443 \label{agda-interface-stack} 437 \label{agda-interface-stack}
444 438
445 % Stack の仕様記述 439 % Stack の仕様記述
446 Stack や Tree の Interface を使い、 Agda で Interface を 経由した証明が可能であ 440 Stack の Interface を使い、 Agda で Interface を 経由した証明を行なった。
447 ることを示す。
448 ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。 441 ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。
449 442
450 Stack の処理として様々な性質が存在する。例えば、 443 Stack の処理として様々な性質が存在する。例えば、
451 444
452 \begin{itemize} 445 \begin{itemize}
460 などの性質がある。 453 などの性質がある。
461 454
462 ここでは「どのような状態の Stack でも、値を push した後 pop した値は直前 455 ここでは「どのような状態の Stack でも、値を push した後 pop した値は直前
463 に入れた値と一致する」という性質を証明する。 456 に入れた値と一致する」という性質を証明する。
464 457
465 まず始めに不定状態の Stack を定義する。ソースコード~\ref{agda-in-some-state} 458 まず始めに不定状態の Stack を定義する。 Code~\ref{agda-in-some-state}
466 の stackInSomeState 型は中身の分からない抽象的な Stack を表現している。ソースコー 459 の stackInSomeState 型は引数として \verb+SingleLinkedStack+ 型の \verb+s+を受け
467 ド~\ref{agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を 460 取り新しいレコードを返す関数である。
468 2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明す 461 この関数により、中身の分からない抽象的な Stack を表現している。ソースコー
469 る。 462 ド~\ref{agda-in-some-state}の証明ではこの \verb+stackInSomeState+ に対して、
470 463 \verb+push+ 操作を2回行い、 \verb+pop+を2回行なって取れたデータは push したデー
471 \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda} 464 タと同じものになることを証明している。
472 465
473 この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の2つのデー 466 この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の2つのデー
474 タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が 467 タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が
475 Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として 468 Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として
476 型に書かれている。 469 型に書かれている。
478 この関数本体で返ってくる値は$ x \equiv x1$ と $y \equiv y1$ のため record でまと 471 この関数本体で返ってくる値は$ x \equiv x1$ と $y \equiv y1$ のため record でまと
479 めて refl で推論が通る。 472 めて refl で推論が通る。
480 これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも 473 これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも
481 のを受け取れることが証明できた。 474 のを受け取れることが証明できた。
482 475
483 476 \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda}
484 % \lstinputlisting[label=agda-Test, caption=]{src/AgdaStackTest.agda} 477
485 478 しかし、同様の証明を Tree 側で記述した際、 Agda 側で等しいことを認識できず記述が
486 % \section{Agda による Interface 部分を含めた Binary Tree の部分的な証明と課題} 479 複雑になっていったため、今後の証明は Hoare Logic をベースにしたものを取り入れて
487 % ここでは Binary Tree の性質の一部に対して証明を行う。 480 行きたいと考えている。
488 % Binary Tree の性質として挙げられるのは次のようなものである
489 % % 上の2つはデータ構造として最低限守られるべき部分ではあるがとりあえず書いてる
490
491 % \begin{itemize}
492 % \item Tree に対して Node を Put することができる。
493 % \item Tree に Put された Node は Delete されるまでなくならない。
494 % \item Tree に 存在する Node とその子の関係は必ず「右の子 $>$ Node」かつ「Node $>$ 左の子」の関係になっている。
495 % \item どのような状態の Tree に値を put しても Node と子の関係は保たれる
496 % \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。
497 % \end{itemize}
498
499 % ここで証明する性質は
500
501 % ${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。
502
503 % \lstinputlisting[label=agda-tree-proof, caption=Tree Interface の証
504 % 明]{src/AgdaTreeProof.agda}
505
506 % この Tree の証明では、不定状態の Tree を redBlackInSomeState で作成し、その状態の Tree
507 % に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの
508 % である。
509
510 % しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した
511 % Node が存在するのか、などの条件や、 Get した Node と Put した Node が合同なのか、
512 % key の値が等しい場合の eq は合同と同義であるのか等の様々な補題を証明する必要が
513 % あった。今回この証明では Put した Node と Get した
514 % Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合
515 % 同であることを示すことが困難であった。
516
517 % 今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を
518 % 行おうと考えている。
519 481
520 \section{Hoare Logic} 482 \section{Hoare Logic}
521 \label{hoare-logic} 483 \label{hoare-logic}
522 484
523 Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正 485 Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正
547 \caption{cbc と hoare logic} 509 \caption{cbc と hoare logic}
548 \label{fig:cbc-hoare} 510 \label{fig:cbc-hoare}
549 \end{figure} 511 \end{figure}
550 512
551 この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると 513 この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると
552 Pre Condition は CodeGear に入力として与えられる Input DataGear として、 514 PreCondition は CodeGear に入力として与えられる Input DataGear として、
553 Command は処理の単位である CodeGear、 Post Condition を Output DataGear として当てはめることができると考える。 515 Command は処理の単位である CodeGear、 PostCondition を Output DataGear として当てはめることができると考える。
554 516
555 ここでは binary tree での findNode、 replaceNode、 getRedBlackTree の流れを図 517 ここでは binary tree での findNode、 replaceNode、 getRedBlackTree の流れを図
556 \ref{fig:tree-hoare} で示す。 518 \ref{fig:tree-hoare} で示す。
557 519
558 \begin{figure}[htpb] 520 \begin{figure}[htpb]