--- a/presentation/slide.html	Mon Feb 13 17:39:10 2017 +0900
+++ b/presentation/slide.html	Mon Feb 13 17:41:26 2017 +0900
@@ -86,7 +86,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
-                on 2017-02-13 17:33:22 +0900 with Markdown engine kramdown (1.13.0)
+                on 2017-02-13 17:40:39 +0900 with Markdown engine kramdown (1.13.0)
                   using options {}
   -->
 
@@ -111,7 +111,7 @@
 <ul>
   <li>モデル検査的アプローチ
     <ul>
-      <li>メタ計算ライブラリ akasha による網羅的な実行</li>
+      <li>メタ計算ライブラリ akasha による CbC の網羅的な実行</li>
       <li>非破壊赤黒木の仕様定義と検証</li>
     </ul>
   </li>
@@ -301,7 +301,7 @@
       <li>並列に動作するプログラムの仕様を検証可能</li>
       <li>検証した promela から実行可能な C ソースを生成可能</li>
       <li>仕様は bool になる式を用いた assert</li>
-      <li>promela は C とは記述が異なる</li>
+      <li>デメリット: promela は C とは記述が異なる</li>
     </ul>
   </li>
 </ul>
@@ -349,7 +349,7 @@
 <!-- _S9SLIDE_ -->
 <h1 id="section-6">チェックする仕様</h1>
 <ul>
-  <li>赤黒木のの高さに関する仕様に以下のものがある
+  <li>赤黒木の高さに関する仕様に以下のものがある
     <ul>
       <li>木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる</li>
     </ul>
@@ -358,10 +358,15 @@
   <li>この仕様が満たされるかをチェックする</li>
 </ul>
 
-<pre><code>void verifySpecification(struct Context* context, struct Tree* tree) {
-    assert(!(maxHeight(tree-&gt;root, 1) &gt; 2*minHeight(tree-&gt;root, 1)));
-        goto meta(context, EnumerateInputs);
+<pre><code>__code verifySpecificationFinish(struct Context* context) {
+    if (context-&gt;data[AkashaInfo]-&gt;akashaInfo.maxHeight &gt;
+        2*context-&gt;data[AkashaInfo]-&gt;akashaInfo.minHeight)
+    {
+        context-&gt;next = Exit;
+        goto meta(context, ShowTrace);
     }
+    goto meta(context, DuplicateIterator);
+}
 </code></pre>