Mercurial > hg > Papers > 2017 > atton-master

changeset 121:137aae675a94

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 Tue, 14 Feb 2017 15:03:04 +0900
parents 8a84cda440f3
children c195713cf7d7
files presentation/slide.html presentation/slide.md presentation/slide.pdf.html
diffstat 3 files changed, 171 insertions(+), 141 deletions(-) [+]
line wrap: on
line diff
--- a/presentation/slide.html	Tue Feb 14 11:31:08 2017 +0900
+++ b/presentation/slide.html	Tue Feb 14 15:03:04 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-14 11:30:47 +0900 with Markdown engine kramdown (1.13.0)
+                on 2017-02-14 15:02:42 +0900 with Markdown engine kramdown (1.13.0)
                   using options {}
   -->
 
@@ -146,6 +146,7 @@
 <!-- _S9SLIDE_ -->
 <h1 id="section-3">モデル検査的アプローチについての流れ</h1>
 <ul>
+  <li>既存のモデル検査器について</li>
   <li>Continuation based C (CbC) 言語について</li>
   <li>CbC における CodeSegment と DataSegment を用いたプログラミングスタイル</li>
   <li>CbC とメタ計算について</li>
@@ -157,13 +158,60 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="spin">既存のモデル検査器 spin</h1>
+<ul>
+  <li>spin
+    <ul>
+      <li>promela と呼ばれる言語でプログラムを記述</li>
+      <li>並列に動作するプログラムの仕様を検証可能</li>
+      <li>検証した promela から実行可能な C ソースを生成可能</li>
+      <li>仕様は bool になる式を用いた assert</li>
+      <li>デメリット: promela は C とは記述が異なる</li>
+    </ul>
+  </li>
+</ul>
+
+<pre><code>assert(x &lt; 10);
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="cbmc">既存のモデル検査器 CBMC</h1>
+<ul>
+  <li>CBMC
+    <ul>
+      <li>検証対象のCソースを変更しないでも良い</li>
+      <li>C/C++ 言語の記号実行が可能
+        <ul>
+          <li>条件分岐を網羅的に実行</li>
+        </ul>
+      </li>
+      <li>仕様は bool になる式を用いた assert</li>
+      <li>有限ステップだけ検証する有界モデル検査器</li>
+    </ul>
+  </li>
+</ul>
+
+<pre><code>assert(x &lt; 10);
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="continuation-based-c">Continuation based C</h1>
 <ul>
   <li>当研究室で開発しているプログラミング言語</li>
   <li>アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語</li>
   <li>OS や組み込みソフトウェアなどを対象にしている</li>
   <li>CodeSegment と DataSegment という単位を用いてプログラミングする</li>
-  <li>両検証手法をメタ計算として利用可能</li>
+  <li>モデル検査と証明の両検証手法をメタ計算として利用可能
+    <ul>
+      <li>CbC で CbC 自身を検証可能</li>
+    </ul>
+  </li>
 </ul>
 
 
@@ -242,7 +290,7 @@
   <li>通常の CodeSegment どうしの接続の間に入る</li>
 </ul>
 
-<p><img src="./images/mcs.svg" alt="mcs" width="50%" /></p>
+<p><img src="./images/mcs.svg" alt="mcs" width="75%" /></p>
 
 
 </div>
@@ -254,7 +302,7 @@
   <li>通常の DataSegment を含むような DataSegment</li>
 </ul>
 
-<p><img src="./images/mds.svg" alt="mds" width="50%" /></p>
+<p><img src="./images/mds.svg" alt="mds" width="75%" /></p>
 
 
 </div>
@@ -294,7 +342,6 @@
 <ul>
   <li>挿入したい要素を DataSegment に格納して次の CodeSegment へ goto</li>
   <li>goto する前に Meta CodeSegment が実行されて木に挿入する</li>
-  <li>GearsOS では木の実装のためにスタックを用いて経路情報を保持している</li>
 </ul>
 
 <p><img src="./images/put.svg" alt="put" width="50%" /></p>
@@ -310,7 +357,7 @@
 <ul>
   <li>「バランスが取れている」とは何かを表現できる必要がある
     <ul>
-      <li>実行可能な CbC の式を使った assert になる</li>
+      <li>実行可能な CbC の条件式を使った assert になる</li>
     </ul>
   </li>
   <li>そしてそれを保証したい
