Binary file Paper/fig/rbt-stack.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/paper_info.txt	Wed Nov 10 10:34:48 2021 +0900
@@ -0,0 +1,21 @@
+論文タイトル：Gears Agda による Red Black Tree の検証
+
+論文タイトル英語：Red Black Tree verification by Gears Agda
+
+キーワード：プログラミング言語, CbC, Gears OS, Agda, 検証
+
+著者名：上地 悠斗
+
+著者名英語：Yuto Uechi
+
+著者所属：琉球大学大学院理工学研究科工学専攻知能情報プログラム
+
+著者所属英語：Graduate School of Computer sience & Intelligent systems, University of the Ryukyus
+
+論文抄録（日本語論文の場合）：OS やアプリケーションの信頼性を高めることは重要な課題である。
+信頼性を高める為にはプログラムが仕様を満たした実装を検証する必要がある。
+具体的には「モデル検査」や「定理証明」などが検証手法としてあげられる。
+当研究室では Continuation based C (CbC) という言語を開発している。
+CbC とは、 C 言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C 言語の下位言語である。
+その為、それを実装した際のプログラムが正確に動作するのか検証を行いたい。検証には定理証明を用いるため、 定理証明支援器の Agda を用いる。
+agda が変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である red black tree の検証を行う
\ No newline at end of file

--- a/Paper/soto.tex	Sun Nov 07 00:51:16 2021 +0900
+++ b/Paper/soto.tex	Wed Nov 10 10:34:48 2021 +0900
@@ -1,5 +1,6 @@
 % withpage: ページ番号をつける (著者確認用)
 % english: 英語原稿用フォーマット
+\AtBeginDvi{\special{pdf:mapfile ptex-ipa.map}}
 \documentclass{ipsjprosym}
 %\usepackage{graphicx}
 \usepackage[T1]{fontenc}

--- a/Paper/tex/agda.tex	Sun Nov 07 00:51:16 2021 +0900
+++ b/Paper/tex/agda.tex	Wed Nov 10 10:34:48 2021 +0900
@@ -109,7 +109,7 @@
 ここでは \verb/rewrite/ と ≡\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。
 
 \verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し、複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する。
-Code \ref{agda-rewrite} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である。
+Code \ref{agda-term-post} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である。
 ここでは、\verb/+zero/ を利用し、 \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり、左右の項が等しいことを示す \verb/refl/ になっている。
 
 \lstinputlisting[caption=等式変形の例3/3,label=agda-term-post]{src/agda-term3.agda.replaced}

--- a/Paper/tex/cbc_agda.tex	Sun Nov 07 00:51:16 2021 +0900
+++ b/Paper/tex/cbc_agda.tex	Wed Nov 10 10:34:48 2021 +0900
@@ -6,7 +6,7 @@
 で実装を行う際には再帰呼び出しを行わないようにする。
 code \ref{agda-cg}が例となるコードである。
 
-\lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg, firstline=6]{src/agda/cbc-agda.agda}
+\lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg, firstline=6]{src/agda/cbc-agda.agda.replaced}
 
 1行目で Data Gear の定義を行っている。
 今回は 2つの数値の足し算を行うコードを実装するため、

--- a/Paper/tex/tree_desc.tex	Sun Nov 07 00:51:16 2021 +0900
+++ b/Paper/tex/tree_desc.tex	Wed Nov 10 10:34:48 2021 +0900
@@ -3,12 +3,21 @@
 本研究では、Gears Agda にて Red Black Tree の検証を行うにあたり、
 Agda が変数に対して再代入を許していないことが問題になってくる。
 
-そのため下図のように、木構造の root から leaf　に 辿る際に見ているnodeから
+そのため下図 \ref{rbt-stack} のように、木構造の root から leaf　に 辿る際に見ているnodeから
 下の　tree をそのまま stack に持つようにする。
 
 そして insert や delete を行った後に stack から tree を取り出し、
 元の木構造を再構築 していきながら　rootへ戻る。
 
+\begin{figure}[H]
+  \begin{center}
+    \includegraphics[height=3.5cm]{fig/rbt-stack.pdf}
+  \end{center}
+  \caption{tree を stack して目的の node まで辿った場合の例}
+  \label{rbt-stack}
+\end{figure}
+
+
 このようにして Gears Agda にて Red Black Tree を実装していく。
 
 \section{Gears Agda における Binary Tree の実装}
