---
marp: true
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 -->
# Gears Agda による <br> 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 による性質の記述

---
# Left Learning Red Black Tree
- Red Black Tree の定義を満たしつつ、実装が用意な Binary Treeの一つ
- 定義は以下である。
  - 各点は赤か黒の色である。
  - 点が赤である場合の親となる点の色は黒である。
  - 外点 (葉。つまり一番下の点) は黒である。
  - 任意の点から外点までの黒色の点はいずれも同数となる。
  - node は parent から見て左の node にしか 現れない

---
# Left Learning Red Black Tree の一例

![height:500](images/llrbt.svg)

---
# Gears Agda による Left Leaning Red Black Tree の記述
- 通常のプログラミング言語であれば、再代入と再起処理を用いて実装を行う
- Gears Agda では両方行えないため、これらを回避する
- insert / delete をする際に、目的の node まで辿るが、ここで辿った分を
Listに保持する
- 目的の node まで辿った後に、List に保持した node を結合させることで実装を行う
<!-- 今までdeleteの話ができる。 -->

---
# 実際の Left Leaning Red Black Tree の実装コード

```
insert-c : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
insert-c env next exit with Env.vart env
... | bt-empty = exit record env{vart = (bt-node (record { 
  key = record { coler = red ; number = Env.varn env };
  ltree = bt-empty; rtree = bt-empty }))}
... | bt-node node with <-cmp (Env.varn env) (node.number (tree.key node))
... | tri≈ ¬a b ¬c = exit env
... | tri> ¬a ¬b c = next record env{
  vart = (tree.ltree node) ; 
  varl = (bt-node record node{ltree = bt-empty}) ∷ (Env.varl env) }
... | tri< a ¬b ¬c = next record env{
  vart = (tree.rtree node) ; 
  varl = (bt-node record node{rtree = bt-empty}) ∷ (Env.varl env) }
```

---
# 証明付き Data 構造を用いた List による性質の記述
- 検証には実装が仕様を満たしている必要がある
- Binary Tree の性質も持っているので、大小関係を検証する
- そこで、証明付き Data 構造を用いた List を下記のように定義した
```
data  right-List : Set where
  [] : right-List
  [_] : ℕ → right-List
  _∷>_Cond_ : (x : ℕ) → (xs : right-List ) → (p : x Data.Nat.> top-r xs) → right-List
```

---
# 今後の課題

- 作成した Left Learning Red Black Tree を Hoare Logicに当てはめる
- その後、条件の接続ができているのかと、健全性について示す
- CbCはC言語とアセンブラの中間言語に位置しており、人が書くのは困難である
  - そのため、Gears Agda から CbC へ変換ができないか調査する

---
# まとめ

- Left Learning Red Black Tree について記述した
- Meta Data Gear を記述した
  - 証明付き Data 構造を用いた List による性質の記述
- 今後検証に向けて、条件の接続と、健全性について示す