--- a/presentation/slide.html	Mon Feb 13 17:41:26 2017 +0900
+++ b/presentation/slide.html	Tue Feb 14 11:31:08 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:40:39 +0900 with Markdown engine kramdown (1.13.0)
+                on 2017-02-14 11:30:47 +0900 with Markdown engine kramdown (1.13.0)
                   using options {}
   -->
 
@@ -129,7 +129,22 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-2">モデル検査的アプローチについての流れ</h1>
+<h1 id="section-2">本発表ではモデル検査的アプローチについて中心に見ていきます</h1>
+<ul>
+  <li>修士論文の内部の比率は半分半分くらい</li>
+  <li>定理証明の方は説明する内容が多くて複雑</li>
+  <li>モデル検査的アプローチは過去論文を提出したもの
+    <ul>
+      <li>なのでそちらをメインで発表します</li>
+    </ul>
+  </li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-3">モデル検査的アプローチについての流れ</h1>
 <ul>
   <li>Continuation based C (CbC) 言語について</li>
   <li>CbC における CodeSegment と DataSegment を用いたプログラミングスタイル</li>
@@ -159,16 +174,24 @@
 <ul>
   <li>CodeSegment とは
     <ul>
-      <li>処理の単位</li>
+      <li>処理の単位であり、入力と出力を持つ</li>
       <li>結合や分割が容易</li>
-      <li>入力と出力を持つ</li>
     </ul>
   </li>
-  <li>CodeSegment どうしを接続することによりプログラム全体を作る</li>
+  <li>CodeSegment どうしを接続することによりプログラム全体を作る
+    <ul>
+      <li>関数呼び出しと違って戻ってこない(goto)</li>
+    </ul>
+  </li>
 </ul>
 
 <p><img src="./images/cs.svg" alt="cs" width="50%" /></p>
 
+<pre><code>__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+</code></pre>
+
 
 </div>
 <div class='slide '>
@@ -186,11 +209,16 @@
 
 <p><img src="./images/ds.svg" alt="ds" width="50%" /></p>
 
+<pre><code>__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+</code></pre>
+
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-3">メタ計算</h1>
+<h1 id="section-4">メタ計算</h1>
 <ul>
   <li>とある計算を実現するための計算</li>
   <li>ネットワーク接続、例外処理、メモリ確保、並列処理など</li>
@@ -244,7 +272,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-4">赤黒木</h1>
+<h1 id="section-5">赤黒木</h1>
 <ul>
   <li>データの保存に用いる二分木</li>
   <li>特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
@@ -256,7 +284,7 @@
   </li>
 </ul>
 
-<p><img src="./images/rbtree.svg" alt="rbtree" width="50%" /></p>
+<p><img src="./images/rbtree.svg" alt="rbtree" width="35%" /></p>
 
 
 </div>
@@ -271,11 +299,14 @@
 
 <p><img src="./images/put.svg" alt="put" width="50%" /></p>
 
+<pre><code>goto meta(context, Put);
+</code></pre>
+
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-5">仕様の記述とその確認</h1>
+<h1 id="section-6">仕様の記述とその確認</h1>
 <ul>
   <li>「バランスが取れている」とは何かを表現できる必要がある
     <ul>
@@ -306,6 +337,9 @@
   </li>
 </ul>
 
+<pre><code>assert(x &lt; 10);
+</code></pre>
+
 
 </div>
 <div class='slide '>
@@ -326,36 +360,21 @@
   </li>
 </ul>
 
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="akasha">メタ計算ライブラリ akasha</h1>
-<ul>
-  <li>メタ計算としてプログラムの状態を数え上げる
-    <ul>
-      <li>goto された時に挿入される要素の組み合わせを全て列挙して実行する</li>
-      <li>その度に仕様の式は成り立つかをチェックする</li>
-    </ul>
-  </li>
-  <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
-</ul>
-
-<p><img src="./images/akashaPut.svg" alt="akashaPut" width="51%" /></p>
+<pre><code>assert(x &lt; 10);
+</code></pre>
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-6">チェックする仕様</h1>
+<h1 id="section-7">チェックする仕様</h1>
 <ul>
   <li>赤黒木の高さに関する仕様に以下のものがある
     <ul>
       <li>木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる</li>
     </ul>
   </li>
