Mercurial > hg > Papers > 2020 > soto-midterm

changeset 8:27a6616b6683

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author soto@cr.ie.u-ryukyu.ac.jp
date Mon, 14 Sep 2020 19:58:10 +0900
parents acad18934981
children 2652bc4fc17f
files mid_thesis.pdf mid_thesis.tex tex/abstract.tex tex/agda.tex tex/cbc.tex tex/future.tex tex/hoare.tex tex/intro.tex tex/spec.tex
diffstat 9 files changed, 74 insertions(+), 58 deletions(-) [+]
line wrap: on
line diff
Binary file mid_thesis.pdf has changed
--- a/mid_thesis.tex	Mon Sep 14 05:41:23 2020 +0900
+++ b/mid_thesis.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -27,7 +27,7 @@
 	Scale=MatchLowercase
 ]
 
-\renewcommand{\abstractname}{要 旨}
+
 \lstset{
   frame=single,
   keepspaces=true,
@@ -56,7 +56,7 @@
 \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}
-\author{学籍番号 175706H 氏名 上地 悠斗 \and 指導教員 : 河野 真治}
+\author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
 \date{}
 \maketitle
 \thispagestyle{fancy}
@@ -68,14 +68,13 @@
 \begin{multicols*}{2}
     \input{tex/intro.tex} % 研究目的
     \input{tex/cbc.tex} % CbC の説明
+    \input{tex/agda.tex} % agda の説明
     \input{tex/hoare.tex} % Hoare Logic の説明
-    \input{tex/agda.tex} % agda の説明
 	\input{tex/rbtree.tex} % 赤黒木の説明
     \input{tex/spec.tex}% 手法
-
-	\section{今後の課題}
-	% 参考文献
+    \input{tex/future.tex}% 今後の課題
 	
+% 参考文献	
 \begin{thebibliography}{9}
 \bibitem{1}CbCの論文
 \bibitem{2}外間先輩の先行研究
--- a/tex/abstract.tex	Mon Sep 14 05:41:23 2020 +0900
+++ b/tex/abstract.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -1,10 +1,15 @@
+\renewcommand{\abstractname}{\normalsize 要 旨}
 \begin{abstract}
 	当研究室にて Continuation based C (以下CbC) なるC言語の下位言語に当たる言語を開発している。
 	外間による先行研究にて Floyd-Hoare Logic(以下Hoare Logic)を用いてその検証を行なった。
 	本稿では、先行研究にて実施されなかった CbC における赤黒木の検証を Hoare Logic を用いて検証することを目指す。
-	\\
+\end{abstract}
 
+\renewcommand{\abstractname}{\normalsize Abstract}
+\begin{abstract}
 	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.
 \end{abstract}
+
+
--- a/tex/agda.tex	Mon Sep 14 05:41:23 2020 +0900
+++ b/tex/agda.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -7,8 +7,7 @@
 
 \subsection{プログラムの読み方}
 以下は Agda プログラムの一例となる。
-本節では以下のコードを説明することにより、Agda プログラムについて理解を深めることにより、
-後述する Agda コードの理解を容易にすることを目的としている。
+本節ではAgdaの基本事項について解説する。
 
 基本事項として、ℕ というのは自然数 (Natulal Number) のことである。
 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
@@ -24,7 +23,6 @@
 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
 自然数を返すという定義になる。
 		
-実装部分の説明をする。
 関数の定義をしたコードの直下で実装を行うのが常である。
 関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
 引数に対応した実装をする。
@@ -36,7 +34,7 @@
 
 関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。
 y が 0 になった際に計算が終了となっている。
-指折りでの足し算を実装していると捉えても良い
+指折りでの足し算を実装していると捉えても良い。
 
 \subsection{Data 型}
 Deta 型とは分岐のことである。
--- a/tex/cbc.tex	Mon Sep 14 05:41:23 2020 +0900
+++ b/tex/cbc.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -1,42 +1,34 @@
 \section{Continuation based C}
-	前述した通り CbC とはC言語からループ制御構造とサブルーチンコールを取り除き、
-	継続を導入したC言語の下位言語である。継続呼び出しは引数付き goto 文で表現される。
-	また、CodeGear を処理の単位、DataGear をデータの単位として記述するプログラミング言語である。
-	CbC のプログラミングでは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を行う。
+CbC とはC言語からループ制御構造とサブルーチンコールを取り除き、
+継続を導入したC言語の下位言語である。継続呼び出しは引数付き goto 文で表現される。
+また、CodeGear を処理の単位、DataGear をデータの単位として記述するプログラミング言語である。
+CbC のプログラミングでは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を行う。
 
 \subsection{Code Gear / Data Gear}
-	CbCでは、検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いるプログラミングスタイルを提案している。
+CbCでは、検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いる。
 
-	CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。
-	DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。
-	CodeGear の入力となる DataGear を Input DataGear と呼び、出力は Output DataGear と呼ぶ。
-	
-	CodeGear 間の移動は継続を用いて行われる。
-	継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、次の CodeGear へ継続を行う。
-	これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。
+CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。
+DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。
+CodeGear の入力となる DataGear を Input DataGear と呼び、出力は Output DataGear と呼ぶ。
+
+CodeGear 間の移動は継続を用いて行われる。
+継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻れず、次の CodeGear へ継続を行う。
+これは、関数型プログラミングでは末尾再帰をしていることと同義である。
 
 
 \subsection{Meta Code Gear / Meta Data Gear}
