|
0
|
1 % withpage: ページ番号をつける (著者確認用)
|
|
|
2 % english: 英語原稿用フォーマット
|
|
|
3 \documentclass{ipsjprosym}
|
|
|
4 %\usepackage{graphicx}
|
|
|
5 \usepackage[T1]{fontenc}
|
|
|
6 \usepackage{lmodern}
|
|
|
7 \usepackage{textcomp}
|
|
|
8 \usepackage{latexsym}
|
|
|
9 %\usepackage[fleqn]{amsmath}
|
|
|
10 %\usepackage{amssymb}
|
|
|
11 \usepackage{listings}
|
|
|
12 \usepackage[dvipdfmx]{graphicx}
|
|
|
13 \usepackage{graphicx}
|
|
|
14 \usepackage{lmodern}
|
|
|
15 \usepackage{textcomp}
|
|
|
16 \usepackage{latexsym}
|
|
|
17 \usepackage{ascmac}
|
|
|
18 \usepackage[fleqn]{amsmath}
|
|
|
19 \usepackage{amssymb}
|
|
|
20 \usepackage[deluxe, multi]{otf}
|
|
|
21 \usepackage{url}
|
|
|
22 \usepackage{cite}
|
|
|
23 %\documentclass[withpage, english]{ipsjprosym}
|
|
|
24 \usepackage{comment}
|
|
|
25 \usepackage{here}
|
|
|
26 \lstset{
|
|
|
27 language=C,
|
|
|
28 tabsize=2,
|
|
|
29 frame=single,
|
|
|
30 basicstyle={\tt\footnotesize}, %
|
|
|
31 identifierstyle={\footnotesize}, %
|
|
|
32 commentstyle={\footnotesize\itshape}, %
|
|
|
33 keywordstyle={\footnotesize\ttfamily}, %
|
|
|
34 ndkeywordstyle={\footnotesize\ttfamily}, %
|
|
|
35 stringstyle={\footnotesize\ttfamily},
|
|
|
36 breaklines=true,
|
|
|
37 captionpos=b,
|
|
|
38 columns=[l]{fullflexible}, %
|
|
|
39 xrightmargin=0zw, %
|
|
|
40 xleftmargin=1zw, %
|
|
|
41 aboveskip=1zw,
|
|
|
42 numberstyle={\scriptsize}, %
|
|
|
43 stepnumber=1,
|
|
|
44 numbersep=0.5zw, %
|
|
|
45 lineskip=-0.5ex,
|
|
|
46 escapechar=\@,
|
|
|
47 }
|
|
|
48 \renewcommand{\lstlistingname}{Code}
|
|
|
49 \usepackage{caption}
|
|
|
50 \captionsetup[lstlisting]{font={small, tt}}
|
|
|
51 \usepackage{url}
|
|
|
52 \begin{document}
|
|
|
53
|
|
|
54 % Title, Author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
55 \title{Gears Agda による Red Black Tree の検証}
|
|
|
56
|
|
|
57 %\affiliate{IPSJ}{情報処理学会}
|
|
|
58 \affiliate{IERYUKYU}{琉球大学大学院理工学研究科工学専攻知能情報プログラム}
|
|
|
59
|
|
|
60 \author{上地 悠斗}{Yuto UECHI}{IERYUKYU}[soto@cr.ie.u-ryukyu.ac.jp]
|
|
|
61 \author{河野 真治}{Shinji KONO}{IERYUKYU}[kono@ie.u-ryukyu.ac.jp]
|
|
|
62
|
|
|
63 %概要
|
|
|
64 \begin{abstract}
|
|
|
65 OS やアプリケーションの信頼性を高めることは重要な課題である。
|
|
|
66 信頼性を高める為にはプログラムが仕様を満たした実装を検証する必要がある。
|
|
|
67 具体的には「モデル検査」や「定理証明」などが検証手法としてあげられる。
|
|
|
68 当研究室では Continuation based C (CbC) という言語を開発している。
|
|
|
69 CbC とは、 C言語からループ制御構造とサブルーチンコールを取り除き、
|
|
|
70 継続を導入した C 言語の下位言語である。
|
|
|
71 その為、それを実装した際のプログラムが正確に動作するのか検証を行いたい。
|
|
|
72 検証には定理証明を用いるため、 定理証明支援器のAgda を用いる。
|
|
|
73 agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である red black tree の検証を行う
|
|
|
74 \end{abstract}
|
|
|
75
|
|
|
76 \begin{jkeyword}
|
|
2
|
77 プログラミング言語, CbC, Gears OS, Agda, 検証
|
|
0
|
78 \end{jkeyword}
|
|
|
79
|
|
|
80 \maketitle
|
|
|
81
|
|
|
82 % Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
83 \input{tex/intro.tex} % はじめに
|
|
2
|
84 \input{tex/cbc.tex} % cbc の説明
|
|
|
85 \input{tex/agda.tex} % agda の説明
|
|
|
86 \input{tex/cbc_agda.tex}% cbc と agda(gearsagda)
|
|
|
87 \input{tex/hoare.tex} % hoare logic の説明
|
|
|
88 \input{tex/while_loop.tex} % while loop の実装と検証(簡単に)
|
|
3
|
89 \input{tex/tree_desc.tex}% Gears Agda における木構造の設計
|
|
2
|
90 % red black tree の実装(こいつも簡単に)
|
|
|
91 % red black tree の検証
|
|
0
|
92 % まとめ
|
|
|
93
|
|
|
94 \nocite{*}
|
|
|
95 \bibliographystyle{ipsjsort}
|
|
|
96 \bibliography{reference}
|
|
|
97
|
|
|
98 \end{document} |
