---
marp: false
title: Geas Agda による Left Learning Red Black Tree の検証
paginate: true

theme: default
size: 16:9
style: |
  section {
    background-color: #FFFFFF;
    font-size: 28px;
    color: #4b4b4b;
    font-family: "Arial", "Hiragino Maru Gothic ProN";
  }

  section.title {
    font-size: 40px;
    padding: 40px;
  }
  section.title h1 {
    text-align: center;
  }

  section.slide h1 {
    position: absolute;
    left: 50px; top: 35px;
  }

---
<!-- class: title -->
# Geas Agda による Left Learning Red Black Tree の検証

- 上地 悠斗 
    - 琉球大学工学部工学科知能情報コース
- 河野 真治
    - 琉球大学工学部

---
<!-- class: slide -->
# 証明を用いたプログラムの信頼性の向上を目指す
<!-- 研究目的 -->
- プログラムの信頼性を高めることは重要な課題である
  - 信頼性を高める手法として「モデル検査」や「定理証明」など
- 当研究室でCbCという言語を開発している
  - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
- 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った。
- 本研究では Gears Agda にて 重要なアルゴリズムの一つである Red Black Tree を検証する


---

# これまでの成果

- Gears Agda
- Gears Agda による Hoare Logic を用いた簡単なプログラムの検証
- Gears Agda で実装したRed Black Tree(insert)

---
# 今回の成果 

- Left Lerning Red Black Tree の実装
- 証明付き Data 構造を用いた List による性質の記述

--- 
# Agdaの紹介

- Agdaとは、定理証明支援器であり、関数型言語である
- 特徴として、変数への再代入が許されていない事や、型を明示する必要がある
```Agda
plus : (x y : N ) → N
plus x zero = x
plus x (suc y) = plus (suc x) y
```
---
# 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 })
```
---
# Left Learning Red Black Tree
- Red Black Tree の定義を満たしつつ、実装が用意な Binary Treeの一つ
- 定義は以下である。
<!-- 箇条書きで定義を載せる画像を載っける -->


---
# 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 Learning Red Black Tree について記述した
- Meta Data Gear を記述した
  - 証明付き Data 構造を用いた List による性質の記述
- 今後検証に向けて、条件の接続ができているのかと、健全性について示す。