|
7
|
1 \documentclass[twocolumn,twoside,9.5pt]{jarticle}
|
|
|
2 \usepackage[dvipdfmx]{graphicx}
|
|
|
3 \usepackage{picins}
|
|
|
4 \usepackage{fancyhdr}
|
|
|
5 %\pagestyle{fancy}
|
|
|
6 \usepackage{abstract}
|
|
|
7 \usepackage{url}
|
|
|
8 \usepackage{bussproofs}
|
|
|
9 \usepackage{listings,jlisting}
|
|
|
10 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{../pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
|
|
|
11 \rhead{}
|
|
|
12 \cfoot{}
|
|
|
13
|
|
|
14 \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
|
|
|
15 \setlength{\headheight}{0mm}
|
|
|
16 \setlength{\headsep}{5mm}
|
|
|
17 \setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
|
|
|
18 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
|
|
|
19 \setlength{\textwidth}{181mm}
|
|
|
20 \setlength{\textheight}{261mm}
|
|
|
21 \setlength{\footskip}{0mm}
|
|
|
22 \pagestyle{empty}
|
|
|
23
|
|
|
24 \lstset{
|
|
|
25 frame=single,
|
|
|
26 keepspaces=true,
|
|
|
27 breaklines=true,
|
|
|
28 xleftmargin=0zw,
|
|
|
29 xrightmargin=0zw,
|
|
|
30 framerule=.2pt,
|
|
|
31 columns=[l]{fullflexible},
|
|
|
32 language={},
|
|
|
33 tabsize=4,
|
|
|
34 lineskip=-0.5zw,
|
|
|
35 escapechar={@},
|
|
|
36 }
|
|
|
37
|
|
|
38
|
|
|
39 \input{dummy.tex}
|
|
|
40 \renewcommand{\abstractname}{Abstract}
|
|
|
41 \begin{document}
|
|
|
42
|
|
|
43 \title{Agda と継続を用いたプログラムの検証 \\ Verification of program using Agda and continuation}
|
|
|
44 \author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治}
|
|
|
45 \date{}
|
|
|
46 \twocolumn [
|
|
|
47 \maketitle
|
|
|
48 \begin{onecolabstract}
|
|
|
49 % 高い信頼性を持つことは重要である。
|
|
|
50 % 私たちはプログラムの信頼性を高めるためにCodeGear、DataGearという単位でプログラ
|
|
|
51 % ムを書くことを提案している。
|
|
|
52 % そのためにCodeGear、DataGearという単位を使える言語 CbC を開発している。
|
|
|
53 % CbC では既存の実装でのデータの取扱が複雑になっている。
|
|
|
54 % そのためにDataGearとCodeGearを Interface という単位でまとめた。
|
|
|
55 % これら単位をAgdaでも使えるようにし、CbC で記述した Stackや Tree を Agda に
|
|
|
56 % 変換した。
|
|
|
57 % この論文ではそれらに対して幾つかの部分的な証明を試みた。
|
|
|
58
|
|
|
59 Program has high reliability. it is important.
|
|
|
60 we are proposing to write program in units of CodeGear, DataGear for increase
|
|
|
61 the reliability.
|
|
|
62 we are deceloping Continuation based C (CbC) that can use units CodeGear and
|
|
|
63 DataGear.
|
|
|
64 In CbC, the handling of data in existing implementations is complicated.
|
|
|
65 for that purpose, we can provide a interface mechanisms which are packages of
|
|
|
66 CodeGears and DataGears.
|
|
|
67 we made these units and interface available for Agda.
|
|
|
68 Also converted Stack and Tree wrote in CbC to Agda.
|
|
|
69 In this papaer, we tried several proofs on them.
|
|
|
70 %
|
|
|
71 % (we are mapping this units to Agda)
|
|
|
72 % CbC では CodeGear 、 DataGear という単位でプログラミングできる。
|
|
|
73 % ~~
|
|
|
74 % Agda で interface を実装
|
|
|
75 % interface を含めて証明ができるか
|
|
|
76 % codeとcode のあいだをcall ではなくjmpで結ぶことができる(goto)
|
|
|
77 %gotoをつかうことによりOSに必須なmeta計算を実現できる
|
|
|
78 %メタ計算は例えばメモリ管理スレッド管理CPUやGPUの資源管理そしてData/Code Gear の管理などである
|
|
|
79 %metaレベルではcode/data gear は一つの塊として操作される。これをcbcではunion dataとして実装している
|
|
|
80 %code gear 間の接続はつぎのcode gearの番号とthread structure に相当するcontextをmeta code gear にgoto する
|
|
|
81 %meta code gear で os の 機能であるメモリ管理やスレッド管理を行う。
|
|
|
82 %ユーザーレベルではmeta構造を直接見ることはなく、継続を用いた関数型プログラミングに見える
|
|
|
83 %metaレベルから見たdata gearをゆーざーれべるのcode gearに接続するにはstub というmeta code gear を用いる
|
|
|
84 %stubとmetaはユーザーレベルcodegear とdatagearから生成することができる
|
|
|
85 %本論文ではstub とcontext 管理構造を生成するスクリプトを作成した
|
|
|
86 %これによりcode gear とdeta gear をデータを操作するinterface というまとまりにすることができる。
|
|
|
87 % CbC gives Code Gear and Data Gear as programing units.
|
|
|
88 % A transfer from a Code Gear to another Code Gear is implemented using a CbC's goto statement,
|
|
|
89 % which is compiled as a jump instruction in CbC.
|
|
|
90 % CbC's goto statements provides a ways of implementing meta computations.
|
|
|
91 % From a view point of meta computation, Data Gear or Code Gear are uniform data units, which are implemented
|
|
|
92 % as union Data in CbC.
|
|
|
93 % In the meta level, a transfer from a Code Gear is a goto statement to meta Code Gear with next Code Gear number and
|
|
|
94 % a Context which corresponds thread structure or an environments in a functional programing.
|
|
|
95 % From a normal level, meta structures are not visible directly and a Code Gear looks like a function using continuations.
|
|
|
96 % A stub Code Gear is used as a bridge between meta level and normal level.
|
|
|
97 % we can generate meta Code Gear and stub Code Gear from normal level Code Gear,
|
|
|
98 % and provide a interface mechanisms which are packages of Code Gears and Data Gears.
|
|
|
99 \end{onecolabstract}]
|
|
|
100 \thispagestyle{fancy}
|
|
|
101
|
|
8
|
102 % ソフトウェアの信頼性の保証
|
|
|
103 % CbC の話(CG,DGの話も)
|
|
|
104 % メタ計算を分けてる
|
|
|
105 % context (Meta DataGear)
|
|
|
106 % そのために interface
|
|
|
107 % Agda でも interfece を実装して検証した
|
|
7
|
108
|
|
|
109 \section{ソフトウェアの信頼性の保証}
|
|
|
110 ソフトウェアの信頼性を保証することは重要である。現在ソフトウェアの信頼性を保証す
|
|
|
111 る方法として代表的なものはモデル検査と、定理証明が存在している。
|
|
|
112 当研究室では検証しやすいプログラムの単位として、 CodeGear と DataGear という単位
|
|
|
113 を用いるプログラミングスタイルを提案している。
|
|
|
114 また、 CodeGear 、 DataGear という単位を用いてプログラミングする言語として
|
|
|
115 Countinuation based C (以下 CbC) を開発している。
|
|
|
116 % 本研究では、検証や証明に直接使用できる言語として CbC を用いる。
|
|
|
117
|
|
8
|
118 CbC では通常の計算とメタ計算を分けて記述している。
|
|
|
119 しかし、CodeGear で DataGear を扱う際、 Context と呼ばれる CodeGear、 DataGear の
|
|
|
120 リスト等を持っている Meta DataGear を経由する。
|
|
9
|
121 通常の CodeGear から Meta DataGear である Context を直接扱えると、ユーザーがメタ
|
|
|
122 計算をノーマルレベルで自由に記述できてしまい、信頼性を損なう。そのため、 CbC
|
|
|
123 では Context を通して、次の CodeGear に接続する Meta CodeGear である stub
|
|
|
124 CodeGear を定義している。
|
|
7
|
125
|
|
8
|
126 CbC で実装していくにつれて特殊な stub CodeGear の記述が複雑になった。
|
|
|
127 そこで既存の実装をモジュールとして扱うために Interface という仕組みを導入した。
|
|
|
128 Interface では、DataGear に対しての操作(API)を CodeGear とその CodeGear で扱われ
|
|
|
129 ている DataGearの集合を抽象的に表現した Meta DataGear として定義されている。
|
|
|
130
|
|
|
131 本研究では CbCで使われている Interface を 、 Agda 上で定義、実装を行い、
|
|
|
132 Interface を含めた Stack と Tree の部分的な証明を行なった。
|
|
7
|
133
|
|
|
134 \section{Countinuation based C (CbC)}
|
|
|
135 Continuation based C (CbC) とは、当研究室で開発されているプログラミング言語である。
|
|
8
|
136 CbC は C 言語とほぼおなじ構文を持つが、 C の関数の代わりに CodeGear を用いて処理
|
|
|
137 を記述する。
|
|
|
138 CodeGear は関数定義の先頭に $\_\_code$ をつけて定義する。
|
|
7
|
139 CodeGear は処理の単位でそれらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。
|
|
|
140 DataGear は CodeGear が扱うデータの単位であり、処理に必要なデータが全て入っている。次の CodeGear に処理を移す際は、 goto の後に CodeGear 名と DataGear を指定する。
|
|
9
|
141 CbC ではこの継続処理がメタ計算として定義されており、通常計算である CodeGear を変
|
|
|
142 更することなく検証や資源管理等の記述を行うことができる。
|
|
8
|
143 例として CbC の簡単な例(ソースコード\ref{src:goto})と、流れ\ref{fig:code_simple}を示す。
|
|
7
|
144
|
|
8
|
145 \lstinputlisting[label=src:goto, caption=CbCコードの例]{./src/goto.cbc}
|
|
|
146 \begin{figure}[htpb]
|
|
|
147 \begin{center}
|
|
|
148 \scalebox{0.7}[0.7]{\includegraphics{fig/codesegment.pdf}}
|
|
|
149 \end{center}
|
|
|
150 \caption{ソースコード\ref{src:goto}の流れ}
|
|
|
151 \label{fig:code_simple}
|
|
|
152 \end{figure}
|
|
7
|
153
|
|
8
|
154 ソースコード\ref{src:goto}では cs0、 cs1 が CodeGear で a+b が cs0 の Output DataGear であり、
|
|
|
155 cs1 の Input DataGear になる。
|
|
|
156 流れ\ref{fig:code_simple}は cs0 から cs1 へ継続した後、 cs0 には戻らずに次の継
|
|
|
157 続に指定された CodeGear へ継続する。
|
|
|
158
|
|
|
159 \section{CbC における Interface の定義}
|
|
|
160 CbC で実装していくにつれ、stub CodeGear の記述が煩雑になった。
|
|
7
|
161 そのため 既存の実装を モジュールとして扱うため Interface を導入した。
|
|
|
162 Interface は DataGear に対して何らかの操作(API)を行う CodeGear とその
|
|
|
163 CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear
|
|
8
|
164 として定義した。例として Stack での Interface の実装(ソースコード\ref{src:interface})を示す。
|
|
7
|
165
|
|
|
166 \lstinputlisting[label=src:interface, caption=CbCでのStack-Interfaceの実装] {src/singleLinkedStackInterface.cbc}
|
|
|
167
|
|
|
168 元の実装の push では Stack を指定する必要があるが、
|
|
|
169 Interface での実装は push 先の Stack が stackImpl として扱
|
|
|
170 われている。この stackImpl は呼ばれた時の Stack と同じになる。
|
|
|
171 これにより、 ユーザーは実行時に Stack を指定する必要がなくなる。
|
|
|
172 このように Interface 記述をすることで CbC で通常記述する必要がある一定の部分を省略し呼び出
|
|
|
173 しが容易になる。
|
|
|
174
|
|
8
|
175 \section{Agda}
|
|
|
176 Agda\cite{agda} とは定理証明支援器であり依存型を関数プログラミング言語である。
|
|
|
177 依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。
|
|
|
178 CbC を Agda に変換する場合 DataGear はレコード型、 CodeGear は Agda での通常関数
|
|
|
179 として定義できる。
|
|
|
180 前項で示した CbC の簡単な例を Agda に変換する。(ソースコード\ref{src:agda-css})
|
|
7
|
181
|
|
8
|
182 \lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義]
|
|
|
183 {src/CodeSegments.agda}
|
|
7
|
184
|
|
8
|
185 Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。
|
|
|
186 関数の型では → または \verb/->/ を使い定義し、関数本体は関数名の後に$=$をつけて
|
|
|
187 記述する。
|
|
|
188 DataGear はレコード型で表記できるため Agda 上で DataGear を定義することが可能で
|
|
|
189 ある。
|
|
|
190 % 定義をする際は record キーワードのあとにレコード名、
|
|
7
|
191 % 型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコー
|
|
|
192 % ドを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙
|
|
8
|
193 % していく。複数の値を列挙する際は ; で区切る。
|
|
|
194 % Agda での DataGear の定義の例を以下のソースコード\ref{src:agda-ds}示す
|
|
|
195 % \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda}
|
|
|
196 このように CbC のコードを Agda に変換し、証明を行う。
|
|
7
|
197
|
|
8
|
198 \section{Agda における Interface の定義、実装}
|
|
|
199 Agda でも CbC と同様に Interface の定義、実装した。
|
|
|
200 例として Agda で実装した Stack-interface の一部をみる。
|
|
|
201 Stack の定義はソースコード\ref{src:agda-interface}、実装は ソースコード
|
|
|
202 \ref{src:agda-single-linked-stack}
|
|
7
|
203 として書かれている。それを Stack 側から interface を通して呼び出している。
|
|
|
204
|
|
8
|
205 \lstinputlisting[label=src:agda-interface, caption=Agda における Stack
|
|
|
206 -Interface の定義の一部] {src/AgdaInterface.agda}
|
|
|
207
|
|
7
|
208 \lstinputlisting[label=src:agda-single-linked-stack, caption=Agda における Stack
|
|
8
|
209 -Interface の実装の一部] {src/AgdaSingleLinkedStack.agda}
|
|
7
|
210
|
|
|
211 \section{Agda による Interface 部分を含めた Stack の部分的な証明}
|
|
8
|
212 今回は Interface を通した Stack で push
|
|
7
|
213 、 pop などの操作が正しく行われるかの証明を行った。
|
|
8
|
214 ここでの証明とは Stack が特定の性質を持つことを保証することである。
|
|
7
|
215
|
|
|
216 Stack の処理として様々な性質が存在するが、ここでは
|
|
|
217 「どのような状態の Stack でも、値を push した後 pop した値は直前
|
|
|
218 に入れた値と一致する」という性質を証明した。
|
|
|
219
|
|
|
220 まず始めに不定状態の Stack をソースコード~\ref{src:agda-in-some-state}
|
|
|
221 で定義した。 stackInSomeState が不定状態の Stack である。
|
|
|
222 ソースコード~\ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対し
|
|
|
223 て、 push を2回行い、 pop2 をして取れたデータは push したデータと同じものになる
|
|
|
224 ことの証明している。
|
|
|
225
|
|
|
226 \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda}
|
|
|
227
|
|
|
228 stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー
|
|
|
229 タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が
|
|
|
230 Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として
|
|
|
231 型に書いた。関数本体で返る値は$ x \equiv x1 と y \equiv y1$で両方共に成り立つ為、
|
|
|
232 refl で推論が通る。
|
|
|
233 これにより、抽象化した Stack に対して push を2回行い、 pop を行うと push したものと同じも
|
|
|
234 のを受け取れることが証明できた。
|
|
|
235
|
|
|
236 \section{まとめ}
|
|
|
237 本研究では CodeGear、 DataGear を用いたプログラミング手法を用いて、Agda で
|
|
|
238 Interface を用いたプログラムを実装、検証した。
|
|
|
239 また、 CbC で記述した時には細かく分かっていなかった Interface の型が明確に
|
|
|
240 なった。
|
|
8
|
241 今後の課題としては、Tree 側では証明が複雑化し、うまく証明できていないことと、
|
|
|
242 Hoare Logic 用いての証明を行えるように、CodeGear、DataGear をベースにした Hoare
|
|
|
243 Logic を Agda 上で定義し、実際に証明を行うことなどが挙げられる。
|
|
7
|
244
|
|
|
245 \nocite{*}
|
|
|
246 \bibliographystyle{junsrt}
|
|
|
247 \bibliography{reference}
|
|
|
248 \end{document}
|
