Binary file paper/final_thesis.pdf has changed

--- a/paper/tex/future.tex	Mon Feb 15 03:51:35 2021 +0900
+++ b/paper/tex/future.tex	Mon Feb 15 05:13:01 2021 +0900
@@ -18,7 +18,7 @@
 
 展望としては、Gears Agda コードから CbC コードの変換をしたい。
 Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが、
-CbC はC言語の下位言語であり、
+CbC はC言語とアセンブラの中間に位置しているため、コーディングはさらに困難である。
+そのため、Gears Agdaのコードを CbC に変換できるようにしたい。
+これができるようになれば、CbC での記述も Agda での証明も容易になると考えている。
 
-
-

--- a/slide/slide.md	Mon Feb 15 03:51:35 2021 +0900
+++ b/slide/slide.md	Mon Feb 15 05:13:01 2021 +0900
@@ -38,7 +38,13 @@
 ---
 <!-- class: slide -->
 # 証明を用いたプログラムの信頼性の向上を目指す
-
+<!-- 研究目的 -->
+- プログラムの信頼性を高めることは重要な課題である
+  - 信頼性を高める手法として「モデル検査」や「定理証明」など
+- 当研究室でCbCという言語を開発している
+  - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
+- 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った。
+- 本研究では Gears Agda にて 重要なアルゴリズムの一つである Red Black Tree を検証する
 
 
 ---
@@ -47,28 +53,66 @@
 
 - Gears Agda
 - Gears Agda による Hoare Logic を用いた簡単なプログラムの検証
-- Gears Agda で実装したRed Black Tree
+- Gears Agda で実装したRed Black Tree(insert)
 
 ---
 # 今回の成果 
 
 - Left Lerning Red Black Tree の実装
-- (delete) 誰もやろうとしていなかった
 - 証明付き Data 構造を用いた List による性質の記述
 
 --- 
 # Agdaの紹介
 
+- Agdaとは、定理証明支援器であり、関数型言語である
+- 特徴として、変数への再代入が許されていない事や、型を明示する必要がある
+```Agda
+plus : (x y : N ) → N
+plus x zero = x
+plus x (suc y) = plus (suc x) y
+```
 ---
-# gears Agda
+# Gears Agda
+- CbC 実行を継続すると言う仕様に合わせた Agda の記法
+- Env を Data Gear としている
+- Env → t を用いる事で次の遷移先を示す
 
+```Agda
+plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
+plus-com env next exit with vary env
+... | zero  = exit (record { varx = varx env ; vary = vary env })
+... | suc y = next (record { varx = suc (varx env) ; vary = y })
+```
 ---
-# llrbt
+# Left Learning Red Black Tree
+- Red Black Tree の定義を満たしつつ、実装が用意な Binary Treeの一つ
+- 定義は以下である。
+<!-- 箇条書きで定義を載せる画像を載っける -->
+
 
 ---
-# delete
+# Left Leaning Red Black Tree の実装
+- 通常のプログラミング言語であれば、再代入と再起処理を用いて実装を行う
+- Gears Agda では両方行えないため、これらを回避する
+- insert / delete をする際に、目的の node まで辿るが、ここで辿った分を
+Listに保持する
+- 目的の node まで辿った後に、List に保持した node を結合させることで実装を行う
+<!-- deleteの話ができる。 -->
+---
+# 証明付き Data 構造を用いた List による性質の記述
+- Binary Tree の性質も持っているので、大小関係を検証する必要がある
+- そこで、証明付き Data 構造を用いた List を下記のように定義した
+<!-- 定義を載せる -->
+---
+# 今後の課題
+
+- 作成した Left Learning Red Black Tree を Hoare Logicに当てはめる
+- その後、条件の接続ができているのかと、健全性について示す。
 
 ---
-# Left Lerning Red Black Tree の実装
+# まとめ
 
----
+- Left Learning Red Black Tree について記述した
+- Meta Data Gear を記述した
+  - 証明付き Data 構造を用いた List による性質の記述
+- 今後検証に向けて、条件の接続ができているのかと、健全性について示す。