# HG changeset patch # User soto # Date 1613399799 -32400 # Node ID a63df15c9afcfbf34744f043b0fdc615ce3dd329 # Parent 4361e7b7d3dbe751302dcd1667e5a2dfea6e106f DONE diff -r 4361e7b7d3db -r a63df15c9afc paper/final_thesis.pdf Binary file paper/final_thesis.pdf has changed diff -r 4361e7b7d3db -r a63df15c9afc paper/soto.bib --- a/paper/soto.bib Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/soto.bib Mon Feb 15 23:36:39 2021 +0900 @@ -64,7 +64,23 @@ school = "琉球大学 大学院理工学研究科 情報工学専攻", year = "2016" } - + +@inproceedings{mitsuki-prosym, + author = "宮城光希 and 河野真治", + title = "Code Gear と Data Gear を持つ Gears OS の設計", + booktitle = "第59回プログラミング・シンポジウム予稿集", + year = "2018", + volume = "2018", + pages = "197--206", + month = "jan" +} + +@misc{cbc-llvm, + title = {cbc-llvm - 並列信頼研 mercurial repository}, + howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_llvm/}}, + note = {Accessed: 2020/2/9(Sun)} +} + @misc{rbtree, title={データ構造と基本アルゴリズム}, author={渡邉}, diff -r 4361e7b7d3db -r a63df15c9afc paper/tex/agda.tex --- a/paper/tex/agda.tex Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/tex/agda.tex Mon Feb 15 23:36:39 2021 +0900 @@ -40,16 +40,16 @@ y が 0 になった際に計算が終了となっている。 指折りでの足し算を実装していると捉えても良い。 -\subsection{三項演算子の実装} +\subsection{二項演算子の実装} \_ (アンダースコア) を用いることで入力を受け取る事ができる。 -これを用いることで、三項演算子を実装することができる。 -以下に、三項演算子を使用した \coderef{plus} と同義の関数の例を +これを用いることで、二項演算子を実装することができる。 +以下に、二項演算子を使用した \coderef{plus} と同義の関数の例を 以下 \coderef{plus2} 挙げる。 -\lstinputlisting[label=plus2, caption=三項演算子を用いたplusの実装, firstline=5] {src/agda/plus2.agda} +\lstinputlisting[label=plus2, caption=二項演算子を用いたplusの実装, firstline=5] {src/agda/plus2.agda} 利点としては、直感的な記号論理の記述ができる。 -以下、記号論理は基本的に三項演算子を使用して記述する。 +以下、記号論理は基本的に二項演算子を使用して記述する。 \begin{comment} \subsection{Agdaにおけるラムダ計算} @@ -78,17 +78,14 @@ \subsection{Record 型の実装} Record 型とはオブジェクトあるいは構造体ののようなものである。 -\coderef{And}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 - -\lstinputlisting[label=And の定義, caption=And] {src/agda/And.agda} +\coderef{Andの定義}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 -また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。 +\lstinputlisting[label=Andの定義, caption=Andの記述] {src/agda/And.agda} -これを使用して三段論法を定義することができる。 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。 \coderef{syllogism}を以下に示す。 -\lstinputlisting[label=syllogism の実装, caption=syllogism] {src/agda/syllogism.agda} +\lstinputlisting[label=syllogism, caption=syllogism の記述] {src/agda/syllogism.agda} コードの解説をすると、引数として x と a が関数に与えられている。 引数 x の中身は ((A $ \rightarrow $ B) ∧ (B $ \rightarrow $ C)) 、引数 a の中身 @@ -97,7 +94,7 @@ よって A を与えて C を取得することができたため、三段論法を定義できた。 \section{本論で使用する Agda の記法} -本論では、ソースコードを出しながら実施内容について述べるが、 +本論では、ソースコードを出し、それの実施内容について述べるが、 特殊な記法を用いている場合があるので、前もって解説をする。 \subsection{Agdaの省略記法} @@ -106,6 +103,8 @@ これを防ぐために、withを使用し、必要な変数のみ取り出してパターンマッチを行う。 例を \coderef{abridgement} に示す。 +\newpage + \lstinputlisting[label=abridgement, caption=入力を省略する Agda コードの例, firstline=5] {src/agda/abridgement.agda} patternmatch-default は入力されている record をそのまま展開することで、 diff -r 4361e7b7d3db -r a63df15c9afc paper/tex/cbc_agda.tex --- a/paper/tex/cbc_agda.tex Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/tex/cbc_agda.tex Mon Feb 15 23:36:39 2021 +0900 @@ -1,10 +1,6 @@ \chapter{Continuation based C と Agda} -\section{検証手法} -本章では検証する際の手法を説明する。 -CodeGear の引数となる DataGear が事前条件となり、 -それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。 -その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。 -これらを用いて Hoare Logic によりプログラムの検証を行いたい。 +\section{記述手法} +本章では CbC に対応した Agda を記述する際の手法を説明する。 \subsection{GearsAgda 形式で書く agda} Agdaでは関数の再帰呼び出しが可能であるが、CbCでは値が 帰って来ない。そのためAgda @@ -21,7 +17,7 @@ Env と next と exit を受け取っている。 next と next は Env → t となっているが、 -これは env を受け取って不定の型 (t) を返すという意味である。 +これは Env を受け取って不定の型 (t) を返すという意味である。 これで 次の関数遷移先を取れるようにしている。 @@ -33,8 +29,8 @@ CbCでは再起処理を実装することはできないが、自己呼び出しを行うことはできるので、 それに合ったようにAgdaでも実装を行なう。 -17行目が実際に値を入れる部分になっています。 -Exitが実行の終了になるようにしています。 +17行目が実際に値を入れる部分で、 +Exitが実行の終了になるようにしている。 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。 これがAgdaで表現された CodeGear となり、本論では Gears Agda と呼ぶ diff -r 4361e7b7d3db -r a63df15c9afc paper/tex/rbt_imple.tex --- a/paper/tex/rbt_imple.tex Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/tex/rbt_imple.tex Mon Feb 15 23:36:39 2021 +0900 @@ -1,6 +1,6 @@ \chapter{Red Black Tree の実装} -Left Learning Red Blacl Tree の実装において、 +Left Learning Red Black Tree の実装において、 通常の言語であれば再起処理を用いて実装を行える部分を 継続にて実行可能なように変更する必要がある。 本節では、この課題に対して Gears Agda での @@ -12,14 +12,13 @@ \begin{figure}[H] \begin{center} - \includegraphics[height=7.5cm]{pic/imple/実装.pdf} + \includegraphics[height=7.5cm]{pic/imple.pdf} \end{center} \caption{再起処理を回避する手順} \label{rbt_imple} \end{figure} -41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説 -明する。 +41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説明する。 まず Root node である 59 と比較した際に、41はそれより小さい。 この際、left node に遷移するが、CbC では再起処理が行えないため、listに保持していく。 順々に辿っていき、対象の場所に到達すると insert / delete を行う。 @@ -34,13 +33,14 @@ 箇条書きにてそれぞれについて解説を行う。 -\begin{description} -\item[col] 色のことで、red と black の data 型で記述し、パターンマッチを行えるようにした -\item[node] その名の通り node に格納されている値を保存する。 色と値となる自然数が入る -\item[tree] tree の構造 を保存する。ここで node と x / right tree を持つ -\item[rbt] 上3つの要素を合わせて持つことで Left Learning Red Black Tree を定義する -\item[Env] rbt 以外に追加や削除を行う対象となる値と、 rbtを保存できる List を持つ Data Gear -\end{description} + +\begin{itemize} +\item col: 色のことで、red と black の data 型で記述し、パターンマッチを行う。 +\item node: その名の通り node に格納されている値を保存する。 色と自然数が入る +\item tree: tree の構造 を保存する。ここで node と x / right tree を持つ +\item rbt: 上3つの要素を合わせて持つことで Left Learning Red Black Tree を定義する +\item Env: rbt 以外に追加や削除を行う対象となる値と、 rbtを保存できる List を持つ Data Gear +\end{itemize} \subsection{目的の node まで辿る Gears Agda} 上記に示した手順通りにAgdaで記述すると下 \coderef{insert_imple}のようになる。 diff -r 4361e7b7d3db -r a63df15c9afc paper/tex/rbt_verif.tex --- a/paper/tex/rbt_verif.tex Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/tex/rbt_verif.tex Mon Feb 15 23:36:39 2021 +0900 @@ -1,5 +1,6 @@ -\chapter{Red Black Tree の検証} -実装が困難であったため、検証するまでには至らなかった。 +\chapter{Left Learning Red Black Tree の検証} +本章では、Left Learning Red Black Tree の +検証方法について述べる \section{Meta Data Gearの記述} 検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と @@ -46,13 +47,14 @@ inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を 持った List となっている。 +これを Left Learning Red Black Tree の 仕様を満たすように、 +全てに対して行う。 +その後、条件が接続されているのかを検証したのち、健全性について示す事で +Hoare Logic による検証ができる。 -以上を用いて Meta Data Gear を作成する Gears Agda は以下になる。 -これを用いることで、各 node より上の node の大小関係を検証できると考えた。 - %\subsection{Black node の数え上げ} %他にも、Left Learning Red Brack Tree の black node の数え上げを記述した。 diff -r 4361e7b7d3db -r a63df15c9afc paper/tex/thanks.tex --- a/paper/tex/thanks.tex Mon Feb 15 21:42:10 2021 +0900 +++ b/paper/tex/thanks.tex Mon Feb 15 23:36:39 2021 +0900 @@ -1,6 +1,12 @@ \chapter*{謝辞} -感謝します。 +本研究の水光、本論文の作成にあたり、御多忙にも関わらず終始懇切丁寧なる御指導と御教授 +を賜わりました、河野真治准教授に心より感謝致します。そして、 共に研究を行い暖か +な気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致しま +す。また、全員最終学年であるにもかかわらず、本コースのシステム更新に関わったシス +テム管理チームに感謝いたします。 +最後に、 有意義な時間を共に過ごした理工学研究科情報工学専攻の学友、 +並びに物心両面で支えてくれた家族に深く感謝致します。 \thispagestyle{empty} diff -r 4361e7b7d3db -r a63df15c9afc slide/slide.html --- a/slide/slide.html Mon Feb 15 21:42:10 2021 +0900 +++ b/slide/slide.html Mon Feb 15 23:36:39 2021 +0900 @@ -1,4 +1,4 @@ -コンテナ技術を用いた教育情報システムの構築