Mercurial > hg > Papers > 2020 > soto-midterm

comparison mid_thesis.tex @ 3:b124f02ea3f1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
post agda code
author soto@cr.ie.u-ryukyu.ac.jp
date Wed, 09 Sep 2020 22:07:32 +0900
parents 73127e0ab57c
children 35f0e5f12fe6
comparison
equal deleted inserted replaced
2:0d85c5be9fb6 3:b124f02ea3f1
1 \documentclass[a4j,9.5pt]{jarticle} 1 \documentclass[a4j,9.5pt]{article}
2 % \usepackage[dvips]{graphicx} 2 \usepackage{graphicx}
3 \usepackage{picins} 3 \usepackage{picins}
4 \usepackage{fancyhdr} 4 \usepackage{fancyhdr}
5 \usepackage[]{multicol} 5 \usepackage[]{multicol}
6 \usepackage{listings,jlisting} 6 \usepackage{listings}
7 %\pagestyle{fancy} 7 %\pagestyle{fancy}
8 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部工学科知能情報コース 中間発表予稿} 8 \lhead{\parpic{\includegraphics[height=1\zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部工学科知能情報コース 中間発表予稿}
9 \rhead{} 9 \rhead{}
10 \cfoot{} 10 \cfoot{}
11 11
12 \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}} 12 \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
13 \setlength{\headheight}{0mm} 13 \setlength{\headheight}{0mm}
16 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}} 16 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
17 \setlength{\textwidth}{181mm} 17 \setlength{\textwidth}{181mm}
18 \setlength{\textheight}{261mm} 18 \setlength{\textheight}{261mm}
19 \setlength{\footskip}{0mm} 19 \setlength{\footskip}{0mm}
20 \pagestyle{empty} 20 \pagestyle{empty}
21 21 \usepackage[top=2cm, bottom=2cm, left=1cm, right=1cm]{geometry}
22 22 % 特殊文字の表示に必要
23 \usepackage{ascmac} 23 \usepackage{luatexja}
24 \usepackage[dvipdfmx]{graphicx} 24 \usepackage{fontspec}
25 \usepackage{amssymb} 25 \setmainfont{STIX Math}%
26 \usepackage{type1cm} 26 \setmonofont{STIXGeneralBol}[
27 \usepackage[usenames]{color} 27 Scale=MatchLowercase
28 \usepackage{ulem} 28 ]
29 29
30 \renewcommand{\abstractname}{要 旨} 30 \renewcommand{\abstractname}{要 旨}
31 \lstset{ 31 \lstset{
32 frame=single, 32 frame=single,
33 keepspaces=true, 33 keepspaces=true,
35 commentstyle={\ttfamily}, 35 commentstyle={\ttfamily},
36 identifierstyle={\ttfamily}, 36 identifierstyle={\ttfamily},
37 keywordstyle={\ttfamily}, 37 keywordstyle={\ttfamily},
38 basicstyle={\small\ttfamily}, 38 basicstyle={\small\ttfamily},
39 breaklines=true, 39 breaklines=true,
40 xleftmargin=0zw, 40 xleftmargin=0\zw,
41 xrightmargin=0zw, 41 xrightmargin=0\zw,
42 framerule=.3pt, 42 framerule=.3pt,
43 columns=[l]{fullflexible}, 43 columns=[l]{fullflexible},
44 numbers=none, 44 numbers=none,
45 stepnumber=1, 45 stepnumber=1,
46 numberstyle={\scriptsize}, 46 numberstyle={\scriptsize},
47 numbersep=2em, 47 numbersep=2em,
48 language={}, 48 language={},
49 tabsize=4, 49 tabsize=4,
50 lineskip=-0.1zw, 50 lineskip=-0.1\zw,
51 escapechar={@}, 51 escapechar={@},
52 } 52 }
53 53
54 \begin{document} 54 \begin{document}
55 \title{Continuation based C での Hoare Logic を用いた赤黒木の検証 \\ Validation of red-black tree implemented in Continuation based C using Hoare Logic} 55 \ltjsetparameter{jacharrange={-3}}
56 \title{Continuation based C による赤黒木の Hoare Logic を用いた検証 \\ Verification of red-black tree implemented in Continuation based C using Hoare Logic}
56 \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治} 57 \author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
57 \date{} 58 \date{}
58 \maketitle 59 \maketitle
59 \thispagestyle{fancy} 60 \thispagestyle{fancy}
60 61
61 % 要旨 62 % 要旨
62 \input{./tex/abstract/abstract.tex} 63 \input{./tex/abstract.tex}
63 64
65 % 2段組開始
64 \begin{multicols}{2} 66 \begin{multicols}{2}
65 \input{./tex/intro/intro.tex} 67 \input{./tex/intro.tex} % 研究目的
66 68 \input{./tex/cbc.tex} % CbC の説明
67 \section{Continuation based C} 69 \input{./tex/hoare.tex} % Hoare Logic の説明
68 前述した通り CbC とはC言語からループ制御構造とサブルーチンコールを取り除き、 70 \input{./tex/agda.tex} % agda の説明
69 継続を導入したC言語の下位言語である。継続呼び出しは引数付き goto 文で表現される。 71 \input{./tex/spec.tex}% 手法
70 また、CodeGear を処理の単位、DataGear をデータの単位として記述するプログラミング言語である。
71 CbC のプログラミングでは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を行う。
72
73 \subsection{Code Gear / Data Gear}
74 CbCでは、検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いるプログラミングスタイルを提案している。
75
76 CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。
77 DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。
78 CodeGear の入力となる DataGear を Input DataGear と呼び、出力は Output DataGear と呼ぶ。
79
80 CodeGear 間の移動は継続を用いて行われる。
81 継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、次の CodeGear へ継続を行う。
82 これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。
83
84
85 \subsection{Meta Code Gear / Meta Data Gear}
86 プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、
87 資源管理等を記述しなければならない処理が存在する。
88 これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。
89
90 メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。
91 そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。
92
93 Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。
94 CodeGear を実行する前後やDataGear の大枠として Meta Gear が存在している。
95
96 例として CodeGear が DataGear から値を取得する際に使われる、 stub CodeGear について説明する。
97
98 CbC では CodeGear を実行する際、ノーマルレベルの計算からは見えないが
99 必要な DataGear を Context と呼ばれる Meta DataGear を通して取得することになる。
100 これはユーザーが直接データを扱える状態では信頼性が高いとは言えないと考えるからである。
101 そのために、 Meta CodeGear として Context から必要な DataGear を取り出し、
102 CodeGear に接続する stub CodeGear という Meta CodeGear を定義している。
103
104 Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub
105 CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear
106 のメモリ空間等を持った Meta DataGear を扱っている。
107
108
109 \section{Hoare Logic}
110 Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
111 これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
112 というもので、CbCの実行を継続するという性質に非常に相性が良い。
113 Hoare Logic を表記すると以下のようになる。
114 $$ \{P\}\ C\ \{Q\} $$
115 この3つ組は Hoare Triple と呼ばれる。
116
117 Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。
118
119 Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
120 これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
121
122 \section{agda}
123 agdaとは、Agda は依存型をもつ純粋関数型の言語である。 定理証明支援器でもある。
124
125 \section{関連研究}
126 外間による研究では CbC にて実装された While Loop を Hoare Logic を用いて検証した。
127
128 \section{検証手法}
129 手法は模索中であり、先行研究と同じ手法を取ろうとしている。本章では先行研究で述べられている検証手法について説明する。
130
131 % 手法
132 \input{./tex/spec/spec.tex}
133 72
134 \section{今後の課題} 73 \section{今後の課題}
135 d
136 74
137 \section{類似技術} 75 \section{類似技術}
138 76
139 \subsection{coq} 77 \subsection{coq}
140 78
79 % 参考文献
141 \begin{thebibliography}{9} 80 \begin{thebibliography}{9}
142 81
143 \bibitem{1}CbCの論文 82 \bibitem{1}CbCの論文
144 \bibitem{2}外間先輩の先行研究 83 \bibitem{2}外間先輩の先行研究
145 \bibitem{3}Hoare Logicの論文 84 \bibitem{3}Hoare Logicの論文
147 \bibitem{5}agda のサイト 86 \bibitem{5}agda のサイト
148 \bibitem{6}Aaron Stumpの本 87 \bibitem{6}Aaron Stumpの本
149 \bibitem{7}atttonさんの論文 88 \bibitem{7}atttonさんの論文
150 \bibitem{8}Haskell 89 \bibitem{8}Haskell
151 \bibitem{9}Coq 90 \bibitem{9}Coq
91 \end{thebibliography}
152 92
153 \end{thebibliography}
154 \end{multicols} 93 \end{multicols}
155 94
156 \end{document} 95 \end{document}