Mercurial > hg > Papers > 2018 > ryokka-sigos
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] |