Binary file Report/final/figs/InsertCase.png has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Report/final/text/chapter7.aux	Thu Feb 08 15:44:09 2024 +0900
@@ -0,0 +1,26 @@
+\relax 
+\@writefile{toc}{\contentsline {chapter}{\numberline {第7章}まとめと今後の展望}{30}{}\protected@file@percent }
+\@writefile{lof}{\addvspace {10\jsc@mpt }}
+\@writefile{lot}{\addvspace {10\jsc@mpt }}
+\@setckpt{./text/chapter7}{
+\setcounter{page}{31}
+\setcounter{equation}{0}
+\setcounter{enumi}{3}
+\setcounter{enumii}{0}
+\setcounter{enumiii}{0}
+\setcounter{enumiv}{0}
+\setcounter{footnote}{0}
+\setcounter{mpfootnote}{0}
+\setcounter{part}{0}
+\setcounter{chapter}{7}
+\setcounter{section}{0}
+\setcounter{subsection}{0}
+\setcounter{subsubsection}{0}
+\setcounter{paragraph}{0}
+\setcounter{subparagraph}{0}
+\setcounter{figure}{0}
+\setcounter{table}{0}
+\setcounter{parentequation}{0}
+\setcounter{lstnumber}{20}
+\setcounter{lstlisting}{0}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Report/final/text/chapter7.tex	Thu Feb 08 15:44:09 2024 +0900
@@ -0,0 +1,7 @@
+\chapter{まとめと今後の展望}
+
+本論文では，GearsAgdaを用いたプログラムを数学的に証明する方法とRedBlackTreeの正当性をInvariantを用いて証明する実装について述べた．GearsAgdaを用いて再帰処理を使用しない記述を実装することで，GearsOSに使用されているCbC言語に直接対応するような証明を書くことが可能になった．また，Invariantを定義し，それらを保有しながら処理を行うことにより，数学的な証明を用いてRedBlackTreeの信頼性を向上させることができた．このInvariantからは，さまざまな要素を導出できることから，今後の研究において応用的な処理を記述する際にも役立つと考える．
+
+今後の課題として，Insert，deleteのなどの操作を実装することが挙げられる．現段階で証明されている操作はfindしかなく，これでは実用的なRedBlackTreeとは言えない．Insertの実装は大きな枠組みは既に完成しており，証明部分を記述していく段階である．しかし，Insertなどの木構造を変化させる操作では，木がバランスする動作を記述する必要があり，子供から見た祖父や叔父の色を見ながら場合わけをする必要がある．これにより，場合わけの数が多く実装が難しくなっているのが現状である．Insertを実装することができれば，似たようなアルゴリズムでdeleteを実装できるため，まずはInsertを簡単に記述する方法を探しつつ，着実に実装を進めていく必要がある．
+
+今後の展望として，GearsAgdaのコードをCbCのコードに変換することが挙げられる．GearsAgdaはCbCに直接対応した記述方法であるため，理論上コンパイルすることが可能である．CbC言語はC言語とアセンブラの中間に位置しており，コーディングが困難であることから，GearsAgdaを用いてコーディングできることが望ましい．これが可能になることで，CbCでの記述がGearsAgdaベースで行えるようになり，信頼性のさらなる向上につながると考える．
\ No newline at end of file