Mercurial > hg > Papers > 2021 > soto-thesis

changeset 13:4361e7b7d3db

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
WIP
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Mon, 15 Feb 2021 21:42:10 +0900
parents 68485f45c265
children a63df15c9afc
files paper/pic/imple.pdf paper/pic/imple/実装.pdf paper/src/agda/rbt_t.agda paper/tex/intro.tex paper/tex/rbt_verif.tex prepaper/pic/imple.pdf prepaper/pic/llrbt.pdf prepaper/pre.pdf prepaper/pre.tex prepaper/src/agda/rbt_t.agda prepaper/src/agda/rbt_varif.agda prepaper/tex/abstract.tex prepaper/tex/agda.tex prepaper/tex/cbc.tex prepaper/tex/gearsagda.tex prepaper/tex/imple.tex prepaper/tex/intro.tex prepaper/tex/rbtree.tex prepaper/tex/varif.tex slide/images/llrbt.svg slide/slide.md
diffstat 21 files changed, 539 insertions(+), 110 deletions(-) [+]
line wrap: on
line diff
Binary file paper/pic/imple.pdf has changed
Binary file paper/pic/imple/実装.pdf has changed
--- a/paper/src/agda/rbt_t.agda	Mon Feb 15 05:13:01 2021 +0900
+++ b/paper/src/agda/rbt_t.agda	Mon Feb 15 21:42:10 2021 +0900
@@ -268,7 +268,6 @@
 whileTestPCall' : (tree : rbt) → (n : ℕ)  → Env
 whileTestPCall' tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → mergeP env (λ env → init-col env (λ env → env ) ) ) )
 
-
 -- 以下test部分
 test1 = whileTestPCall' bt-empty 8
 test2 = whileTestPCall' (vart test1) 10
--- a/paper/tex/intro.tex	Mon Feb 15 05:13:01 2021 +0900
+++ b/paper/tex/intro.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -51,5 +51,3 @@
 \end{comment}
 
 
-
-
--- a/paper/tex/rbt_verif.tex	Mon Feb 15 05:13:01 2021 +0900
+++ b/paper/tex/rbt_verif.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -48,7 +48,6 @@
 
 
 
-
 以上を用いて Meta Data Gear を作成する Gears Agda は以下になる。
 
 
Binary file prepaper/pic/imple.pdf has changed
Binary file prepaper/pic/llrbt.pdf has changed
Binary file prepaper/pre.pdf has changed
--- a/prepaper/pre.tex	Mon Feb 15 05:13:01 2021 +0900
+++ b/prepaper/pre.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -9,6 +9,7 @@
 \rhead{}
 \cfoot{}
 
+
 \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
 \setlength{\headheight}{0mm}
 \setlength{\headsep}{5mm}
@@ -53,6 +54,7 @@
 \usepackage{indentfirst}
 \usepackage{url}
 \usepackage{amssymb}
+\usepackage{comment}
 
 \usepackage[backend=biber, style=numeric, bibstyle=ieee]{biblatex}
 \nocite{*}
