|
103
|
1 <!DOCTYPE html>
|
|
|
2 <html>
|
|
|
3 <head>
|
|
|
4 <meta http-equiv="content-type" content="text/html;charset=utf-8">
|
|
|
5 <title>メタ計算を用いた Continuation based C の検証手法</title>
|
|
|
6
|
|
|
7 <meta name="generator" content="Slide Show (S9) v2.5.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]">
|
|
|
8 <meta name="author" content="Yasutaka Higa" >
|
|
|
9
|
|
|
10 <!-- style sheet links -->
|
|
|
11 <link rel="stylesheet" href="s6/themes/projection.css" media="screen,projection">
|
|
|
12 <link rel="stylesheet" href="s6/themes/screen.css" media="screen">
|
|
|
13 <link rel="stylesheet" href="s6/themes/print.css" media="print">
|
|
|
14 <link rel="stylesheet" href="s6/themes/blank.css" media="screen,projection">
|
|
|
15
|
|
|
16 <!-- JS -->
|
|
|
17 <script src="s6/js/jquery-1.11.3.min.js"></script>
|
|
|
18 <script src="s6/js/jquery.slideshow.js"></script>
|
|
|
19 <script src="s6/js/jquery.slideshow.counter.js"></script>
|
|
|
20 <script src="s6/js/jquery.slideshow.controls.js"></script>
|
|
|
21 <script src="s6/js/jquery.slideshow.footer.js"></script>
|
|
|
22 <script src="s6/js/jquery.slideshow.autoplay.js"></script>
|
|
|
23
|
|
|
24 <!-- prettify -->
|
|
|
25 <link rel="stylesheet" href="scripts/prettify.css">
|
|
|
26 <script src="scripts/prettify.js"></script>
|
|
|
27
|
|
|
28 <script>
|
|
|
29 $(document).ready( function() {
|
|
|
30 Slideshow.init();
|
|
|
31
|
|
|
32 $('code').each(function(_, el) {
|
|
|
33 if (!el.classList.contains('noprettyprint')) {
|
|
|
34 el.classList.add('prettyprint');
|
|
|
35 }
|
|
|
36 });
|
|
|
37 prettyPrint();
|
|
|
38 } );
|
|
|
39
|
|
|
40
|
|
|
41 </script>
|
|
|
42
|
|
|
43 <!-- Better Browser Banner for Microsoft Internet Explorer (IE) -->
|
|
|
44 <!--[if IE]>
|
|
|
45 <script src="s6/js/jquery.microsoft.js"></script>
|
|
|
46 <![endif]-->
|
|
|
47
|
|
|
48
|
|
|
49
|
|
|
50 </head>
|
|
|
51 <body>
|
|
|
52
|
|
|
53 <div class="layout">
|
|
|
54 <div id="header"></div>
|
|
|
55 <div id="footer">
|
|
|
56 <div align="right">
|
|
|
57 <img src="s6/images/logo.svg" width="200px">
|
|
|
58 </div>
|
|
|
59 </div>
|
|
|
60 </div>
|
|
|
61
|
|
|
62 <div class="presentation">
|
|
|
63
|
|
|
64 <div class='slide cover'>
|
|
|
65 <table width="90%" height="90%" border="0" align="center">
|
|
|
66 <tr>
|
|
|
67 <td>
|
|
|
68 <div align="center">
|
|
|
69 <h1><font color="#808db5">メタ計算を用いた Continuation based C の検証手法</font></h1>
|
|
|
70 </div>
|
|
|
71 </td>
|
|
|
72 </tr>
|
|
|
73 <tr>
|
|
|
74 <td>
|
|
|
75 <div align="left">
|
|
|
76 Yasutaka Higa
|
|
|
77
|
|
|
78 <hr style="color:#ffcc00;background-color:#ffcc00;text-align:left;border:none;width:100%;height:0.2em;">
|
|
|
79 </div>
|
|
|
80 </td>
|
|
|
81 </tr>
|
|
|
82 </table>
|
|
|
83 </div>
|
|
|
84
|
|
|
85 <div class='slide '>
|
|
|
86 <!-- === begin markdown block ===
|
|
|
87
|
|
|
88 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
|
|
|
89 on 2017-02-12 18:10:22 +0900 with Markdown engine kramdown (1.13.0)
|
|
|
90 using options {}
|
|
|
91 -->
|
|
|
92
|
|
|
93 <!-- _S9SLIDE_ -->
|
|
|
94 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1>
|
|
|
95 <ul>
|
|
|
96 <li>信頼性の高いソフトウェアを提供したい</li>
|
|
|
97 <li>ソフトウェアの仕様を検証するには二つの手法がある
|
|
|
98 <ul>
|
|
|
99 <li>プログラムの持つ状態を数え上げ、仕様から外れた状態が無いかを確認するモデル検査</li>
|
|
|
100 <li>プログラムの性質を直接証明してしまう定理証明</li>
|
|
|
101 </ul>
|
|
|
102 </li>
|
|
|
103 <li>モデル検査も証明も行ないやすい言語として Continuation based C 言語を開発している</li>
|
|
|
104 </ul>
|
|
|
105
|
|
|
106
|
|
|
107 </div>
|
|
|
108 <div class='slide '>
|
|
|
109 <!-- _S9SLIDE_ -->
|
|
|
110 <h1 id="section-1">二つのアプローチを用いたソフトウェア検証</h1>
|
|
|
111 <ul>
|
|
|
112 <li>モデル検査的アプローチ
|
|
|
113 <ul>
|
|
|
114 <li>メタ計算ライブラリ akasha による網羅的な実行</li>
|
|
|
115 <li>非破壊赤黒木の仕様定義と検証</li>
|
|
|
116 </ul>
|
|
|
117 </li>
|
|
|
118 <li>定理証明的なアプローチ
|
|
|
119 <ul>
|
|
|
120 <li>依存型を持つ証明支援系言語 Agda による CbC の証明</li>
|
|
|
121 <li>部分型を利用して Agda 上に型付きの CbC の項を記述する</li>
|
|
|
122 <li>型システムを通して CbC の形式的な定義を得る</li>
|
|
|
123 <li>SingleLinkedStack の性質の証明</li>
|
|
|
124 </ul>
|
|
|
125 </li>
|
|
|
126 </ul>
|
|
|
127
|
|
|
128
|
|
|
129 </div>
|
|
|
130 <div class='slide '>
|
|
|
131 <!-- _S9SLIDE_ -->
|
|
|
132 <h1 id="continuation-based-c">Continuation based C</h1>
|
|
|
133 <ul>
|
|
|
134 <li>当研究室で開発しているプログラミング言語</li>
|
|
|
135 <li>アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語</li>
|
|
|
136 <li>OS や組み込みソフトウェアなどを対象にしている</li>
|
|
|
137 <li>CodeSegment と DataSegment という単位を用いてプログラミングする</li>
|
|
|
138 </ul>
|
|
|
139
|
|
|
140
|
|
|
141 </div>
|
|
|
142 <div class='slide '>
|
|
|
143 <!-- _S9SLIDE_ -->
|
|
|
144 <h1 id="codesegment">CodeSegment</h1>
|
|
|
145 <ul>
|
|
|
146 <li>CodeSegment とは
|
|
|
147 <ul>
|
|
|
148 <li>処理の単位</li>
|
|
|
149 <li>結合や分割が容易</li>
|
|
|
150 <li>入力と出力を持つ</li>
|
|
|
151 </ul>
|
|
|
152 </li>
|
|
|
153 <li>CodeSegment どうしを接続することによりプログラム全体を作る</li>
|
|
|
154 <li>TODO: 図</li>
|
|
|
155 </ul>
|
|
|
156
|
|
|
157
|
|
|
158 </div>
|
|
|
159 <div class='slide '>
|
|
|
160 <!-- _S9SLIDE_ -->
|
|
|
161 <h1 id="datasegment">DataSegment</h1>
|
|
|
162 <ul>
|
|
|
163 <li>DataSegment とは
|
|
|
164 <ul>
|
|
|
165 <li>データの単位</li>
|
|
|
166 <li>CodeSegment の入出力にあたる</li>
|
|
|
167 <li>接続元の Output DataSegment は接続先の Input DataSegment</li>
|
|
|
168 </ul>
|
|
|
169 </li>
|
|
|
170 <li>TODO: 図</li>
|
|
|
171 </ul>
|
|
|
172
|
|
|
173
|
|
|
174 </div>
|
|
|
175 <div class='slide '>
|
|
|
176 <!-- _S9SLIDE_ -->
|
|
|
177 <h1 id="section-2">メタ計算</h1>
|
|
|
178 <ul>
|
|
|
179 <li>とある計算を実現するための計算</li>
|
|
|
180 <li>ネットワーク接続、例外処理、メモリ確保、並列処理など</li>
|
|
|
181 <li>時に本来行ないたい処理よりも複雑になる</li>
|
|
|
182 <li>CbC は通常レベルの計算とメタ計算を分離して考える
|
|
|
183 <ul>
|
|
|
184 <li>通常レベルではポインタは出てこない、など</li>
|
|
|
185 </ul>
|
|
|
186 </li>
|
|
|
187 <li>TODO: 図</li>
|
|
|
188 </ul>
|
|
|
189
|
|
|
190
|
|
|
191 </div>
|
|
|
192 <div class='slide '>
|
|
|
193 <!-- _S9SLIDE_ -->
|
|
|
194 <h1 id="meta-codesegment">Meta CodeSegment</h1>
|
|
|
195 <ul>
|
|
|
196 <li>メタ計算を行なう CodeSegment</li>
|
|
|
197 <li>通常の CodeSegment どうしの接続の間に入る</li>
|
|
|
198 <li>TODO: 図</li>
|
|
|
199 </ul>
|
|
|
200
|
|
|
201
|
|
|
202 </div>
|
|
|
203 <div class='slide '>
|
|
|
204 <!-- _S9SLIDE_ -->
|
|
|
205 <h1 id="meta-datasegment">Meta DataSegment</h1>
|
|
|
206 <ul>
|
|
|
207 <li>メタ計算用の DataSegment</li>
|
|
|
208 <li>通常の DataSegment を含むような DataSegment</li>
|
|
|
209 <li>TODO: 図</li>
|
|
|
210 </ul>
|
|
|
211
|
|
|
212
|
|
|
213 </div>
|
|
|
214 <div class='slide '>
|
|
|
215 <!-- _S9SLIDE_ -->
|
|
|
216 <h1 id="c">C言語との対応</h1>
|
|
|
217 <ul>
|
|
|
218 <li>CodeSegment は C 言語における返り値の無い関数</li>
|
|
|
219 <li>DataSegment は C 言語における構造体</li>
|
|
|
220 <li>Meta CodeSegment は CodeSegment の前後にある CodeSegment</li>
|
|
|
221 <li>Meta DataSegment は全ての DataSegment の共用体を持つ構造体</li>
|
|
|
222 <li>CodeSegment の接続は goto における軽量継続
|
|
|
223 <ul>
|
|
|
224 <li>末尾のみで行なうスタックを保持しない関数呼び出し</li>
|
|
|
225 </ul>
|
|
|
226 </li>
|
|
|
227 </ul>
|
|
|
228
|
|
|
229
|
|
|
230 </div>
|
|
|
231 <div class='slide '>
|
|
|
232 <!-- _S9SLIDE_ -->
|
|
|
233 <h1 id="gearsos">並列に信頼性高く動作する GearsOS</h1>
|
|
|
234 <ul>
|
|
|
235 <li>CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある</li>
|
|
|
236 <li>並列実行やモデル検査をメタ計算として提供する</li>
|
|
|
237 <li>現在はメモリ管理、Synchronized Queue、非破壊赤黒木などが実装済み</li>
|
|
|
238 <li>今回はこの非破壊赤黒木の検証を行なう</li>
|
|
|
239 </ul>
|
|
|
240
|
|
|
241
|
|
|
242 </div>
|
|
|
243 <div class='slide '>
|
|
|
244 <!-- _S9SLIDE_ -->
|
|
|
245 <h1 id="section-3">赤黒木</h1>
|
|
|
246 <ul>
|
|
|
247 <li>データの保存に用いる二分木</li>
|
|
|
248 <li>特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
|
|
|
249 <ul>
|
|
|
250 <li>ルートノードと葉ノードの色は黒</li>
|
|
|
251 <li>赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)</li>
|
|
|
252 <li>ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定</li>
|
|
|
253 </ul>
|
|
|
254 </li>
|
|
|
255 <li>TODO: 図</li>
|
|
|
256 </ul>
|
|
|
257
|
|
|
258
|
|
|
259 </div>
|
|
|
260 <div class='slide '>
|
|
|
261 <!-- _S9SLIDE_ -->
|
|
|
262 <h1 id="gearsos-">GearsOS における赤黒木の利用例(ノードの挿入)</h1>
|
|
|
263 <ul>
|
|
|
264 <li>挿入したい要素を DataSegment に格納して次の CodeSegment へ goto</li>
|
|
|
265 <li>goto する前に Meta CodeSegment が実行されて木に挿入する</li>
|
|
|
266 <li>GearsOS では木の実装のためにスタックを用いて経路情報を保持している</li>
|
|
|
267 <li>TODO: 図</li>
|
|
|
268 </ul>
|
|
|
269
|
|
|
270
|
|
|
271 </div>
|
|
|
272 <div class='slide '>
|
|
|
273 <!-- _S9SLIDE_ -->
|
|
|
274 <h1 id="section-4">仕様の記述とその確認</h1>
|
|
|
275 <ul>
|
|
|
276 <li>「バランスが取れている」とは何かを表現できる必要がある
|
|
|
277 <ul>
|
|
|
278 <li>実行可能な CbC の式を使った assert になる</li>
|
|
|
279 </ul>
|
|
|
280 </li>
|
|
|
281 <li>そしてそれを保証したい
|
|
|
282 <ul>
|
|
|
283 <li>プログラムの全ての状態においてこれは常に成り立つのか?</li>
|
|
|
284 </ul>
|
|
|
285 </li>
|
|
|
286 </ul>
|
|
|
287
|
|
|
288
|
|
|
289 </div>
|
|
|
290 <div class='slide '>
|
|
|
291 <!-- _S9SLIDE_ -->
|
|
|
292 <h1 id="spin">既存のモデル検査器 spin</h1>
|
|
|
293 <ul>
|
|
|
294 <li>spin
|
|
|
295 <ul>
|
|
|
296 <li>promela と呼ばれる言語でプログラムを記述</li>
|
|
|
297 <li>並列に動作するプログラムの仕様を検証可能</li>
|
|
|
298 <li>検証した promela から実行可能な C ソースを生成可能</li>
|
|
|
299 <li>仕様は bool になる式を用いた assert</li>
|
|
|
300 <li>promela は C とは記述が異なる</li>
|
|
|
301 </ul>
|
|
|
302 </li>
|
|
|
303 </ul>
|
|
|
304
|
|
|
305
|
|
|
306 </div>
|
|
|
307 <div class='slide '>
|
|
|
308 <!-- _S9SLIDE_ -->
|
|
|
309 <h1 id="cbmc">既存のモデル検査器 CBMC</h1>
|
|
|
310 <ul>
|
|
|
311 <li>CBMC
|
|
|
312 <ul>
|
|
|
313 <li>検証対象のCソースを変更しないでも良い</li>
|
|
|
314 <li>C/C++ 言語の記号実行が可能
|
|
|
315 <ul>
|
|
|
316 <li>条件分岐を網羅的に実行</li>
|
|
|
317 </ul>
|
|
|
318 </li>
|
|
|
319 <li>仕様は bool になる式を用いた assert</li>
|
|
|
320 <li>有限ステップ検証する有界モデル検査器</li>
|
|
|
321 </ul>
|
|
|
322 </li>
|
|
|
323 </ul>
|
|
|
324
|
|
|
325
|
|
|
326 </div>
|
|
|
327 <div class='slide '>
|
|
|
328 <!-- _S9SLIDE_ -->
|
|
|
329 <h1 id="akasha">メタ計算ライブラリ akasha</h1>
|
|
|
330 <ul>
|
|
|
331 <li>メタ計算としてプログラムの状態を数え上げる</li>
|
|
|
332 <li>goto された時に挿入される要素の組み合わせを全て列挙して実行する</li>
|
|
|
333 <li>その度に仕様の式は成り立つかをチェックする</li>
|
|
|
334 <li>TODO: 図</li>
|
|
|
335 </ul>
|
|
|
336
|
|
|
337
|
|
|
338 </div>
|
|
|
339 <div class='slide '>
|
|
|
340 <!-- _S9SLIDE_ -->
|
|
|
341 <h1 id="section-5">チェックする仕様</h1>
|
|
|
342 <ul>
|
|
|
343 <li>TODO: たかさについて</li>
|
|
|
344 </ul>
|
|
|
345
|
|
|
346
|
|
|
347 </div>
|
|
|
348 <div class='slide '>
|
|
|
349 <!-- _S9SLIDE_ -->
|
|
|
350 <h1 id="akasha--cbmc-">akasha と CBMC の比較</h1>
|
|
|
351 <ul>
|
|
|
352 <li>akasha は有限の要素数の組み合わせをチェックする
|
|
|
353 <ul>
|
|
|
354 <li>要素数が13個までならどの順で木に挿入しても良い</li>
|
|
|
355 </ul>
|
|
|
356 </li>
|
|
|
357 <li>比較対象として C Bounded Model Checker を使用した
|
|
|
358 <ul>
|
|
|
359 <li>C/C++ の記号実行を行なう</li>
|
|
|
360 <li>実行可能なステップ数411だけ展開しても仕様は満たされる</li>
|
|
|
361 <li>が、恣意的にバグを入れ込んでも反例を返さない</li>
|
|
|
362 <li>akasha は返した</li>
|
|
|
363 </ul>
|
|
|
364 </li>
|
|
|
365 <li>固定の要素数までの仕様検査で十分なのか?</li>
|
|
|
366 </ul>
|
|
|
367
|
|
|
368
|
|
|
369 </div>
|
|
|
370 <div class='slide '>
|
|
|
371 <!-- _S9SLIDE_ -->
|
|
|
372 <h1 id="section-6">定理証明</h1>
|
|
|
373 <ul>
|
|
|
374 <li>任意の回数だけ木の操作を行なっても大丈夫なことを保証したい</li>
|
|
|
375 <li>そのままプログラムの性質を保証してやる</li>
|
|
|
376 <li>プログラムと証明は Curry-Howard Isomorphism により、自然演繹と型付ラムダ計算が対応
|
|
|
377 <ul>
|
|
|
378 <li>プログラムにおける命題は型であり、証明はその導出が存在するかどうか</li>
|
|
|
379 <li>例えば三段論法が書ける
|
|
|
380 <ul>
|
|
|
381 <li>(A -> B) -> (B -> C) -> (A -> C)</li>
|
|
|
382 <li>(int -> bool) -> (bool -> float) -> (int -> float)</li>
|
|
|
383 </ul>
|
|
|
384 </li>
|
|
|
385 </ul>
|
|
|
386 </li>
|
|
|
387 </ul>
|
|
|
388
|
|
|
389
|
|
|
390 </div>
|
|
|
391 <div class='slide '>
|
|
|
392 <!-- _S9SLIDE_ -->
|
|
|
393 <h1 id="agda">証明支援系 Agda</h1>
|
|
|
394 <ul>
|
|
|
395 <li>依存型を持つ言語
|
|
|
396 <ul>
|
|
|
397 <li>型が第一級(型が値である)</li>
|
|
|
398 <li>「型を取って型を返す型」などが定義可能</li>
|
|
|
399 </ul>
|
|
|
400 </li>
|
|
|
401 <li>定理証明が記述可能
|
|
|
402 <ul>
|
|
|
403 <li>この言語の上に CbC の項を表現する</li>
|
|
|
404 <li>Agda 経由で CbC の形式的な定義を得る</li>
|
|
|
405 </ul>
|
|
|
406 </li>
|
|
|
407 </ul>
|
|
|
408
|
|
|
409
|
|
|
410 </div>
|
|
|
411 <div class='slide '>
|
|
|
412 <!-- _S9SLIDE_ -->
|
|
|
413 <h1 id="agda--cbc-">Agda 上に CbC を記述するには?</h1>
|
|
|
414 <ul>
|
|
|
415 <li>CbC と CbC の対応で書ける?
|
|
|
416 <ul>
|
|
|
417 <li>DataSegment -> 構造体(複数の値と名前によって成り立つ)</li>
|
|
|
418 <li>CodeSegment -> 関数型(型を取って型を返す)</li>
|
|
|
419 <li>Meta DataSegment -> 構造体の共用体</li>
|
|
|
420 <li>Meta CodeSegment -> 関数型?</li>
|
|
|
421 </ul>
|
|
|
422 </li>
|
|
|
423 <li>Meta CodeSegment の階層構造をどう定義するか
|
|
|
424 <ul>
|
|
|
425 <li>構造体に相当するレコード型はAgdaにある</li>
|
|
|
426 <li>共用体に相当する直和型も定義可能</li>
|
|
|
427 </ul>
|
|
|
428 </li>
|
|
|
429 </ul>
|
|
|
430
|
|
|
431
|
|
|
432 </div>
|
|
|
433 <div class='slide '>
|
|
|
434 <!-- _S9SLIDE_ -->
|
|
|
435 <h1 id="section-7">メタレベルの型付け</h1>
|
|
|
436 <ul>
|
|
|
437 <li>Meta CodeSegment が持っているべき性質
|
|
|
438 <ul>
|
|
|
439 <li>メタレベルは階層構造を持つ
|
|
|
440 <ul>
|
|
|
441 <li>メタ計算は組み合わせられる</li>
|
|
|
442 </ul>
|
|
|
443 </li>
|
|
|
444 <li>ノーマルレベルの DataSegment を一様に扱える</li>
|
|
|
445 <li>ノーマルレベルの CodeSegment へと goto できる
|
|
|
446 <ul>
|
|
|
447 <li>どんなプログラムからもライブラリとして使える</li>
|
|
|
448 </ul>
|
|
|
449 </li>
|
|
|
450 </ul>
|
|
|
451 </li>
|
|
|
452 <li>構造体では融通が効かない
|
|
|
453 <ul>
|
|
|
454 <li>完全にマッチしなくてはいけない</li>
|
|
|
455 </ul>
|
|
|
456 </li>
|
|
|
457 <li>TODO: ソース</li>
|
|
|
458 </ul>
|
|
|
459
|
|
|
460
|
|
|
461 </div>
|
|
|
462 <div class='slide '>
|
|
|
463 <!-- _S9SLIDE_ -->
|
|
|
464 <h1 id="section-8">部分型</h1>
|
|
|
465 <ul>
|
|
|
466 <li>DataSegment が持つべき制約を表現できる型</li>
|
|
|
467 <li>型 T が期待される文脈で S を用いても良い、というようなことができる
|
|
|
468 <ul>
|
|
|
469 <li>「S <: T」で「S は T の部分型である」と読む</li>
|
|
|
470 <li>全てのDataSegment に対して「MDS <: DS」となるような MDS を用意する</li>
|
|
|
471 </ul>
|
|
|
472 </li>
|
|
|
473 <li>DataSegment X が期待される CodeSegment に Meta DataSegment を渡してやる</li>
|
|
|
474 </ul>
|
|
|
475
|
|
|
476
|
|
|
477 </div>
|
|
|
478 <div class='slide '>
|
|
|
479 <!-- _S9SLIDE_ -->
|
|
|
480 <h1 id="section-9">入力の部分型</h1>
|
|
|
481 <p># 出力の部分型</p>
|
|
|
482
|
|
|
483
|
|
|
484 </div>
|
|
|
485 <div class='slide '>
|
|
|
486 <!-- _S9SLIDE_ -->
|
|
|
487 <h1 id="section-10">部分型で何ができたか?</h1>
|
|
|
488 <ul>
|
|
|
489 <li>Meta CodeSegment を部分型とすることで
|
|
|
490 <ul>
|
|
|
491 <li>ノーマルレベルの CodeSegment の前後に処理を入れても型は整合する</li>
|
|
|
492 <li>Meta CodeSegment を CodeSegment とすることで階層構造を作れる</li>
|
|
|
493 </ul>
|
|
|
494 </li>
|
|
|
495 <li>Meta DataSegment を部分型とすることで
|
|
|
496 <ul>
|
|
|
497 <li>ノーマルレベルからはアクセスできないデータを保持してもOK</li>
|
|
|
498 <li>ノーマルレベルに Meta DataSegment を渡しても良い</li>
|
|
|
499 <li>こちらも階層構造を取ることができる</li>
|
|
|
500 </ul>
|
|
|
501 </li>
|
|
|
502 </ul>
|
|
|
503
|
|
|
504
|
|
|
505 </div>
|
|
|
506 <div class='slide '>
|
|
|
507 <!-- _S9SLIDE_ -->
|
|
|
508 <h1 id="singlelinkedstack-">SingleLinkedStack の証明</h1>
|
|
|
509 <ul>
|
|
|
510 <li>証明支援系 Agda に GearsOS のデータ構造 SingleLinkedStack を定義
|
|
|
511 <ul>
|
|
|
512 <li>スタックは赤黒木に用いられている</li>
|
|
|
513 </ul>
|
|
|
514 </li>
|
|
|
515 <li>その性質を証明する
|
|
|
516 <ul>
|
|
|
517 <li>性質もいくつか考えられる</li>
|
|
|
518 <li>「push して pop するとスタックは元に戻る」</li>
|
|
|
519 </ul>
|
|
|
520 </li>
|
|
|
521 </ul>
|
|
|
522
|
|
|
523
|
|
|
524 </div>
|
|
|
525 <div class='slide '>
|
|
|
526 <!-- _S9SLIDE_ -->
|
|
|
527 <h1 id="agda-">Agda を用いた証明手法</h1>
|
|
|
528 <ul>
|
|
|
529 <li>基本的にはデータの構造に関する帰納法
|
|
|
530 <ul>
|
|
|
531 <li>スタックは内部に SingleLinkedList を持つ</li>
|
|
|
532 <li>SingleLinkedList は NULL か値と次のノードを持つ</li>
|
|
|
533 <li>値がある場合と無い場合との場合分け</li>
|
|
|
534 </ul>
|
|
|
535 </li>
|
|
|
536 <li>挿入する要素を指定せずに push を呼ぶとどうなるのか?
|
|
|
537 <ul>
|
|
|
538 <li>実装依存のコード</li>
|
|
|
539 <li>証明には表れる
|
|
|
540 <ul>
|
|
|
541 <li>TODO: かく…</li>
|
|
|
542 </ul>
|
|
|
543 </li>
|
|
|
544 </ul>
|
|
|
545 </li>
|
|
|
546 </ul>
|
|
|
547
|
|
|
548
|
|
|
549 </div>
|
|
|
550 <div class='slide '>
|
|
|
551 <!-- _S9SLIDE_ -->
|
|
|
552 <h1 id="section-11">まとめ</h1>
|
|
|
553 <ul>
|
|
|
554 <li>Continuation based C 言語を対象にした二種類の検証アプローチ</li>
|
|
|
555 <li>モデル検査的なアプローチ
|
|
|
556 <ul>
|
|
|
557 <li>継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装</li>
|
|
|
558 <li>有限の要素数まで保証できた</li>
|
|
|
559 </ul>
|
|
|
560 </li>
|
|
|
561 <li>証明的なアプローチ
|
|
|
562 <ul>
|
|
|
563 <li>証明支援系 Agda 上で CbC のプログラムを定義して直接証明</li>
|
|
|
564 <li>部分型を利用して CbC を型付け</li>
|
|
|
565 <li>データ構造 SingleLinkedStack の証明ができた</li>
|
|
|
566 </ul>
|
|
|
567 </li>
|
|
|
568 </ul>
|
|
|
569
|
|
|
570
|
|
|
571 </div>
|
|
|
572 <div class='slide '>
|
|
|
573 <!-- _S9SLIDE_ -->
|
|
|
574 <h1 id="section-12">今後の課題</h1>
|
|
|
575 <ul>
|
|
|
576 <li>部分型を利用してCbCを型付け</li>
|
|
|
577 <li>依存型をCbC に導入して自身を証明可能にする</li>
|
|
|
578 <li>型情報から stub を自動生成すkる</li>
|
|
|
579 <li>赤黒木の挿入を証明する</li>
|
|
|
580 </ul>
|
|
|
581
|
|
|
582 <!-- vim: set filetype=markdown.slide: -->
|
|
|
583
|
|
|
584 <!-- === end markdown block === -->
|
|
|
585 </div>
|
|
|
586
|
|
|
587
|
|
|
588 </div><!-- presentation -->
|
|
|
589 </body>
|
|
|
590 </html>
|
