Mercurial > hg > Papers > 2020 > soto-midterm

Binary file mid_thesis.pdf has changed
--- a/mid_thesis.tex	Mon Sep 14 02:58:14 2020 +0900
+++ b/mid_thesis.tex	Mon Sep 14 05:41:23 2020 +0900
@@ -18,7 +18,7 @@
 \setlength{\textheight}{261mm}
 \setlength{\footskip}{0mm}
 \pagestyle{empty}
-\usepackage[top=2cm, bottom=2cm, left=1cm, right=1cm]{geometry}
+\usepackage[top=20mm, bottom=20mm, left=10mm, right=10mm]{geometry}
 % 特殊文字の表示に必要
 \usepackage{luatexja}
 \usepackage{fontspec}
@@ -51,10 +51,12 @@
   escapechar={@},
 }

+\usepackage{indentfirst}
+
 \begin{document}
 \ltjsetparameter{jacharrange={-3}}
-\title{Continuation based C による赤黒木の Hoare Logic を用いた検証 \\ Verification of red-black tree implemented in Continuation based C using Hoare Logic}
-\author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
+\title{\LARGE Continuation based C による RedBlackTree の Hoare Logic を用いた検証 \\ \Large Verification of red-black tree implemented in Continuation based C using Hoare Logic}
+\author{学籍番号 175706H 氏名 上地 悠斗 \and 指導教員 : 河野 真治}
 \date{}
 \maketitle
 \thispagestyle{fancy}
@@ -64,11 +66,12 @@

 % 2段組開始
 \begin{multicols*}{2}
-    \input{./tex/intro.tex} % 研究目的
-    \input{./tex/cbc.tex} % CbC の説明
-    \input{./tex/hoare.tex} % Hoare Logic の説明
-    \input{./tex/agda.tex} % agda の説明
-    \input{./tex/spec.tex}% 手法
+    \input{tex/intro.tex} % 研究目的
+    \input{tex/cbc.tex} % CbC の説明
+    \input{tex/hoare.tex} % Hoare Logic の説明
+    \input{tex/agda.tex} % agda の説明
+	\input{tex/rbtree.tex} % 赤黒木の説明
+    \input{tex/spec.tex}% 手法

 	\section{今後の課題}
 	% 参考文献
Binary file pic/rbtree.pdf has changed
--- a/tex/abstract.tex	Mon Sep 14 02:58:14 2020 +0900
+++ b/tex/abstract.tex	Mon Sep 14 05:41:23 2020 +0900
@@ -2,7 +2,8 @@
 	当研究室にて Continuation based C (以下CbC) なるC言語の下位言語に当たる言語を開発している。
 	外間による先行研究にて Floyd-Hoare Logic(以下Hoare Logic)を用いてその検証を行なった。
 	本稿では、先行研究にて実施されなかった CbC における赤黒木の検証を Hoare Logic を用いて検証することを目指す。
-	\\ \\
+	\\
+
 	We are developing a language called Continuation based C (CbC), which is a Subordinate language of the C.
 	M.Eng Hokama verified it by using Floyd-Hoare Logic (Hoare Logic) in a previous study.
 	In this paper, we aim to use Hoare Logic to validate the red-black tree in CbC, which was not performed in previous studies.
--- a/tex/agda.tex	Mon Sep 14 02:58:14 2020 +0900
+++ b/tex/agda.tex	Mon Sep 14 05:41:23 2020 +0900
@@ -9,43 +9,34 @@
 以下は Agda プログラムの一例となる。
 本節では以下のコードを説明することにより、Agda プログラムについて理解を深めることにより、
 後述する Agda コードの理解を容易にすることを目的としている。
+
+基本事項として、ℕ というのは自然数 (Natulal Number) のことである。
+また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
+ここでは関数を実行した際の例を記述している。
+したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。
+
 \lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda}

