Mercurial > hg > Papers > 2021 > soto-thesis

comparison slide/slide.md @ 12:68485f45c265

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ADD slide
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Mon, 15 Feb 2021 05:13:01 +0900
parents e5248199c73d
children 4361e7b7d3db
comparison
equal deleted inserted replaced
11:1cde48f23236 12:68485f45c265
36 - 琉球大学工学部 36 - 琉球大学工学部
37 37
38 --- 38 ---
39 <!-- class: slide --> 39 <!-- class: slide -->
40 # 証明を用いたプログラムの信頼性の向上を目指す 40 # 証明を用いたプログラムの信頼性の向上を目指す
41 41 <!-- 研究目的 -->
42 - プログラムの信頼性を高めることは重要な課題である
43 - 信頼性を高める手法として「モデル検査」や「定理証明」など
44 - 当研究室でCbCという言語を開発している
45 - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
46 - 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った。
47 - 本研究では Gears Agda にて 重要なアルゴリズムの一つである Red Black Tree を検証する
42 48
43 49
44 --- 50 ---
45 51
46 # これまでの成果 52 # これまでの成果
47 53
48 - Gears Agda 54 - Gears Agda
49 - Gears Agda による Hoare Logic を用いた簡単なプログラムの検証 55 - Gears Agda による Hoare Logic を用いた簡単なプログラムの検証
50 - Gears Agda で実装したRed Black Tree 56 - Gears Agda で実装したRed Black Tree(insert)
51 57
52 --- 58 ---
53 # 今回の成果 59 # 今回の成果
54 60
55 - Left Lerning Red Black Tree の実装 61 - Left Lerning Red Black Tree の実装
56 - (delete) 誰もやろうとしていなかった
57 - 証明付き Data 構造を用いた List による性質の記述 62 - 証明付き Data 構造を用いた List による性質の記述
58 63
59 --- 64 ---
60 # Agdaの紹介 65 # Agdaの紹介
61 66
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 ```
62 --- 74 ---
63 # gears Agda 75 # Gears Agda
76 - CbC 実行を継続すると言う仕様に合わせた Agda の記法
77 - Env を Data Gear としている
78 - Env → t を用いる事で次の遷移先を示す
79
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 ```
86 ---
87 # Left Learning Red Black Tree
88 - Red Black Tree の定義を満たしつつ、実装が用意な Binary Treeの一つ
89 - 定義は以下である。
90 <!-- 箇条書きで定義を載せる画像を載っける -->
91
64 92
65 --- 93 ---
66 # llrbt 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 - その後、条件の接続ができているのかと、健全性について示す。
67 111
68 --- 112 ---
69 # delete 113 # まとめ
70 114
71 --- 115 - Left Learning Red Black Tree について記述した
72 # Left Lerning Red Black Tree の実装 116 - Meta Data Gear を記述した
73 117 - 証明付き Data 構造を用いた List による性質の記述
74 --- 118 - 今後検証に向けて、条件の接続ができているのかと、健全性について示す。