@@ -324,49 +371,6 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="spin">既存のモデル検査器 spin</h1>
-<ul>
-  <li>spin
-    <ul>
-      <li>promela と呼ばれる言語でプログラムを記述</li>
-      <li>並列に動作するプログラムの仕様を検証可能</li>
-      <li>検証した promela から実行可能な C ソースを生成可能</li>
-      <li>仕様は bool になる式を用いた assert</li>
-      <li>デメリット: promela は C とは記述が異なる</li>
-    </ul>
-  </li>
-</ul>
-
-<pre><code>assert(x &lt; 10);
-</code></pre>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="cbmc">既存のモデル検査器 CBMC</h1>
-<ul>
-  <li>CBMC
-    <ul>
-      <li>検証対象のCソースを変更しないでも良い</li>
-      <li>C/C++ 言語の記号実行が可能
-        <ul>
-          <li>条件分岐を網羅的に実行</li>
-        </ul>
-      </li>
-      <li>仕様は bool になる式を用いた assert</li>
-      <li>有限ステップ検証する有界モデル検査器</li>
-    </ul>
-  </li>
-</ul>
-
-<pre><code>assert(x &lt; 10);
-</code></pre>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
 <h1 id="section-7">チェックする仕様</h1>
 <ul>
   <li>赤黒木の高さに関する仕様に以下のものがある
@@ -407,7 +411,7 @@
   <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
 </ul>
 
-<p><img src="./images/akashaPut.svg" alt="akashaPut" width="51%" /></p>
+<p><img src="./images/akashaPut.svg" alt="akashaPut" width="50%" /></p>
 
 
 </div>
@@ -438,7 +442,7 @@
 <h1 id="continuation-based-c-">定理証明を Continuation based C へ適用するには</h1>
 <ul>
   <li>任意の回数だけ木の操作を行なっても大丈夫なことを保証したい</li>
-  <li>そのままプログラムの性質を保証してやる</li>
+  <li>直接プログラムの性質を証明</li>
   <li>Coq, Agda, ATS2 などのプログラミング言語で証明が可能
     <ul>
       <li>本当は CbC で CbC 自身を証明したい</li>
@@ -454,7 +458,11 @@
 <!-- _S9SLIDE_ -->
 <h1 id="agda--datasegment">Agda と DataSegment</h1>
 <ul>
