<!--カンペだよ-->

# タイトル

Gears Agdaにおける
Left Learning Red Black Tree の検証について

琉球大学 並列信頼研究室の上地が発表します

# 目的
そのまま読む

# CbC
もそのまま読む

# Agda
もそのまま読む

# Agda の基本
Agda の基本となる型の１つである Record 型について説明します

record Env とあるところで Env という Record 型を定義  
することを示しています

そしてその中にvarnとvariがあり、その型が自然数であることを定義しています

次に、記述する際の導入が以下のようになり
varnに0を、variに1を定義しています

導入後は変数 スペース record名でその中身にアクセスできます

# Gears Agda の記法
何と対応しているからLoopで記述するんだっけ

Agdaの構文的に禁止していないので再帰呼び出しは使用しないよう注意が必要です

以下がwhile loopのノーマルレベルでの記述になります

まず型の方で
Envを受け取り、Codeを受け取り、
tを返すといった流れになっています

このCodeはEnvを受け取った後にｔを返すというものです

次に、入力を env next で受け取っています

このcodeは後で再び説明するので、withの方はおいておいてください

パターンマッチの方で、false trueの場合をかんがえています
これはfalseの場合はnextにenvを渡します
nextはenvを受け取ってtを返すので正しいです
これがtを返すことでこの後も関数が続くこと、継続を示します


# Gears Agdaと Gears CbCの対応
そのまま読むでよさそう
Contextだけ調べた方がよいかも


# Normal levelと～
今回検証に使用するHoare Conditionと証明も Meta levelです

画像はよなおせ

# Hoare logic
コマンド が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当（correct）であるという

簡単な例としてGears Agdaにてwhile loopを検証します

以下のコードを詳細に説明します

入力と出力に関しては前述しました
このたーみねーてぃんぐはこの関数が停止することを示しています
この実装ではagdaはloopが終了するのかわからず、コンパイルできないので
このあのてーとをつけて停止することを明示します

with文は引数であたえられた値を展開します。
今回はその値をパターンマッチしています。

これがless than で0とvarnを比較しています

このwhileloopは、
varnがこれからループする回数で、variがループした回数になります

なので、これが0になると終了し次の関数であるnextに遷移し
0でないならループする回数varxから今回分の１引いて
variには今回分の1を足したものをEnvとしてもう一度関数を実行するという記述になっています

# post condition 
先ほど実装したノーマルレベルなwhile loopに対して
条件となるPre / Post Condition を追加した実装をします

そのまえにterminatingが付いていると停止性の証明をしたことにはならないので～
loopを分割した実装を行います

このconditionはループしたい回数は
これからループする回数とループした回数の和と等しいというものです


# loopの接続
loopが前のページのWhile LoopSeg だな

loopの部分の証明のみだな

# 実際のloopの接続
最終的にはループした回数が入力のループしたい回数と一致していることを
証明したいので以下のようになります

で、前回のものは最初から構造体（record）に値が格納されている状態から始まっていたので
proofGearsTermS では、入力が自然数で、recordの定義から検証を行っている

そしてそれを行っているのが最初の関数であるwhileTest'で
ここでvarnが入力c10と一致し、variが0であることを証明している

次の関数であるversionでは、whileTest'のrecord定義時のConditionから
loop時のconditionを生成しています

# testとの違い
そのまま読むよ

Condition 

# BTの実装
これはノーマルレベルの BinaryTree の find 実装になります

これが行っているのはkeyと等しいnodeを見つける

なので入力されているtreeのkeyと比較し
等しかった場合は終了

入力のkeyの方が小さい場合は
左のtreeを次のfindの対象とし
今回対象のtreeをstackに積む

# replace tree

先ほどと同じように入力のkeyと比較し
今度は木を再構成するので

# Invariant
Binary Treeの証明には３つのInvariant（不変条件）をもちいる
あとはそのまま読む

# find hoare condition

最初のtreeInvariant tree ∧ stackInvariantが
pre conditionで、
treeInvariant と stackInvariantを満たしていることを証明する

nextには次のInvariant と現在の木の深さが最大ではないことを示しています

exitなのでfindを終了する際には
valueを見つけられなかったことを表す
tree1がleefか

valueを見つけたことを表す
tree1のkeyが入力のkeyといっちしていることを表します

# カンペ
synchronized queue
- 読めない間は待っている
concurrent tree
-