@@ -64,9 +66,12 @@
 \newcommand\figref[1]{図 \ref{#1}}
 \newcommand\coderef[1]{ソースコード \ref{#1}}
 
+\renewcommand{\figurename}{図}
+
 \begin{document}
 \ltjsetparameter{jacharrange={-3}}
-\title{\LARGE Continuation based C による RedBlackTree の Hoare Logic を用いた検証 \\ \Large Verification of red-black tree implemented in Continuation based C using Hoare Logic}
+\title{Gears Agda による Left Learning Red Black Tree の検証 \\ \Large
+  Verification of Left-Learning Red-Black Tree using Gears Agda}
 \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
 \date{}
 \maketitle
@@ -80,11 +85,15 @@
     \input{tex/intro.tex} % 研究目的
     \input{tex/cbc.tex} % CbC の説明
     \input{tex/agda.tex} % agda の説明　levelの説明
-    \input{tex/continuation_agda.tex} % continuation agdaの説明
-    \input{tex/hoare.tex} % Hoare Logic の説明
+    %\input{tex/gearsagda.tex}
+
+    % \input{tex/cbc_agda.tex} % continuation agdaの説明
+    % \input{tex/hoare.tex} % Hoare Logic の説明
     % Hoare Logicでの検証方法
     \input{tex/rbtree.tex} % 赤黒木の説明
-    \input{tex/spec.tex}% 手法
+    \input{tex/imple.tex}
+    \input{tex/varif.tex}
+    %\input{tex/spec.tex}% 手法
     % btの実装
     % btの検証
     % rbtの実装
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/src/agda/rbt_t.agda	Mon Feb 15 21:42:10 2021 +0900
@@ -0,0 +1,283 @@
+module rbt_t where
+
+open import Data.Nat hiding (compare)
+open import Data.Nat.Properties as NatProp -- <-cmp
+open import Relation.Binary
+open import Data.List
+
+-- → t を適用するために必要だった
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Level
+
+
+data col : Set where
+  black : col
+  red : col
+
+record node (A B : Set) : Set where
+  field
+    coler : A
+    number : B
+open node
+
+record tree (A B C : Set) : Set where
+  field
+    key : A
+    ltree : B
+    rtree : C
+open tree
+
+data rbt : Set where
+  bt-empty : rbt
+  bt-node  : (node : tree (node col ℕ) rbt rbt ) → rbt
+
+record Env : Set (succ Zero) where
+  field
+    vart : rbt
+    varn : ℕ
+    varl : List rbt
+open Env
+
+
+whileTest-next : {l : Level} {t : Set l}  → (c10 : rbt) → (n : ℕ) → (list : List rbt) → (next : Env → t) → (exit : Env → t) → t
+whileTest-next c10 n list next exit = next (record {vart = c10 ; varn = n ; varl = list} )
+
+merge-tree :  {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+
+-- 全てmerge-treeへ
+split : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+split node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+split node@record { vart = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ; varn = varn ; varl = varl } next exit = exit node
+split node@record { vart = (bt-node record { key = key ; ltree = (bt-node node₁) ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node
+split record { vart = (bt-node record { key = record { coler = coler₁ ; number = number₁ }
+  ; ltree = (bt-node record { key = record { coler = ly ; number = ln } ; ltree = ll ; rtree = lr })
+  ; rtree = (bt-node record { key = record { coler = ry ; number = rn } ; ltree = rl ; rtree = rr }) })
+  ; varn = varn ; varl = varl } next exit
+  = next record { vart = (bt-node record { key = record { coler = red ; number = number₁ }
+    ; ltree = (bt-node record { key = record { coler = black ; number = ln } ; ltree = ll ; rtree = lr })
+    ; rtree = (bt-node record { key = record { coler = black ; number = rn } ; ltree = rl ; rtree = rr }) })
+    ; varn = varn ; varl = varl }
+
+
+-- 右回転
+-- 実行時splitへ、それ以外はmerge-treeへ
+merge-rotate-right : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+merge-rotate-right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate-right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate-right record { vart = bt-node record { key = record { coler = y ; number = x }
+  ; ltree = (bt-node record { key =  record { coler = ly ; number = lx } ; ltree = ll ; rtree = lr })
+  ; rtree = r }
+  ; varn = varn ; varl = varl } next exit
+    = next record { vart = bt-node record { key = record { coler = y ; number = lx }
+      ; ltree = ll
+      ; rtree = (bt-node record { key = record { coler = red ; number = x } ; ltree = lr; rtree = r }) }
+      ; varn = varn ; varl = varl }
+
+
+-- split
+split-branch : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+split-branch node@record{ vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key ; ltree = bt-empty ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = lc ; number = number } ; ltree = bt-empty ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = (bt-node node₁) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = red ; number = number₁ } ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree₁ }) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key₁
+  ; ltree = (bt-node record { key = record { coler = red ; number = number₁ }
+    ; ltree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree₁ })
+    ; rtree = lr })
+  ; rtree = rtree }
+  ; varn = varn ; varl = varl } next exit
+  = next node
+
+
+-- 左回転、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 }
+
+
+-- skew exitがsplitへ　nextが左回転
+skew-bt : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+skew-bt node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit =  exit node
+skew-bt node@record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node
+skew-bt node@record { vart = (bt-node record { key = key₁
+  ; ltree = ltree₁
+  ; rtree = (bt-node record { key = record { coler = black ; number = number }
+  ; ltree = ltree ; rtree = rtree }) }) ; varn = varn ; varl = varl } next exit
+    = exit node
+skew-bt node@record { vart = (bt-node record { key = key₁
+  ; ltree = ltree₁
+  ; rtree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree }) })
+  ; varn = varn ; varl = varl } next exit
+    = next node
+
+
+set-node-coler : Env → Env
+set-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } = node
+set-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
+  = record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
+
+init-node-coler : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+init-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+init-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit
+  = exit record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
+
+--修正前
+merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit node
+merge-tree node@record { vart = vart ; varn = varn ; varl = (bt-empty ∷ varl₁) } next exit = exit node
+
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit with <-cmp varn number
+
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri≈ ¬a b ¬c
+  = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = number ; varl = varl₁ }
+
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri> ¬a ¬b c
+  = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = vart }) ; varn = number ; varl = varl₁ }
+
+merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri< a ¬b ¬c
+  = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl₁ }
+
+-- do marge-tree
+-- next merge-tree-c
+-- exit fin
+merge-tree-c :  {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+merge-tree-c env next exit with varl env
+... | [] = exit env
+... | bt-empty ∷ nl = exit env
+... | bt-node xtree ∷ varl with <-cmp (varn env) (number ( key xtree ))
+... | tri≈ ¬a b ¬c = next (record env { vart = bt-node xtree ; varn = number (key xtree) ; varl = varl })
+... | tri> ¬a ¬b c = next (record env { vart = (bt-node record xtree{rtree = Env.vart env}) ; varn = number (key xtree) ; varl = varl })
+... | tri< a ¬b ¬c = next (record env { vart = (bt-node record xtree{ltree = Env.vart env}) ; varn = number (key xtree) ; varl = varl })
+
+-- do brandh
+-- next insert-c
+-- exit merge-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) }
+
+-- insert
+bt-insert : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+-- mergeへ遷移する
+bt-insert (record { vart = bt-empty ; varn = varn ; varl = varl }) next exit
+  = exit (record { vart = (bt-node (record { key = record { coler = red ; number = varn }; ltree = bt-empty; rtree = bt-empty })) ; varn = varn ; varl = varl })
+
+-- 場合分けを行う
+bt-insert record {vart = (bt-node record { key = record { coler = y; number = x } ; ltree = ltree ; rtree = rtree }) ; varn = n ; varl = varl } next exit with <-cmp x n
+bt-insert node@(record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } ) next exit | tri≈ ¬a b ¬c
+  = exit node
+
+bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri> ¬a ¬b c
+  = next (record {vart = ltree ; varn = varn ; varl = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ∷ varl })
+
+bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a ¬b ¬c
+  = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ∷ varl })
+
+-- normal loop without termination
+{-# TERMINATING #-}
+insert : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+insert env exit = bt-insert env (λ env → insert env exit ) exit
+
+init-col : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+init-col env exit = init-node-coler env exit exit
+
+{-
+{-# TERMINATING #-}
+merge : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+
+{-# TERMINATING #-}
+split-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+split-p env exit = split env (λ env → merge env (λ env → merge env exit ) ) exit
+
+{-# TERMINATING #-}
+rotate_right : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+rotate_right env exit = merge-rotate-right env (λ env → split-p env (λ env → merge env exit ) ) exit
+
+{-# TERMINATING #-}
+split-b : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+split-b env exit = split-branch env (λ env → rotate_right env exit ) λ env → merge env exit
+
+{-# TERMINATING #-}
+rotate_left : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+rotate_left env exit = merge-rotate-left env (λ env → split-b env exit ) exit
+
+{-# TERMINATING #-}
+skew : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+skew env exit = skew-bt env (λ env → rotate_left env (λ env → split-b env exit ) ) exit
+
+merge env exit = merge-tree env (λ env → skew env exit ) exit
+-}
+-- skewはnextがrotate-right。exitはsplitとなる
+-- skewの中にrotate-rightが内包され、実行後は必ずsplitに遷移する
+-- それはskewのexitと等しいので同時に記述してやる。
+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
+
+
+{-
+merge' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+merge' node@record { vart = vart ; varn = varn ; varl = [] } exit = exit node
+merge' node@record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = merge' (merge-tree node (λ env → skew' env (λ env → split' env (λ env → env) ) ) (λ env → env) ) exit
+-}
+
+whileTestP : {l : Level} {t : Set l} → (tree : rbt) → (n : ℕ) → (Code : Env → t) → t
+whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } )
+
+
+
+{-# 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
+
+{-
+mergeP1 : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+mergeP1 record { vart = vart ; varn = varn ; varl = [] } exit = {!!}
+mergeP1 record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = {!!}
+-}
+
+{-
+merge-tree env
+  (λ env → skew-bt env
+    (λ env → merge-rotate-left env
+      (λ env → split-branch env
+        (λ env →  merge-rotate-right env
+          (λ env → split env (λ env → mergeP env exit ) (λ env → mergeP env exit ) ) exit)
+      (λ env → mergeP env exit ) )
+    exit )
+  exit ) exit
+-}
+
+--whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (c11 : ℕ) → (Code : Envc → t) → t
+--whileTestP c10 n next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
+
+--whileTestPCall : (tree : rbt) → (n : ℕ)  → Env
+--whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → merge env (λ env → init-col env (λ env → env ) ) ) )
+
+whileTestPCall' : (tree : rbt) → (n : ℕ)  → Env
+whileTestPCall' tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → mergeP env (λ env → init-col env (λ env → env ) ) ) )
+
+-- 以下test部分
+test1 = whileTestPCall' bt-empty 8
+test2 = whileTestPCall' (vart test1) 10
+test3 = whileTestPCall' (vart test2) 24
+test4 = whileTestPCall' (vart test3) 31
+test5 = whileTestPCall' (vart test4) 41
+test6 = whileTestPCall' (vart test5) 45
+test7 = whileTestPCall' (vart test6) 50
+test8 = whileTestPCall' (vart test7) 59
+test9 = whileTestPCall' (vart test8) 73
+test10 = whileTestPCall' (vart test9) 74
+test11 = whileTestPCall' (vart test10) 79
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/src/agda/rbt_varif.agda	Mon Feb 15 21:42:10 2021 +0900
@@ -0,0 +1,54 @@
+module rbt_varif where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Binary
+open import Data.Nat hiding (_≤_  ; _≤?_)
+open import Data.List hiding ([_])
+open import Data.Product
+open import Data.Nat.Properties as NP
+
+
+
+mutual
+  data  right-List : Set where
+    [] : right-List
+    [_] : ℕ → right-List
+    _∷>_Cond_ : (x : ℕ) → (xs : right-List ) → (p : x Data.Nat.> top-r xs) → right-List
+
+  top-r : right-List → ℕ
+  top-r [] = {!!}
+  top-r [ x ] = x
+  top-r (x ∷> l Cond x₁) = x
+
+  insert-r : ℕ → right-List → right-List
+  insert-r x [] = {!!}
+  insert-r x [ y ] with <-cmp x y
+  ... | tri< a ¬b ¬c = [ y ]
+  ... | tri≈ ¬a b ¬c = [ y ]
+  ... | tri> ¬a ¬b c = x ∷>  [ y ] Cond c
+  insert-r x (y ∷> ys Cond p) with <-cmp x y
+  ... | tri< a ¬b ¬c = (y ∷> ys Cond p)
+  ... | tri≈ ¬a b ¬c = (y ∷> ys Cond p)
+  ... | tri> ¬a ¬b c = x ∷> (y ∷> ys Cond p) Cond c
+
+  data  left-List : Set where
+    [] : left-List
+    [_] : ℕ -> left-List
+    _<∷_Cond_ : (x : ℕ) -> (xs : left-List ) -> (p : x Data.Nat.< top-l xs) -> left-List
+
+  top-l : left-List → ℕ
+  top-l [] = {!!}
+  top-l [ x ] = x
+  top-l (x <∷ l Cond x₁) = x
+
+  insert-l : ℕ -> left-List -> left-List
+  insert-l x [] = [ x ]
+  insert-l x l@([ y ]) with <-cmp x y
+  ... | tri< a ¬b ¬c = x <∷ l Cond a
+  ... | tri≈ ¬a b ¬c = l
+  ... | tri> ¬a ¬b c = l
+  insert-l x l@(y <∷ ys Cond p) with <-cmp x y
+  ... | tri< a ¬b ¬c = x <∷ l Cond a
+  ... | tri≈ ¬a b ¬c = l
+
+  ... | tri> ¬a ¬b c = l
--- a/prepaper/tex/abstract.tex	Mon Feb 15 05:13:01 2021 +0900
+++ b/prepaper/tex/abstract.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -1,15 +1,17 @@
+\begin{comment}
 \renewcommand{\abstractname}{\normalsize 要 旨}
 \begin{abstract}
 	当研究室にて Continuation based C\cite{cbc-gcc} (以下CbC) なるC言語の下位言語に当たる言語を開発している。
 	先行研究\cite{ryokka-master}にて Floyd-Hoare Logic\cite{hoare}(以下Hoare Logic)を用いてその検証を行なった。
 	本稿では、先行研究にて実施されなかった CbC における RedBlackTree の検証を Hoare Logic を用いて検証することを目指す。
 \end{abstract}
+\end{comment}
 
 \renewcommand{\abstractname}{\normalsize Abstract}
 \begin{abstract}
 	We are developing a language called Continuation based C\cite{cbc-gcc} (CbC), which is a lower language of the C.
 	In a previous study\cite{ryokka-master} , Floyd-Hoare Logic\cite{hoare} (Hoare Logic) was used to validate it.
-	In this paper, we aim to use Hoare Logic to validate the red-black tree in CbC, which was not performed in previous studies.
+	In this paper, we aim to verification the Left-Learning-Red-Black Tree used Gears Agda, which was not performed in previous studies.
 \end{abstract}
 
 
--- a/prepaper/tex/agda.tex	Mon Feb 15 05:13:01 2021 +0900
+++ b/prepaper/tex/agda.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -4,7 +4,7 @@
 ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは
 Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で
 は記述したプログラムを証明することができる。
-
+\begin{comment}
 \subsection{プログラムの読み方}
 本節ではAgdaの基本事項について \coderef{plus} を例として解説する。
 
@@ -34,41 +34,4 @@
 関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。
 y が 0 になった際に計算が終了となっている。
 指折りでの足し算を実装していると捉えても良い。
-
-\subsection{Data 型}
-Deta 型とは分岐のことである。
-そのため、それぞれの動作について実装する必要がある。
-例として既出で Data 型である $ \mathbb{N} $ の実装を \coderef{Nat} に示す。
-
-\lstinputlisting[label=Nat, caption=Nat] {src/agda/Nat.agda}
-
-実装から、$ \mathbb{N} $ という型は zero と suc の2つのコンストラクタを持っていることが分かる。
-それぞれの仕様を見てみると、zeroは $ \mathbb{N} $ のみであるが、suc は (n : $ \mathbb{N} $ ) $ \rightarrow \  \mathbb{N} $ である。
-つまり、suc 自体の型は $ \mathbb{N} $ であるが、そこから $ \mathbb{N} $  に遷移するということである。
-そのため、suc からは suc か zero に遷移する必要があり、また zero に遷移することで停止する。
-したがって、数値は zero に遷移するまでの suc が遷移した数によって決定される。
-
-Data型にはそれぞれの動作について実装する必要があると述べたが、
-言い換えればパターンマッチをする必要があると言える。
-これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。
-
-\subsection{Record 型}
-Record 型とはオブジェクトあるいは構造体ののようなものである。
-\coderef{And}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。
-
-\lstinputlisting[label=And, caption=And] {src/agda/And.agda}
-
-また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。
-
-これを使用して三段論法を定義することができる。
-定義は「AならばB」かつ「BならばC」なら「AならばC」となる。
-\coderef{syllogism}を以下に示す。
-
-\lstinputlisting[label=syllogism, caption=syllogism] {src/agda/syllogism.agda}
-
-コードの解説をすると、引数として x と a が関数に与えられている。
-引数 x の中身は ((A $ \rightarrow $ B) ∧ (B $ \rightarrow $ C)) 、引数 a の中身は A である。
-したがって、(\_∧\_.p1 x a) で (A $ \rightarrow $ B) に A を与えて B を取得し、
-\_∧\_.p2 x で (B $ \rightarrow $ C) であるため、これに B を与えると C が取得できる。
-よって A を与えて C を取得することができたため、三段論法を定義できた。
-
+\end{comment}
--- a/prepaper/tex/cbc.tex	Mon Feb 15 05:13:01 2021 +0900
+++ b/prepaper/tex/cbc.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -15,7 +15,7 @@
 継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻れず、次の CodeGear へ継続を行う。
 これは、関数型プログラミングでは末尾再帰をしていることと同義である。
 
-
+\begin{comment}
 \subsection{Meta Code Gear / Meta Data Gear}
 プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、
 資源管理等を記述しなければならない処理が存在する。これらの処理をメタ計算と呼ぶ。
@@ -30,5 +30,5 @@
 CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear
 のメモリ空間等を持った Meta DataGear を扱っている。
 
+\end{comment}
 
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/tex/gearsagda.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -0,0 +1,15 @@
+\section{Gears Agda}
+本章では検証する際の手法を説明する。
+CodeGear の引数となる DataGear が事前条件となり、
+それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。
+その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。
+これらを用いて Hoare Logic によりプログラムの検証を行いたい。
+
+\subsection{CbC記法で書くagda}
+CbCプログラムの検証をするに当たり、AgdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。
+\coderef{agda-cg}が例となるコードである。
+
+\lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda}
+
+前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。
+これがAgdaで表現された CodeGear となる。
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/tex/imple.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -0,0 +1,50 @@
+\section{Left Learning Red Black Tree の実装}
+
+Left Learning Red Blacl Tree の実装において、
+通常の言語であれば再帰処理を用いて実装を行える部分を
+継続にて実行可能なように変更する必要がある。
+本節では、この課題に対して Gears Agda での
+Left Learning Red Black Tree の実装方法について述べる。
+
+\begin{center}
+  \includegraphics[height=5cm]{pic/imple.pdf}
+  \caption{再帰処理を回避する手順}
+  \label{rbt_imple}
+\end{center}
+
+41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説明する。
+まず Root node である 59 と比較した際に、41はそれより小さい。
+この際、left node に遷移するが、CbC では再帰処理が行えないため、listに保持していく。
+順々に辿っていき、対象の場所に到達すると insert / delete を行う。
+その後はlistからnodeを取り出し、結合することで Left Leaning Red Black Tree の操
+作を行う。
+
+実際の例を\coderef{insert_imple}に示す。
+
+\lstinputlisting[label=insert_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=157, lastline=166] {src/agda/rbt_t.agda}
+
+ソースコードの解説をする。上から3行はコメントで、この関数で行っていることを doに、
+next / exit では次の関数遷移先を記載している。
+
+5行目にて withを使用することで vart のパターンマッチを行っている。
+vart が bt-empty である場合に 6行目が動作する。
+bt-empty であれば node の一番下であるため、
+varn を tree の値として insert して exit に遷移する。
+
+7行目は vart が bt-empty ではないパターンの動作を記述している。
+ここでは insertを行う値である varn と 現在いる位置の tree の値と比較を行い、
+再度パターンマッチを行う。
+
+8行目は比較した結果、同値だった場合であり、そのままexitに遷移している。
+
+9行目は入力の値 varn の方が小さい場合を指している。
+vart に left tree を入れ、varl には 現在の tree から left treeを除いた
+treeを追加している。それを next に遷移させている。
+
+10行目は入力の値 varn の方が大きい場合を指している。
+9行目とは逆に、vart に right tree を入れ、varl には 現在の tree から right treeを除いた
+treeを追加している。それをまたnext に遷移させている。
+
+以上の手順により、目的の node まで辿っている。
+このようにして、再帰処理と変数への再代入を回避した記述を行った。
+
--- a/prepaper/tex/intro.tex	Mon Feb 15 05:13:01 2021 +0900
+++ b/prepaper/tex/intro.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -1,25 +1,21 @@
 \section{研究目的}
-OS やアプリケーションの信頼性を高めることは重要な課題である。
-信頼性を高める為にはプログラムが仕様を満たした実装をされていることを検証する必要がある。
-具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。
-当研究室では CbC という言語を開発している。
-CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。
-この言語の信用性を検証したい。
+OSやアプリケーションの信頼性を高めることは重要な課題である。
+信頼性を高める為にはプログラムが仕様を満たした実装を検証する必要がある。
+具体的には「モデル検査」や「定理証明」などが検証手法としてあげられる。
 
-仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。
-Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、
-事後条件が成り立つことでコマンドの検証を行う。
-この定義が CbC の実行を継続するという性質と相性が良い。
+当研究室では Continuation based C (CbC) という言語を開発している。
+CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、
+継続を導入した C言語の下位言語である。
+その為、それを実装した際のプログラムが正確に動作するのか検証を行いたい。
 
-CbCでは実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。
+CbCでは実行を継続するため、ある関数の実行結果は事後条件になるが、
+その実行結果が遷移する次の関数の事前条件になる。
 それを繋げていくため、個々の関数の
 正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。
 
-CbCではループ制御構造を取り除いているため、CbCにてループが含まれるプログラムを作成した際の検証を行う必要がある。
+CbCではループ制御構造を取り除いているため、
+CbCにてループが含まれるプログラムを作成した際の検証を行う必要がある。
 先行研究ではCbCにおけるWhileLoopの検証を行なっている。
 
 Agdaが変数への再代入を許していない為、
-ループが存在し、かつ再代入がプログラムに含まれる RedBlackTree の検証を行いたい。
-
-% これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。
-これらのことから、CbC に対応するように Agda で RedBlackTree を記述し、Hoare Logic により検証を行うことを目指す。
+ループが存在し、かつ再代入がプログラムに含まれる RedBlackTree の検証を行いたい。
\ No newline at end of file
--- a/prepaper/tex/rbtree.tex	Mon Feb 15 05:13:01 2021 +0900
+++ b/prepaper/tex/rbtree.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -1,17 +1,24 @@
-\section{RedBlackTree}
-RedBlackTree (または赤黒木)とは平衡2分探索木の一つである。
+\section{Left Learning Red Black Tree}
+Left Learning Red Black Tree (または赤黒木)とは
+Red Black Tree の仕様を満たした平衡2分探索木の一つである。
+Red Black Treeとは
 2分探索木の点にランクという概念を追加し、そのランクの違いを赤と黒の色で分け、以下の定義に基づくように
-木を構成した物である。図では省略しているが、値を持っている点の下に黒色の空の葉があり、それが外点となる
+木を構成した物である。
+図では省略しているが、値を持っている点の下に黒色の空の node があり、それが外点となる
+
+仕様を以下に箇条書きにて記す。Red Black Tree の仕様は4番目までで、
+Left Learning Red Black Tree の仕様は、それに5番目を足したものとなる。
 
 \begin{enumerate}
-  \item 各点は赤か黒の色である。
-  \item 点が赤である場合の親となる点の色は黒である。
-  \item 外点(葉。つまり一番下の点)は黒である。
-  \item 任意の点から外点までの黒色の点はいずれも同数となる。
+  \item 各点は赤か黒の色である
+  \item 点が赤である場合の親となる点の色は黒である
+  \item 外点(葉。つまり一番下の点)は黒である
+  \item 任意の点から外点までの黒色の点はいずれも同数となる
+  \item 赤の点は親から見て左側の子にしか現れない
 \end{enumerate}
 参考となる\figref{rbtree}を以下に示す。上記の定義を満たしていることが分かる。
 \begin{center}
-\includegraphics[height=3.5cm]{pic/rbtree.pdf}
+\includegraphics[height=5cm]{pic/llrbt.pdf}
 \caption{RedBlackTree の一例}
 \label{rbtree}
 \end{center}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/tex/varif.tex	Mon Feb 15 21:42:10 2021 +0900
@@ -0,0 +1,39 @@
+\section{大小関係を検証する Meta Data Gear}
+検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と
+比較することで Hoare Triple に当てはめる。
+
+Red Black Tree は Binary Search Tree の 定義を持っているので、
+parent から見て left node には parent の値より小さい値が、
+right node には大きい値が入る。これを検証する必要がある。
+
+そのために定義した証明付き Data 構造を用いた List による性質の記述を
+\coderef{list_v}に示す。
+
+\lstinputlisting[label=list_v, caption=証明付き Data 構造を持った List,firstline=12,lastline=30] {src/agda/rbt_varif.agda}
+
+証明付き Data 構造を持った List の定義は right-List で行っている。
+List の Top と比較した際に、
+Topの値より大きい値でなければ insert できない。
+加えて insert できた値が Top より大きい事を示す証明も持つ事ができる。
+
+mutual は 以下の記述全てに対して掛かっている。
+これは right-List の定義の中で、top-r　を呼び出しており、
+top-r は定義の部分で right-List を使用している。
+したがって相互呼び出しとなっている。
+Agdaは 逐次処理であるため、プログラムの上に宣言してある関数や型しか使用できない。
+mutual を掛けることで、プログラムの下で宣言している関数や型を使用する事ができる。
+
+right-List の定義は、何も入っていない場合は right-List で停止するようにしている。
+List に一つしか値が入っていない場合は、証明付き Data 構造を持つ必要がない。
+そのため特記して記述している。
+List に他の値が入っている場合は、top とその次の値との比較を証明を持っている。
+
+top-r は Listに入っている Top の値を持ってくる関数を記述している。
+insert-r は right-List に 値を insert するための関数で、
+right-List の top と入れる引数を比較し、
+inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を
+持った List となっている。
+
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slide/images/llrbt.svg	Mon Feb 15 21:42:10 2021 +0900
@@ -0,0 +1,1 @@
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" version="1.1" width="1122px" height="603px" viewBox="-0.5 -0.5 1122 603"><defs/><g><ellipse cx="201" cy="560" rx="40" ry="40" fill="#bababa" stroke="#000000" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 560px; margin-left: 162px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">24</div></div></div></foreignObject><text x="201" y="568" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">24</text></switch></g><ellipse cx="121" cy="400" rx="40" ry="40" fill="#bababa" stroke="#000000" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 400px; margin-left: 82px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">10</div></div></div></foreignObject><text x="121" y="408" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">10</text></switch></g><ellipse cx="41" cy="560" rx="40" ry="40" fill="#bababa" stroke="#000000" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 560px; margin-left: 2px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">8</div></div></div></foreignObject><text x="41" y="568" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">8</text></switch></g><ellipse cx="281" cy="240" rx="40" ry="40" fill="#f8cecc" stroke="#b85450" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 240px; margin-left: 242px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">31</div></div></div></foreignObject><text x="281" y="248" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">31</text></switch></g><path d="M 121 360 L 281 280" fill="none" stroke="#000000" stroke-width="2" stroke-miterlimit="10" pointer-events="stroke"/><path d="M 41 520 L 121 440" fill="none" stroke="#000000" stroke-width="2" stroke-miterlimit="10" pointer-events="stroke"/><path d="M 201 520 L 121 440" fill="none" stroke="#000000" stroke-width="2" stroke-miterlimit="10" pointer-events="stroke"/><ellipse cx="441" cy="400" rx="40" ry="40" fill="#bababa" stroke="#000000" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 400px; margin-left: 402px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">45</div></div></div></foreignObject><text x="441" y="408" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">45</text></switch></g><ellipse cx="361" cy="560" rx="40" ry="40" fill="#bababa" stroke="#000000" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 560px; margin-left: 322px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">41</div></div></div></foreignObject><text x="361" y="568" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">41</text></switch></g><path d="M 361 520 L 441 440" fill="none" stroke="#000000" stroke-width="2" stroke-miterlimit="10" pointer-events="stroke"/><path d="M 441 360 L 281 280" fill="none" stroke="#000000" stroke-width="2" stroke-miterlimit="10" pointer-events="stroke"/><ellipse cx="761" cy="400" rx="40" ry="40" fill="#bababa" stroke="#000000" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 400px; margin-left: 722px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">73</div></div></div></foreignObject><text x="761" y="408" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">73</text></switch></g><ellipse cx="921" cy="240" rx="40" ry="40" fill="#bababa" stroke="#000000" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 240px; margin-left: 882px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">74</div></div></div></foreignObject><text x="921" y="248" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">74</text></switch></g><path d="M 761 360 L 921 280" fill="none" stroke="#000000" stroke-width="2" stroke-miterlimit="10" pointer-events="stroke"/><ellipse cx="1081" cy="400" rx="40" ry="40" fill="#bababa" stroke="#000000" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 400px; margin-left: 1042px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">79</div></div></div></foreignObject><text x="1081" y="408" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">79</text></switch></g><path d="M 1081 360 L 921 280" fill="none" stroke="#000000" stroke-width="2" stroke-miterlimit="10" pointer-events="stroke"/><ellipse cx="601" cy="40" rx="40" ry="40" fill="#bababa" stroke="#000000" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 40px; margin-left: 562px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">59</div></div></div></foreignObject><text x="601" y="48" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">59</text></switch></g><path d="M 281 200 L 601 80" fill="none" stroke="#000000" stroke-width="2" stroke-miterlimit="10" pointer-events="stroke"/><path d="M 921 200 L 601 80" fill="none" stroke="#000000" stroke-width="2" stroke-miterlimit="10" pointer-events="stroke"/><ellipse cx="521" cy="560" rx="40" ry="40" fill="#bababa" stroke="#000000" stroke-width="2" pointer-events="all"/><g transform="translate(-0.5 -0.5)"><switch><foreignObject style="overflow: visible; text-align: left;" pointer-events="none" width="100%" height="100%" requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"><div xmlns="http://www.w3.org/1999/xhtml" style="display: flex; align-items: unsafe center; justify-content: unsafe center; width: 78px; height: 1px; padding-top: 560px; margin-left: 482px;"><div style="box-sizing: border-box; font-size: 0; text-align: center; "><div style="display: inline-block; font-size: 25px; font-family: Helvetica; color: #000000; line-height: 1.2; pointer-events: all; white-space: normal; word-wrap: normal; ">50</div></div></div></foreignObject><text x="521" y="568" fill="#000000" font-family="Helvetica" font-size="25px" text-anchor="middle">50</text></switch></g><path d="M 521 520 L 441 440" fill="none" stroke="#000000" stroke-width="2" stroke-miterlimit="10" pointer-events="stroke"/></g><switch><g requiredFeatures="http://www.w3.org/TR/SVG11/feature#Extensibility"/><a transform="translate(0,-5)" xlink:href="https://www.diagrams.net/doc/faq/svg-export-text-problems" target="_blank"><text text-anchor="middle" font-size="10px" x="50%" y="100%">Viewer does not support full SVG 1.1</text></a></switch></svg>
\ No newline at end of file
--- a/slide/slide.md	Mon Feb 15 05:13:01 2021 +0900
+++ b/slide/slide.md	Mon Feb 15 21:42:10 2021 +0900
@@ -1,5 +1,5 @@
 ---
-marp: false
+marp: true
 title: Geas Agda による Left Learning Red Black Tree の検証
 paginate: true
 
@@ -28,25 +28,24 @@
 
 ---
 <!-- class: title -->
-# Geas Agda による Left Learning Red Black Tree の検証
+# Gears Agda による <br> Left Learning Red Black Tree の検証
 
-- 上地 悠斗 
+- 上地 悠斗
     - 琉球大学工学部工学科知能情報コース
 - 河野 真治
     - 琉球大学工学部
 
 ---
 <!-- class: slide -->
-# 証明を用いたプログラムの信頼性の向上を目指す
+# 証明を用いてプログラムの信頼性の向上を目指す
 <!-- 研究目的 -->
 - プログラムの信頼性を高めることは重要な課題である
   - 信頼性を高める手法として「モデル検査」や「定理証明」など
 - 当研究室でCbCという言語を開発している
   - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
-- 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った。
+- 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った
 - 本研究では Gears Agda にて 重要なアルゴリズムの一つである Red Black Tree を検証する
 
-
 ---
 
 # これまでの成果
@@ -61,53 +60,68 @@
 - 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の一つ
 - 定義は以下である。
-<!-- 箇条書きで定義を載せる画像を載っける -->
-
+  - 各点は赤か黒の色である。
+  - 点が赤である場合の親となる点の色は黒である。
+  - 外点 (葉。つまり一番下の点) は黒である。
+  - 任意の点から外点までの黒色の点はいずれも同数となる。
+  - node は parent から見て左の node にしか 現れない
 
 ---
-# Left Leaning Red Black Tree の実装
+# 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の話ができる。 -->
+<!-- 今まで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 の性質も持っているので、大小関係を検証する必要がある
+- 検証には実装が仕様を満たしている必要がある
+- 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 へ変換ができないか調査する
 
 ---
 # まとめ
@@ -115,4 +129,4 @@
 - Left Learning Red Black Tree について記述した
 - Meta Data Gear を記述した
   - 証明付き Data 構造を用いた List による性質の記述
-- 今後検証に向けて、条件の接続ができているのかと、健全性について示す。
+- 今後検証に向けて、条件の接続と、健全性について示す