# HG changeset patch # User soto@cr.ie.u-ryukyu.ac.jp # Date 1600029683 -32400 # Node ID acad18934981987f0652fc86e6479ce2fb170e08 # Parent 4bf00f7ba825a9a95528aa7772ad9f2688f193c7 add description of rbtree diff -r 4bf00f7ba825 -r acad18934981 mid_thesis.pdf Binary file mid_thesis.pdf has changed diff -r 4bf00f7ba825 -r acad18934981 mid_thesis.tex --- 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{今後の課題} % 参考文献 diff -r 4bf00f7ba825 -r acad18934981 pic/rbtree.pdf Binary file pic/rbtree.pdf has changed diff -r 4bf00f7ba825 -r acad18934981 tex/abstract.tex --- 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. diff -r 4bf00f7ba825 -r acad18934981 tex/agda.tex --- 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 型とは分岐のことである。 diff -r 4bf00f7ba825 -r acad18934981 tex/hoare.tex --- 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} diff -r 4bf00f7ba825 -r acad18934981 tex/rbtree.tex --- /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} diff -r 4bf00f7ba825 -r acad18934981 tex/spec.tex --- 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 の 遷移の検証}