|
9
|
1 ---
|
|
|
2 marp: false
|
|
|
3 title: Geas Agda による Left Learning Red Black Tree の検証
|
|
|
4 paginate: true
|
|
|
5
|
|
|
6 theme: default
|
|
|
7 size: 16:9
|
|
|
8 style: |
|
|
|
9 section {
|
|
|
10 background-color: #FFFFFF;
|
|
|
11 font-size: 28px;
|
|
|
12 color: #4b4b4b;
|
|
|
13 font-family: "Arial", "Hiragino Maru Gothic ProN";
|
|
|
14 }
|
|
|
15
|
|
|
16 section.title {
|
|
|
17 font-size: 40px;
|
|
|
18 padding: 40px;
|
|
|
19 }
|
|
|
20 section.title h1 {
|
|
|
21 text-align: center;
|
|
|
22 }
|
|
|
23
|
|
|
24 section.slide h1 {
|
|
|
25 position: absolute;
|
|
|
26 left: 50px; top: 35px;
|
|
|
27 }
|
|
|
28
|
|
|
29 ---
|
|
|
30 <!-- class: title -->
|
|
|
31 # Geas Agda による Left Learning Red Black Tree の検証
|
|
|
32
|
|
|
33 - 上地 悠斗
|
|
|
34 - 琉球大学工学部工学科知能情報コース
|
|
|
35 - 河野 真治
|
|
|
36 - 琉球大学工学部
|
|
|
37
|
|
|
38 ---
|
|
|
39 <!-- class: slide -->
|
|
|
40 # 証明を用いたプログラムの信頼性の向上を目指す
|
|
12
|
41 <!-- 研究目的 -->
|
|
|
42 - プログラムの信頼性を高めることは重要な課題である
|
|
|
43 - 信頼性を高める手法として「モデル検査」や「定理証明」など
|
|
|
44 - 当研究室でCbCという言語を開発している
|
|
|
45 - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
|
|
|
46 - 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った。
|
|
|
47 - 本研究では Gears Agda にて 重要なアルゴリズムの一つである Red Black Tree を検証する
|
|
9
|
48
|
|
|
49
|
|
|
50 ---
|
|
|
51
|
|
|
52 # これまでの成果
|
|
|
53
|
|
|
54 - Gears Agda
|
|
|
55 - Gears Agda による Hoare Logic を用いた簡単なプログラムの検証
|
|
12
|
56 - Gears Agda で実装したRed Black Tree(insert)
|
|
9
|
57
|
|
|
58 ---
|
|
|
59 # 今回の成果
|
|
|
60
|
|
|
61 - Left Lerning Red Black Tree の実装
|
|
|
62 - 証明付き Data 構造を用いた List による性質の記述
|
|
|
63
|
|
|
64 ---
|
|
|
65 # Agdaの紹介
|
|
|
66
|
|
12
|
67 - Agdaとは、定理証明支援器であり、関数型言語である
|
|
|
68 - 特徴として、変数への再代入が許されていない事や、型を明示する必要がある
|
|
|
69 ```Agda
|
|
|
70 plus : (x y : N ) → N
|
|
|
71 plus x zero = x
|
|
|
72 plus x (suc y) = plus (suc x) y
|
|
|
73 ```
|
|
9
|
74 ---
|
|
12
|
75 # Gears Agda
|
|
|
76 - CbC 実行を継続すると言う仕様に合わせた Agda の記法
|
|
|
77 - Env を Data Gear としている
|
|
|
78 - Env → t を用いる事で次の遷移先を示す
|
|
9
|
79
|
|
12
|
80 ```Agda
|
|
|
81 plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
|
82 plus-com env next exit with vary env
|
|
|
83 ... | zero = exit (record { varx = varx env ; vary = vary env })
|
|
|
84 ... | suc y = next (record { varx = suc (varx env) ; vary = y })
|
|
|
85 ```
|
|
9
|
86 ---
|
|
12
|
87 # Left Learning Red Black Tree
|
|
|
88 - Red Black Tree の定義を満たしつつ、実装が用意な Binary Treeの一つ
|
|
|
89 - 定義は以下である。
|
|
|
90 <!-- 箇条書きで定義を載せる画像を載っける -->
|
|
|
91
|
|
9
|
92
|
|
|
93 ---
|
|
12
|
94 # Left Leaning Red Black Tree の実装
|
|
|
95 - 通常のプログラミング言語であれば、再代入と再起処理を用いて実装を行う
|
|
|
96 - Gears Agda では両方行えないため、これらを回避する
|
|
|
97 - insert / delete をする際に、目的の node まで辿るが、ここで辿った分を
|
|
|
98 Listに保持する
|
|
|
99 - 目的の node まで辿った後に、List に保持した node を結合させることで実装を行う
|
|
|
100 <!-- deleteの話ができる。 -->
|
|
|
101 ---
|
|
|
102 # 証明付き Data 構造を用いた List による性質の記述
|
|
|
103 - Binary Tree の性質も持っているので、大小関係を検証する必要がある
|
|
|
104 - そこで、証明付き Data 構造を用いた List を下記のように定義した
|
|
|
105 <!-- 定義を載せる -->
|
|
|
106 ---
|
|
|
107 # 今後の課題
|
|
|
108
|
|
|
109 - 作成した Left Learning Red Black Tree を Hoare Logicに当てはめる
|
|
|
110 - その後、条件の接続ができているのかと、健全性について示す。
|
|
9
|
111
|
|
|
112 ---
|
|
12
|
113 # まとめ
|
|
9
|
114
|
|
12
|
115 - Left Learning Red Black Tree について記述した
|
|
|
116 - Meta Data Gear を記述した
|
|
|
117 - 証明付き Data 構造を用いた List による性質の記述
|
|
|
118 - 今後検証に向けて、条件の接続ができているのかと、健全性について示す。
|