-  <li>以下のように assert を用いて CbC で定義できる</li>
-  <li>この仕様が満たされるかをチェックする</li>
+  <li>以下のような条件式を仕様として CbC で定義、検証できる</li>
 </ul>
 
 <pre><code>__code verifySpecificationFinish(struct Context* context) {
@@ -373,6 +392,27 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="akasha">メタ計算ライブラリ akasha</h1>
+<ul>
+  <li>メタ計算としてプログラムの状態を数え上げる
+    <ul>
+      <li>goto された時に挿入される要素の組み合わせを全て列挙して実行する
+        <ul>
+          <li>赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……</li>
+        </ul>
+      </li>
+      <li>その度に仕様の式は成り立つかをチェックする</li>
+    </ul>
+  </li>
+  <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
+</ul>
+
+<p><img src="./images/akashaPut.svg" alt="akashaPut" width="51%" /></p>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="akasha--cbmc-">akasha と CBMC の比較</h1>
 <ul>
   <li>akasha は有限の要素数の組み合わせをチェックする
@@ -395,18 +435,6 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-7">定理証明的なアプローチの流れ</h1>
-<ul>
-  <li>プログラムを証明するにはどうするのか</li>
-  <li>証明支援系 Agda における証明</li>
-  <li>Agda による CbC の定義</li>
-  <li>Agda を用いて CbC のコードを証明する</li>
-</ul>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
 <h1 id="continuation-based-c-">定理証明を Continuation based C へ適用するには</h1>
 <ul>
   <li>任意の回数だけ木の操作を行なっても大丈夫なことを保証したい</li>
@@ -475,7 +503,7 @@
   <li>部分型を使う
     <ul>
       <li>Java におけるインターフェース、Haskell における型クラス</li>
-      <li>「このデータにはこのフィールドさえあれば良い」</li>
+      <li>「このフィールドXがあればデータ型Tとみなして良い」</li>
     </ul>
   </li>
 </ul>
@@ -493,11 +521,16 @@
   </li>
 </ul>
 
+<pre><code>cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -&gt; goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+</code></pre>
+
 <pre><code>main : ds1
 main = goto cs0 (record {a = 100 ; b = 50})
 </code></pre>
 <pre><code>main : Meta
-main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
+main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70})
+                                 ; c' = 0 ; next = (N.cs id)})
 </code></pre>
 
 
@@ -553,6 +586,30 @@
   <li>赤黒木の挿入に関する性質を証明する</li>
 </ul>
 
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-11">発表履歴</h1>
+<ul>
+  <li>Agda 入門.
+    <ul>
+      <li>オープンソースカンファレンス 2014 Okinawa, May 2014.</li>
+    </ul>
+  </li>
+  <li>形式手法を学び始めて思うことと、形式手法を広めるには(2p).
+    <ul>
+      <li>情報処理学会ソフトウェア工学研究会 (IPSJ SIGSE) ウィンターワークショップ 2015・ イン・宜野湾 (WWS2015), Jan 2015.</li>
+    </ul>
+  </li>
+  <li>Continuation based C を用いたプログラムの検証手法(6p).
+    <ul>
+      <li>2016 年並列/分散/協調処理に関する『松本』サマー・ワークショップ (SWoPP2016)</li>
+      <li>情報処理学会・プログラミング研究会 第 110 回プログラミング研究会 (PRO-2016-2) Aug 2016.</li>
+    </ul>
+  </li>
+</ul>
+
 <!-- vim: set filetype=markdown.slide: -->
 
 <!-- === end markdown block === -->