-\begin{itemize}
-	\item 基本事項
-		\begin{itemize}
-			\item
-				ℕ というのは自然数 (Natulal Number) のことである。
-				また、- (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
-				ここでは関数を実行した際の例を記述している。
-				したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。
-		\end{itemize}
-    \item 定義部分
-		\begin{itemize}
-			\item
-				コードの1行目に : (セミコロン)がある。
-				この : の前が関数名になり、その後ろがその関数の定義となる。\\
-				: の後ろの (x y : ℕ ) は関数は x, y の自然数2つを受けとる。
-				という意味になる。
-				→ の後ろは関数が返す型を記述している。
-				まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
-				自然数を返すという定義になる。
-		\end{itemize}
-	\item 実装部分
-		\begin{itemize}
-			\item
-				関数の定義をしたコードの直下で実装を行うのが常である。
-				関数名を記述した後に引数を記述して受け取り、= (イコール) の後ろで
-				引数に対応し実装を作を記述していく。
-				今回の場合では、 plus x zero であれば +0 である為、そのまま x を返す。
-				2行目の方では受け取った y の値を減らし、x の値を増やして再び plus の関数に
-				遷移している。
-				受け取った y は+1されていたことにすることでyの値を減らしている。
-				実装部分もまとめると、x と y の値を足す為に、y から x に数値を1つずつ渡す。
-				y が 0 になった際に計算が終了となっている。
-				指折りでの足し算を実装していると捉えても良い
-		\end{itemize}
-\end{itemize}
+この関数の定義部分の説明をする。コードの1行目に : (セミコロン)がある。
+この : の前が関数名になり、その後ろがその関数の定義となる。
+: 以降の (x y : ℕ ) は関数は x, y の自然数2つを受けとるという意味になる。
+→ 以降は関数が返す型を記述している。
+まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
+自然数を返すという定義になる。
+
+実装部分の説明をする。
+関数の定義をしたコードの直下で実装を行うのが常である。
+関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
+引数に対応した実装をする。
+
+今回の場合 plus x zero であれば +0 である為、そのまま x を返す。
+実装2行目の方で受け取った y の値を減らし、x の値を増やして再び plus の関数に
+遷移している。
+受け取った y を +1 されていたとして y の値を減らしている。
+
+関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。
+y が 0 になった際に計算が終了となっている。
+指折りでの足し算を実装していると捉えても良い

 \subsection{Data 型}
 Deta 型とは分岐のことである。
--- a/tex/hoare.tex	Mon Sep 14 02:58:14 2020 +0900
+++ b/tex/hoare.tex	Mon Sep 14 05:41:23 2020 +0900
@@ -1,13 +1,20 @@
 \section{Hoare Logic}
-	Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
-	これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
-	というもので、CbCの実行を継続するという性質に非常に相性が良い。
-	Hoare Logic を表記すると以下のようになる。
-    {P} C {Q}
-	この3つ組は Hoare Triple と呼ばれる。
+Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
+これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
+というもので、CbCの実行を継続するという性質に非常に相性が良い。
+Hoare Logic を表記すると以下のようになる。
+{P} C {Q}
+この3つ組は Hoare Triple と呼ばれる。
+
+Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。

-	Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。
+Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
+これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
+

-	Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
-	これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
+\begin{center}
+\includegraphics[height=3.5cm]{pic/hoare_cg_dg.pdf}
+\caption{CodeGear、DataGear での Hoare Logic}
+\label{hoare}
+\end{center}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tex/rbtree.tex	Mon Sep 14 05:41:23 2020 +0900
@@ -0,0 +1,17 @@
+\section{赤黒木}
+赤黒木とは平衡2分探索木の一つである。
+2分探索木の点にランクという概念を追加し、そのランクの違いを赤と黒の色で分け、以下の定義に基づくように
+木を構成した物である。
+
+\begin{enumerate}
+  \item 各点は赤か黒の色である。
+  \item 点が赤である場合の親となる点の色は黒である。
+  \item 外点(葉。つまり一番下の点)は黒である。
+  \item 任意の点から外点までの黒色の点はいずれも同数となる。
+\end{enumerate}
+参考となるグラフを以下に示す。上記の定義を満たしていることが分かる。
+\begin{center}
+\includegraphics[height=3.5cm]{pic/rbtree.pdf}
+\caption{CodeGear、DataGear での Hoare Logic}
+\label{hoare}
+\end{center}
--- a/tex/spec.tex	Mon Sep 14 02:58:14 2020 +0900
+++ b/tex/spec.tex	Mon Sep 14 05:41:23 2020 +0900
@@ -23,19 +23,14 @@
 今回はその Meta Gears をagdaによる検証の為に用いる。

 \begin{itemize}
-  \item Meta DataGear
-  \begin{itemize}
-    \item
-    Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
-    これを用いることで、仕様となる制約条件を記述することができる。
-  \end{itemize}
-  \item Meta CodeGear
-  \begin{itemize}
-    \item
-    Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
-    である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
-    す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである
-  \end{itemize}
+    \item Meta DataGear \mbox{}\\
+		Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
+		これを用いることで、仕様となる制約条件を記述することができる。
+
+	\item Meta CodeGear\mbox{}\\
+		Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
+		である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
+		す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである
 \end{itemize}

 \subsection{Code Gear の 遷移の検証}