-	プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、
-	資源管理等を記述しなければならない処理が存在する。
-	これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。
+プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、
+資源管理等を記述しなければならない処理が存在する。これらの処理をメタ計算と呼ぶ。
 
-	メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。
-	そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。
-
-	Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。
-	CodeGear を実行する前後やDataGear の大枠として Meta Gear が存在している。
+メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。
+そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。
 
-	例として CodeGear が DataGear から値を取得する際に使われる、 stub CodeGear について説明する。
+Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。
+CodeGear を実行する前後やDataGear の大枠として Meta Gear が存在している。
 
-	CbC では CodeGear を実行する際、ノーマルレベルの計算からは見えないが
-	必要な DataGear を Context と呼ばれる Meta DataGear を通して取得することになる。
-	これはユーザーが直接データを扱える状態では信頼性が高いとは言えないと考えるからである。
-	そのために、 Meta CodeGear として Context から必要な DataGear を取り出し、
-	CodeGear に接続する stub CodeGear という Meta CodeGear を定義している。
-
-	Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub
-	CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear
-	のメモリ空間等を持った Meta DataGear を扱っている。
+Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub
+CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear
+のメモリ空間等を持った Meta DataGear を扱っている。
 
 
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tex/future.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -0,0 +1,12 @@
+\section{今後の課題}
+今後の課題として、以下が挙げられる。
+赤黒木の基本操作として insert や delete が挙げられる。
+通常は、再代入などを用いて実装を行うと思われるが、agda が変数への代入を許していないため、
+操作後の赤黒木を再構成するように実装を行う必要がある。
+その際にどこの状態の検証を行うかが課題になっている。
+
+先行研究にて、
+個々の Code Gear の条件を書いてそれを接続することは agda で実装されている。
+しかし、接続された条件が健全であるか証明されていない。
+
+今後はこの接続された条件の健全性の証明からしていく。
--- a/tex/hoare.tex	Mon Sep 14 05:41:23 2020 +0900
+++ b/tex/hoare.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -3,7 +3,7 @@
 これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
 というもので、CbCの実行を継続するという性質に非常に相性が良い。
 Hoare Logic を表記すると以下のようになる。
-{P} C {Q}
+$$ \{P\}\ C \ \{Q\} $$
 この3つ組は Hoare Triple と呼ばれる。
 
 Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。
@@ -11,6 +11,12 @@
 Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
 これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
 
+\subsection{Hoare による Code Gear の検証 }
+
+以下の図が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる。
+input DataGear が Hoare Logic上の Pre Condition(事前条件)となり、output DataGear が Post Conditionとなる。
+各DataGear が Pre / Post Condition を満たしているかの検証は、各 Condition を Meta DataGear で定義し、
+条件を満たしているのかをMeta CodeGear で検証する。
 
 \begin{center}
 \includegraphics[height=3.5cm]{pic/hoare_cg_dg.pdf}
@@ -18,3 +24,5 @@
 \label{hoare}
 \end{center}
 
+
+
--- a/tex/intro.tex	Mon Sep 14 05:41:23 2020 +0900
+++ b/tex/intro.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -1,15 +1,19 @@
 \section{研究目的}
-	OS やアプリケーションの信頼性を高めることは重要な課題である。
-	信頼性を高める為には仕様を満たしたプログラムが実装されていることを検証する必要がある。
-	具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。
+OS やアプリケーションの信頼性を高めることは重要な課題である。
+信頼性を高める為には仕様を満たしたプログラムが実装されていることを検証する必要がある。
+具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。
+研究室で CbC という言語を開発している。
+CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。
+この言語の信用性を検証したい。
 
-	研究室で CbC という言語を開発している。
-	CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。
-	この言語の信用性を検証したい。
-	
-	仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。
-	Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、
-	に事後条件が成り立つことでコマンドの検証を行う。
-	
-	CbC の実行を継続するという性質が Hoare Logic の事前条件と事後条件の定義から検証を行うことと非常に相性が良い。
-	これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。
+仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。
+Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、
+に事後条件が成り立つことでコマンドの検証を行う。
+この定義が CbC の実行を継続するという性質と相性が良い。
+
+CbCでは実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。
+それを繋げていくので、個々の関数の
+正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。
+
+% これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。
+これらのことから、本稿では CbC に対応するようにagdaで記述し、Hoare Logic により検証を行うことを目指す。
--- a/tex/spec.tex	Mon Sep 14 05:41:23 2020 +0900
+++ b/tex/spec.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -1,7 +1,5 @@
 \section{検証手法}
-手法は模索中であり、大半が先行研究と同じ手法を考えている。
-本章では先行研究で述べられている検証手法について説明する。
-流れとしては、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に
+現在提案している手法は、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に
 コマンドの部分的な正当性を導けることを前述した。
 その為、agdaでのcbcの検証は下図のようになる。
 流れを説明すると、