-  <li>CbC の DataSegment は Agda のレコード型</li>
+  <li>CbC の DataSegment は Agda のレコード型
+    <ul>
+      <li>名前付きの値が複数ある(C の構造体)</li>
+    </ul>
+  </li>
 </ul>
 
 <pre><code>__code cs0(int a, int b){
@@ -473,7 +481,11 @@
 <!-- _S9SLIDE_ -->
 <h1 id="agda--codesegment">Agda と CodeSegment</h1>
 <ul>
-  <li>CbC の CodeSegment は、Agda の関数型(Input を取って Output を返す)</li>
+  <li>CbC の CodeSegment は、Agda の関数型
+    <ul>
+      <li>Input を取って Output を返す</li>
+    </ul>
+  </li>
 </ul>
 
 <pre><code>__code cs0(int a, int b){
@@ -580,10 +592,11 @@
 <!-- _S9SLIDE_ -->
 <h1 id="section-10">今後の課題</h1>
 <ul>
+  <li>より大きなサイズの赤黒木の検証</li>
+  <li>赤黒木の挿入に関する性質を証明する</li>
   <li>部分型を利用してCbCを型付け</li>
   <li>依存型をCbC に導入して自身を証明可能にする</li>
   <li>型情報から stub を自動生成すkる</li>
-  <li>赤黒木の挿入に関する性質を証明する</li>
 </ul>
 
 
--- a/presentation/slide.md	Tue Feb 14 11:31:08 2017 +0900
+++ b/presentation/slide.md	Tue Feb 14 15:03:04 2017 +0900
@@ -28,18 +28,44 @@
     *  なのでそちらをメインで発表します
 
 # モデル検査的アプローチについての流れ
+* 既存のモデル検査器について
 * Continuation based C (CbC) 言語について
 * CbC における CodeSegment と DataSegment を用いたプログラミングスタイル
 * CbC とメタ計算について
 * CbC で記述された GearsOS とそのデータ構造である赤黒木
 * 赤黒木の仕様の定義とその検証手法
 
+# 既存のモデル検査器 spin
+* spin
+    * promela と呼ばれる言語でプログラムを記述
+    * 並列に動作するプログラムの仕様を検証可能
+    * 検証した promela から実行可能な C ソースを生成可能
+    * 仕様は bool になる式を用いた assert
+    * デメリット: promela は C とは記述が異なる
+
+```
+assert(x < 10);
+```
+
+# 既存のモデル検査器 CBMC
+* CBMC
+    * 検証対象のCソースを変更しないでも良い
+    * C/C++ 言語の記号実行が可能
+        * 条件分岐を網羅的に実行
+    * 仕様は bool になる式を用いた assert
+    * 有限ステップだけ検証する有界モデル検査器
+
+```
+assert(x < 10);
+```
+
 # Continuation based C
 * 当研究室で開発しているプログラミング言語
 * アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語
 * OS や組み込みソフトウェアなどを対象にしている
 * CodeSegment と DataSegment という単位を用いてプログラミングする
-* 両検証手法をメタ計算として利用可能
+* モデル検査と証明の両検証手法をメタ計算として利用可能
+    * CbC で CbC 自身を検証可能
 
 # CodeSegment
 * CodeSegment とは
@@ -84,13 +110,13 @@
 * メタ計算を行なう CodeSegment
 * 通常の CodeSegment どうしの接続の間に入る
 
-![mcs](./images/mcs.svg){:width="50%"}
+![mcs](./images/mcs.svg){:width="75%"}
 
 # Meta DataSegment
 * メタ計算用の DataSegment
 * 通常の DataSegment を含むような DataSegment
 
-![mds](./images/mds.svg){:width="50%"}
+![mds](./images/mds.svg){:width="75%"}
 
 # 並列に信頼性高く動作する GearsOS
 * CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある
@@ -110,7 +136,6 @@
 # GearsOS における赤黒木の利用例(ノードの挿入)
 * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto
 * goto する前に Meta CodeSegment が実行されて木に挿入する
-* GearsOS では木の実装のためにスタックを用いて経路情報を保持している
 
 
 ![put](./images/put.svg){:width="50%"}
@@ -121,34 +146,10 @@
 
 # 仕様の記述とその確認
 * 「バランスが取れている」とは何かを表現できる必要がある
-    * 実行可能な CbC の式を使った assert になる
+    * 実行可能な CbC の条件式を使った assert になる
 * そしてそれを保証したい
     * プログラムの全ての状態においてこれは常に成り立つのか?
 
-# 既存のモデル検査器 spin
-* spin
-    * promela と呼ばれる言語でプログラムを記述
-    * 並列に動作するプログラムの仕様を検証可能
-    * 検証した promela から実行可能な C ソースを生成可能
-    * 仕様は bool になる式を用いた assert
-    * デメリット: promela は C とは記述が異なる
-
-```
-assert(x < 10);
-```
-
-# 既存のモデル検査器 CBMC
-* CBMC
-    * 検証対象のCソースを変更しないでも良い
-    * C/C++ 言語の記号実行が可能
-        * 条件分岐を網羅的に実行
-    * 仕様は bool になる式を用いた assert
-    * 有限ステップ検証する有界モデル検査器
-
-```
-assert(x < 10);
-```
-
 # チェックする仕様
 * 赤黒木の高さに関する仕様に以下のものがある
     * 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
@@ -173,7 +174,7 @@
     * その度に仕様の式は成り立つかをチェックする
 * ノーマルレベルのコードを検証用に変更せず検証可能
 
-![akashaPut](./images/akashaPut.svg){:width="51%"}
+![akashaPut](./images/akashaPut.svg){:width="50%"}
 
 # akasha と CBMC の比較
 * akasha は有限の要素数の組み合わせをチェックする
@@ -187,7 +188,7 @@
 
 # 定理証明を Continuation based C へ適用するには
 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
-* そのままプログラムの性質を保証してやる
+* 直接プログラムの性質を証明
 * Coq, Agda, ATS2 などのプログラミング言語で証明が可能
     * 本当は CbC で CbC 自身を証明したい
     * しかし CbC の形式的な定義が無いために今はできない
@@ -195,6 +196,7 @@
 
 # Agda と DataSegment
 * CbC の DataSegment は Agda のレコード型
+    * 名前付きの値が複数ある(C の構造体)
 
 ```
 __code cs0(int a, int b){
@@ -209,7 +211,8 @@
 ```
 
 # Agda と CodeSegment
-* CbC の CodeSegment は、Agda の関数型(Input を取って Output を返す)
+* CbC の CodeSegment は、Agda の関数型
+    * Input を取って Output を返す
 
 ```
 __code cs0(int a, int b){
@@ -270,10 +273,11 @@
     * データ構造 SingleLinkedStack の証明ができた
 
 # 今後の課題
+* より大きなサイズの赤黒木の検証
+* 赤黒木の挿入に関する性質を証明する
 * 部分型を利用してCbCを型付け
 * 依存型をCbC に導入して自身を証明可能にする
 * 型情報から stub を自動生成すkる
-* 赤黒木の挿入に関する性質を証明する
 
 # 発表履歴
 * Agda 入門.
--- a/presentation/slide.pdf.html	Tue Feb 14 11:31:08 2017 +0900
+++ b/presentation/slide.pdf.html	Tue Feb 14 15:03:04 2017 +0900
@@ -70,7 +70,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
-                on 2017-02-14 11:30:47 +0900 with Markdown engine kramdown (1.13.0)
+                on 2017-02-14 15:02:42 +0900 with Markdown engine kramdown (1.13.0)
                   using options {}
   -->
 
@@ -130,6 +130,7 @@
 <!-- _S9SLIDE_ -->
 <h1 id="section-3">モデル検査的アプローチについての流れ</h1>
 <ul>
+  <li>既存のモデル検査器について</li>
   <li>Continuation based C (CbC) 言語について</li>
   <li>CbC における CodeSegment と DataSegment を用いたプログラミングスタイル</li>
   <li>CbC とメタ計算について</li>
@@ -141,13 +142,60 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="spin">既存のモデル検査器 spin</h1>
+<ul>
+  <li>spin
+    <ul>
+      <li>promela と呼ばれる言語でプログラムを記述</li>
+      <li>並列に動作するプログラムの仕様を検証可能</li>
+      <li>検証した promela から実行可能な C ソースを生成可能</li>
+      <li>仕様は bool になる式を用いた assert</li>
+      <li>デメリット: promela は C とは記述が異なる</li>
+    </ul>
+  </li>
+</ul>
+
+<pre><code>assert(x &lt; 10);
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="cbmc">既存のモデル検査器 CBMC</h1>
+<ul>
+  <li>CBMC
+    <ul>
+      <li>検証対象のCソースを変更しないでも良い</li>
+      <li>C/C++ 言語の記号実行が可能
+        <ul>
+          <li>条件分岐を網羅的に実行</li>
+        </ul>
+      </li>
+      <li>仕様は bool になる式を用いた assert</li>
+      <li>有限ステップだけ検証する有界モデル検査器</li>
+    </ul>
+  </li>
+</ul>
+
+<pre><code>assert(x &lt; 10);
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="continuation-based-c">Continuation based C</h1>
 <ul>
   <li>当研究室で開発しているプログラミング言語</li>
   <li>アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語</li>
   <li>OS や組み込みソフトウェアなどを対象にしている</li>
   <li>CodeSegment と DataSegment という単位を用いてプログラミングする</li>
-  <li>両検証手法をメタ計算として利用可能</li>
+  <li>モデル検査と証明の両検証手法をメタ計算として利用可能
+    <ul>
+      <li>CbC で CbC 自身を検証可能</li>
+    </ul>
+  </li>
 </ul>
 
 
@@ -226,7 +274,7 @@
   <li>通常の CodeSegment どうしの接続の間に入る</li>
 </ul>
 
-<p><img src="./images/mcs.svg" alt="mcs" width="50%" /></p>
+<p><img src="./images/mcs.svg" alt="mcs" width="75%" /></p>
 
 
 </div>
@@ -238,7 +286,7 @@
   <li>通常の DataSegment を含むような DataSegment</li>
 </ul>
 
-<p><img src="./images/mds.svg" alt="mds" width="50%" /></p>
+<p><img src="./images/mds.svg" alt="mds" width="75%" /></p>
 
 
 </div>
@@ -278,7 +326,6 @@
 <ul>
   <li>挿入したい要素を DataSegment に格納して次の CodeSegment へ goto</li>
   <li>goto する前に Meta CodeSegment が実行されて木に挿入する</li>
-  <li>GearsOS では木の実装のためにスタックを用いて経路情報を保持している</li>
 </ul>
 
 <p><img src="./images/put.svg" alt="put" width="50%" /></p>
@@ -294,7 +341,7 @@
 <ul>
   <li>「バランスが取れている」とは何かを表現できる必要がある
     <ul>
-      <li>実行可能な CbC の式を使った assert になる</li>
+      <li>実行可能な CbC の条件式を使った assert になる</li>
     </ul>
   </li>
   <li>そしてそれを保証したい
@@ -308,49 +355,6 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="spin">既存のモデル検査器 spin</h1>
-<ul>
-  <li>spin
-    <ul>
-      <li>promela と呼ばれる言語でプログラムを記述</li>
-      <li>並列に動作するプログラムの仕様を検証可能</li>
-      <li>検証した promela から実行可能な C ソースを生成可能</li>
-      <li>仕様は bool になる式を用いた assert</li>
-      <li>デメリット: promela は C とは記述が異なる</li>
-    </ul>
-  </li>
-</ul>
-
-<pre><code>assert(x &lt; 10);
-</code></pre>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="cbmc">既存のモデル検査器 CBMC</h1>
-<ul>
-  <li>CBMC
-    <ul>
-      <li>検証対象のCソースを変更しないでも良い</li>
-      <li>C/C++ 言語の記号実行が可能
-        <ul>
-          <li>条件分岐を網羅的に実行</li>
-        </ul>
-      </li>
-      <li>仕様は bool になる式を用いた assert</li>
-      <li>有限ステップ検証する有界モデル検査器</li>
-    </ul>
-  </li>
-</ul>
-
-<pre><code>assert(x &lt; 10);
-</code></pre>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
 <h1 id="section-7">チェックする仕様</h1>
 <ul>
   <li>赤黒木の高さに関する仕様に以下のものがある
@@ -391,7 +395,7 @@
   <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
 </ul>
 
-<p><img src="./images/akashaPut.svg" alt="akashaPut" width="51%" /></p>
+<p><img src="./images/akashaPut.svg" alt="akashaPut" width="50%" /></p>
 
 
 </div>
@@ -422,7 +426,7 @@
 <h1 id="continuation-based-c-">定理証明を Continuation based C へ適用するには</h1>
 <ul>
   <li>任意の回数だけ木の操作を行なっても大丈夫なことを保証したい</li>
-  <li>そのままプログラムの性質を保証してやる</li>
+  <li>直接プログラムの性質を証明</li>
   <li>Coq, Agda, ATS2 などのプログラミング言語で証明が可能
     <ul>
       <li>本当は CbC で CbC 自身を証明したい</li>
@@ -438,7 +442,11 @@
 <!-- _S9SLIDE_ -->
 <h1 id="agda--datasegment">Agda と DataSegment</h1>
 <ul>
-  <li>CbC の DataSegment は Agda のレコード型</li>
+  <li>CbC の DataSegment は Agda のレコード型
+    <ul>
+      <li>名前付きの値が複数ある(C の構造体)</li>
+    </ul>
+  </li>
 </ul>
 
 <pre><code>__code cs0(int a, int b){
@@ -457,7 +465,11 @@
 <!-- _S9SLIDE_ -->
 <h1 id="agda--codesegment">Agda と CodeSegment</h1>
 <ul>
-  <li>CbC の CodeSegment は、Agda の関数型(Input を取って Output を返す)</li>
+  <li>CbC の CodeSegment は、Agda の関数型
+    <ul>
+      <li>Input を取って Output を返す</li>
+    </ul>
+  </li>
 </ul>
 
 <pre><code>__code cs0(int a, int b){
@@ -564,10 +576,11 @@
 <!-- _S9SLIDE_ -->
 <h1 id="section-10">今後の課題</h1>
 <ul>
+  <li>より大きなサイズの赤黒木の検証</li>
+  <li>赤黒木の挿入に関する性質を証明する</li>
   <li>部分型を利用してCbCを型付け</li>
   <li>依存型をCbC に導入して自身を証明可能にする</li>
   <li>型情報から stub を自動生成すkる</li>
-  <li>赤黒木の挿入に関する性質を証明する</li>
 </ul>