|
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 # 証明を用いたプログラムの信頼性の向上を目指す
|
|
|
41
|
|
|
42
|
|
|
43
|
|
|
44 ---
|
|
|
45
|
|
|
46 # これまでの成果
|
|
|
47
|
|
|
48 - Gears Agda
|
|
|
49 - Gears Agda による Hoare Logic を用いた簡単なプログラムの検証
|
|
|
50 - Gears Agda で実装したRed Black Tree
|
|
|
51
|
|
|
52 ---
|
|
|
53 # 今回の成果
|
|
|
54
|
|
|
55 - Left Lerning Red Black Tree の実装
|
|
|
56 - (delete) 誰もやろうとしていなかった
|
|
|
57 - 証明付き Data 構造を用いた List による性質の記述
|
|
|
58
|
|
|
59 ---
|
|
|
60 # Agdaの紹介
|
|
|
61
|
|
|
62 ---
|
|
|
63 # gears Agda
|
|
|
64
|
|
|
65 ---
|
|
|
66 # llrbt
|
|
|
67
|
|
|
68 ---
|
|
|
69 # delete
|
|
|
70
|
|
|
71 ---
|
|
|
72 # Left Lerning Red Black Tree の実装
|
|
|
73
|
|
|
74 ---
|
