Mercurial > hg > Papers > 2018 > nozomi-master

comparison presentation/slide.pdf.html @ 119:26563097333c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update slide
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 13 Feb 2017 17:41:26 +0900
parents 1a9c04ea28fb
children 8a84cda440f3
comparison
equal deleted inserted replaced
118:05068a4d0b52 119:26563097333c
68 68
69 <div class='slide '> 69 <div class='slide '>
70 <!-- === begin markdown block === 70 <!-- === begin markdown block ===
71 71
72 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16] 72 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
73 on 2017-02-13 17:33:22 +0900 with Markdown engine kramdown (1.13.0) 73 on 2017-02-13 17:40:39 +0900 with Markdown engine kramdown (1.13.0)
74 using options {} 74 using options {}
75 --> 75 -->
76 76
77 <!-- _S9SLIDE_ --> 77 <!-- _S9SLIDE_ -->
78 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1> 78 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1>
93 <!-- _S9SLIDE_ --> 93 <!-- _S9SLIDE_ -->
94 <h1 id="section-1">二つのアプローチを用いたソフトウェア検証</h1> 94 <h1 id="section-1">二つのアプローチを用いたソフトウェア検証</h1>
95 <ul> 95 <ul>
96 <li>モデル検査的アプローチ 96 <li>モデル検査的アプローチ
97 <ul> 97 <ul>
98 <li>メタ計算ライブラリ akasha による網羅的な実行</li> 98 <li>メタ計算ライブラリ akasha による CbC の網羅的な実行</li>
99 <li>非破壊赤黒木の仕様定義と検証</li> 99 <li>非破壊赤黒木の仕様定義と検証</li>
100 </ul> 100 </ul>
101 </li> 101 </li>
102 <li>定理証明的なアプローチ 102 <li>定理証明的なアプローチ
103 <ul> 103 <ul>
283 <ul> 283 <ul>
284 <li>promela と呼ばれる言語でプログラムを記述</li> 284 <li>promela と呼ばれる言語でプログラムを記述</li>
285 <li>並列に動作するプログラムの仕様を検証可能</li> 285 <li>並列に動作するプログラムの仕様を検証可能</li>
286 <li>検証した promela から実行可能な C ソースを生成可能</li> 286 <li>検証した promela から実行可能な C ソースを生成可能</li>
287 <li>仕様は bool になる式を用いた assert</li> 287 <li>仕様は bool になる式を用いた assert</li>
288 <li>promela は C とは記述が異なる</li> 288 <li>デメリット: promela は C とは記述が異なる</li>
289 </ul> 289 </ul>
290 </li> 290 </li>
291 </ul> 291 </ul>
292 292
293 293
331 </div> 331 </div>
332 <div class='slide '> 332 <div class='slide '>
333 <!-- _S9SLIDE_ --> 333 <!-- _S9SLIDE_ -->
334 <h1 id="section-6">チェックする仕様</h1> 334 <h1 id="section-6">チェックする仕様</h1>
335 <ul> 335 <ul>
336 <li>赤黒木のの高さに関する仕様に以下のものがある 336 <li>赤黒木の高さに関する仕様に以下のものがある
337 <ul> 337 <ul>
338 <li>木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる</li> 338 <li>木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる</li>
339 </ul> 339 </ul>
340 </li> 340 </li>
341 <li>以下のように assert を用いて CbC で定義できる</li> 341 <li>以下のように assert を用いて CbC で定義できる</li>
342 <li>この仕様が満たされるかをチェックする</li> 342 <li>この仕様が満たされるかをチェックする</li>
343 </ul> 343 </ul>
344 344
345 <pre><code>void verifySpecification(struct Context* context, struct Tree* tree) { 345 <pre><code>__code verifySpecificationFinish(struct Context* context) {
346 assert(!(maxHeight(tree-&gt;root, 1) &gt; 2*minHeight(tree-&gt;root, 1))); 346 if (context-&gt;data[AkashaInfo]-&gt;akashaInfo.maxHeight &gt;
347 goto meta(context, EnumerateInputs); 347 2*context-&gt;data[AkashaInfo]-&gt;akashaInfo.minHeight)
348 {
349 context-&gt;next = Exit;
350 goto meta(context, ShowTrace);
348 } 351 }
352 goto meta(context, DuplicateIterator);
353 }
349 </code></pre> 354 </code></pre>
350 355
351 356
352 </div> 357 </div>
353 <div class='slide '> 358 <div class='slide '>