---
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: "Droid Sans Mono", "Hiragino Maru Gothic ProN";
    background-image: url("logo.svg");
    background-position: right 3% bottom 2%;
    background-repeat: no-repeat;
    background-attachment: 5%;
    background-size: 20% auto;
  }
  
    section.title h1 {
      color: #808db5;
      text-align: center;
      }
    
    section.title p {
        bottom: 25%;
        width: 100%;
        position: absolute;
        font-size: 25px;
        color: #4b4b4b;
        background: linear-gradient(transparent 90%, #ffcc00 0%);
    }

  section.slide h1 {
      width: 95%;
      color: white;
      background-color: #808db5;
      position: absolute;
      left: 50px; 
      top: 35px;
  }

---
<!-- headingDivider: 1 -->

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

Uechi Yuto, Shinji Kono 琉球大学

# 証明を用いてプログラムの信頼性の向上を目指す
<!-- class: slide -->

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

# CbC について
- CbCとは当研究室で開発しているC言語の下位言語
    - CbC とは C 言語からループ制御構造とサブルーチンコールを取り除き、継続を導入したC 言語の下位言語
    - 継続呼び出しは引数付き goto 文で表現される。
    - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
- CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。

# Gears Agda の記法
このこーどで使用しているAgdaの構文は解説が必要
- Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない
    - 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 })
```

- → t で Set に遷移させるようにし, この後に関数が続くことと関数を tail call していることで Continuation を定義している

# Hoare Logic について
- Hoare Logic とは C.A.R Hoare、R.W Floyd が考案したプログラムの検証の手法
- 「プログラムの事前条件 (P) が成立しているとき、コマンド (C) 実行して停止
すると事後条件 (Q) が成り立つ」というもの
    - CbC の実行を継続するという性質に非常に相性が良い

pre/post conditionの

# Gears Agda による検証の例（一部）
plus

# Binary Tree について
<!-- たぶん聴講者はわかると思うのでかるくで良い -->

# Gears Agda による Binary Tree の実装
Agda が再代入を許していないことから
stackを用いてエスケープしている説明が必要

# Gears Agda による Binary Tree の検証

# これで検証を行えているのかの説明
Hoare Logic で
Hoare Condition が接続されていること

不変条件なににするか
BTの不変条件３つを説明



# 今後の研究方針
- 現在は Binary Tree の検証までしか行えていないが、
今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
- 今後は Gears Agda による実装と条件の追加をおこなう
- モデル検査のこと、CbC変換のことも話してもよい

# まとめ
- Gears Agda にて Binary Tree を検証することができた
  - Gears Agda における Termination を使用しない実装の仕方を確率した
  - Hoare Logic による検証もできるようになった
  - 今後は Red Black Tree の検証をすすめる
- モデル検査をしたい

英語版も欲しい

condition を テンプレみたいに作ってかきやすくする話