@@ -84,6 +93,16 @@
 現時点では条件を満たしていることの証明まで行っていないが
 コード中の {!!} に記述を行い、前述した While Loop と同じように中身を記述することで検証を行える。
 
+\section{まとめと今後の課題}
+本論文では、Gears Agda にて Hoare Logic を用いて While Loop の検証を行えた。
+これはプログラムが Code Gear という単位で分かれているため、
+一つ一つの Code Gear に対して検証を行いながら実装を行っていくことも可能である。
+そのため、従来の検証手法よりもスコープが小さく、簡単に検証と実装を行えると考える。
+
+今後の課題として、Gears Agda による Red Black Tree の実装と検証を行う必要がある。
+While Loop と同じように検証を行えると考えているが、研究目的である
+「ループが存在し、かつ再代入がプログラムに含まれるデータ構造」を
+Gaers Agda を実装することが難しく、それをさらに検証しなければならない。
 
 
 

--- a/rbt/rbt.agda	Sun Nov 07 00:51:16 2021 +0900
+++ b/rbt/rbt.agda	Wed Nov 10 10:34:48 2021 +0900
@@ -1,2 +1,150 @@
 module rbt where
 
+open import Data.Nat
+open import Level renaming (zero to Z ; suc to succ)
+open import Data.List
+
+open import Data.Nat.Properties as NatProp -- <-cmp
+open import Relation.Binary
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+open import Data.Product
+
+open import Function as F hiding (const)
+
+open import Level renaming (zero to Z ; suc to succ)
+
+open import Data.Nat hiding (compare)
+open import Data.Nat.Properties as NatProp
+open import Data.Maybe
+-- open import Data.Maybe.Properties
+open import Data.Empty
+open import Data.List
+open import Data.Product
+
+open import Function as F hiding (const)
+
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+
+data coler : Set where
+  red : coler
+  black : coler
+
+data bool : Set where
+  true : bool
+  false : bool
+
+data rbt {n : Level} (A : Set n) : Set n where
+  leaf : rbt A
+  node : (key-t : ℕ) →  (col : coler) → (value : A) →
+    (ltree : rbt A ) → (rtree : rbt A ) → rbt A
+
+record Env {n : Level} (A : Set n) : Set n where
+  field
+    varn : ℕ
+    varv : A
+    vart : rbt A
+    varl : List (rbt A)
+    flag : bool
+open Env
+
+find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
+           → (next : (env : Env A ) → t )
+           → (exit : (env : Env A ) → t ) → t
+find env next exit = find-c (vart env) env next exit where
+    find-c : {n m : Level} {A : Set n} {t : Set m} → (tree : rbt A) → (env : Env A )
+           → (next : (env : Env A ) → t )
+           → (exit : (env : Env A ) → t ) → t
+    find-c leaf env next exit = exit env
+    find-c n@(node key-t col value ltree rtree) env next exit with <-cmp (varn env) key-t
+    ... | tri< a ¬b ¬c = find-c ltree record env {vart = ltree ; varl = (n ∷ (varl env))} next exit
+    ... | tri≈ ¬a b ¬c = exit record env {vart = n}
+    ... | tri> ¬a ¬b c = find-c rtree record env {vart = rtree ; varl = (n ∷ (varl env))} next exit
+
+replaceNode1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
+    → (next : Env A → t) → t
+replaceNode1 env next with vart env
+... | leaf = next record env {vart = (node (varn env) red (varv env) leaf leaf) }
+... | node key-t col value ltree rtree = next record env {vart = (node (varn env) col (varv env) ltree rtree) }
+
+replace : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
+    → (next : Env A → t )
+    → (exit : Env A → t) → t
+replace env next exit = replace-c (varl env) env exit where
+    split-c : {n m : Level} {A : Set n} {t : Set m} → Env A → (exit : Env A → t) → t
+    split-c env exit with (vart env)
+    ... | leaf = {!!}  -- replace-c
+    ... | node key-t col value leaf leaf = {!!}
+    ... | node key-t col value leaf (node key-t₁ col₁ value₁ rtree rtree₁) = {!!}
+    ... | node key-t col value (node key-t₁ col₁ value₁ ltree ltree₁) leaf = {!!}
+    ... | node key-t col value (node key-t₁ col₁ value₁ ltree ltree₁) (node key-t₂ col₂ value₂ rtree rtree₁) = {!!}
+    marge-left-tree : {n m : Level} {A : Set n} {t : Set m} → Env A → (exit : Env A → t) → t
+    marge-left-tree env exit with (varl env)
+    ... | [] = {!!} -- split
+    ... | tree ∷ st with (vart env)
+    ... | leaf = {!!} -- split
+    ... | node key-t col value x x₁ = {!!} -- split
+    rotate-left : {n m : Level} {A : Set n} {t : Set m} → (rbt A) → Env A → (next : Env A → t) → (exit : Env A → t) → t
+    rotate-left tree env next exit with varl env
+    ... | [] = {!!} -- split
+    ... | tree ∷ st with vart env
+    ... | leaf = {!!} -- split
+    ... | node nkey-t ncol nvalue nltree nrtree with tree
+    ... | leaf = {!!} -- split
+    ... | node key-t col value ltree leaf = exit env
+    ... | node key-t col value ltree rtree@(node rkey-t rcol rvalue rltree rrtree)
+        = next record env { vart = node nkey-t ncol nvalue
+          (node rkey-t col rvalue (node key-t red value ltree rltree) rrtree) -- ltree
+          nrtree
+        ; varn = varn env; varl = varl env }
+    replace-c : {n m : Level} {A : Set n} {t : Set m} → List (rbt A) → (env : Env A)
+        → (exit : Env A → t) → t
+    balance_insert_left : {n m : Level} {A : Set n} {t : Set m} → List (rbt A)  → (rbt A) → (env : Env A)
+        → (exit : Env A → t ) → t
+    balance_insert_left st tree env exit with flag env
+    ... | true = replace-c st env exit
+    ... | false with tree
+    ... | leaf = {!!} -- split
+    ... | node key-t col value leaf rtree = {!!} --split
+    ... | node key-t col value ltree@(node lkey-t lcol lvalue lltree lrtree) rtree with lrtree
+    ... | leaf = {!!} --split
+    ... | (node lrkey-t black lrvalue lrltree lrrtree) = {!!} -- split
+    ... | (node lrkey-t red lrvalue lrltree lrrtree)
+        = rotate-left ltree env (λ env → replace-c st env exit) (λ env → {!!}) -- rotate left
+    replace-c st env exit with st
+    ... | [] = exit env
+    ... | leaf ∷ st1 = replace-c st1 env  exit
+    ... | n@(node key-t col value ltree rtree) ∷ st1 with <-cmp (varn env) (key-t)
+    ... | tri< a ¬b ¬c = balance_insert_left st1 (node key-t col value (vart env) rtree) record env{vart = (node key-t col value (vart env) rtree); varl = st1} exit -- balance left
+    ... | tri≈ ¬a b ¬c = replace-c st1 record env{vart = (node key-t col (varv env) ltree rtree); varl = st1} exit -- そのままloop
+    ... | tri> ¬a ¬b c = replace-c st1 record env{vart = (node key-t col value ltree (vart env)); varl = st1} exit -- balance right
+
+-- 左回転、exitはsplit_branchへ　nextもsplit_branchへ
+rotate-left : {n m : Level} {A : Set n} {t : Set m} → Env A → (next : Env A → t) → (exit : Env A → t) → t
+rotate-left env next exit with vart env
+... | leaf = exit env
+... | node key-t col value ltree leaf = exit env
+... | node key-t col value ltree rtree@(node rkey-t rcol rvalue rltree rrtree)
+    = next record env { vart = (node rkey-t col rvalue
+      (node key-t red value ltree rltree)
+      rrtree)
+    ; varn = varn env; varl = varl env }
+
+-- 右回転、実行時splitへ、それ以外はmerge-treeへ
+rotate-right : {n m : Level} {A : Set n} {t : Set m} → Env A → (next : Env A → t) → (exit : Env A → t) → t
+rotate-right env next exit with vart env
+... | leaf = exit env
+... | node key-t col value leaf rtree = exit env
+... | node key-t col value (node lkey-t lcol lvalue lltree lrtree) rtree
+    = next record env { vart = (node lkey-t col lvalue
+      lltree
+      (node key-t red value lrtree rtree) )
+    ; varn = varn env; varl = varl env }
+
+
+
+
+