# 研究目的

- OSやアプリケーションの信頼性を高めることは重要な課題である。

- 研究室でCbCという言語を開発している。その信頼性を証明したい。

- CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。

- プログラムの正当性を証明するためにHoare Logicという検証手法がある。これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というものである。

- CbC では実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。それを繋げていくため、個々の関数の正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。

- これらのことから、Hoare Logicを用いてCbCを検証できるか実験していく。

- cbcはサブルーチンとスープ制御をcから取り除いている。その為、それを実装した際のプログラムを検証をする必要がある。

- 先行研究ではCbCにおけるWhileLoopの検証を行なった。

- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う

## 今週の進捗
- continuationなLLRB-Treeのinsertを若干修正
    - あまりよろしく無い実装をしていたのでそれを修正
    - ループ部分のterminationは外せなさそう(外す際にその部分で実装を行わないといけなくなり、意味が変わってくる)

- nextとexitに投げるものに着いて悩んでいる

- 水を購入

- ダージリンを設置

### 修正部分

```Agda
skew' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
skew' env exit = skew-bt env (λ env → merge-rotate-left env exit exit ) exit

split' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
split' env exit = split-branch env (λ env → merge-rotate-right env (λ env → split env exit exit ) (λ env → split env exit exit ) ) exit

{-# TERMINATING #-}
mergeP : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
mergeP env exit = merge-tree env (λ env → skew' env (λ env → split' env (λ env → mergeP env exit)) ) exit

whileTestPCall' : (tree : rbt) → (n : ℕ)  → Env
whileTestPCall' tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → mergeP env (λ env → init-col env (λ env → env ) ) ) )
```

- skewとsplitの動作をまとめた
- skew,split関数はループしないのでterminationを落とした

### nextとexitの話

``` Agda
-- 左回転、exitはsplit_branchへ　nextもsplit_branchへ
merge-rotate-left : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
merge-rotate-left node@record { vart = bt-empty ; varn = varn ; varl = varl }  next exit = exit node
merge-rotate-left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node
merge-rotate-left record { vart = bt-node record { key = record { coler = y ; number = x } ; ltree = l ; rtree = (bt-node record { key = record { coler = ry ; number = rx } ; ltree = rl ; rtree = rr }) } ; varn = varn ; varl = varl } next exit
  = next record { vart = bt-node record { key = record { coler = y ; number = rx }
  　　; ltree = (bt-node record { key = record { coler = red ; number = x } ; ltree = l ; rtree = rl })
  　　; rtree = rr}
  　　; varn = varn ; varl = varl }
```

本来は動かない部分をexitとしている。この部分をどうしようか考えている。
- 全てnext/exitのどちらかに統一する方法
- exitに例外処理を渡す
- 現在はexitに、nextと同じ遷移先を示している。


## 余談
- air podsを買った
    - コスパはあまりよくなさそうですが、apple製品との連携が良い
- Agdaのコードを一切ハイライトしてくれなかった…