Mercurial > hg > Papers > 2017 > atton-master

changeset 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 05068a4d0b52
children 8a84cda440f3
files presentation/slide.html presentation/slide.md presentation/slide.pdf.html
diffstat 3 files changed, 35 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- 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>
 
 
--- a/presentation/slide.md	Mon Feb 13 17:39:10 2017 +0900
+++ b/presentation/slide.md	Mon Feb 13 17:41:26 2017 +0900
@@ -13,7 +13,7 @@
 
 # 二つのアプローチを用いたソフトウェア検証
 * モデル検査的アプローチ
-    * メタ計算ライブラリ akasha による網羅的な実行
+    * メタ計算ライブラリ akasha による CbC の網羅的な実行
     * 非破壊赤黒木の仕様定義と検証
 * 定理証明的なアプローチ
     * 依存型を持つ証明支援系言語 Agda による CbC の証明
@@ -108,7 +108,7 @@
     * 並列に動作するプログラムの仕様を検証可能
     * 検証した promela から実行可能な C ソースを生成可能
     * 仕様は bool になる式を用いた assert
-    * promela は C とは記述が異なる
+    * デメリット: promela は C とは記述が異なる
 
 # 既存のモデル検査器 CBMC
 * CBMC
@@ -127,16 +127,21 @@
 ![akashaPut](./images/akashaPut.svg){:width="51%"}
 
 # チェックする仕様
-* 赤黒木のの高さに関する仕様に以下のものがある
+* 赤黒木の高さに関する仕様に以下のものがある
     * 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
 * 以下のように assert を用いて CbC で定義できる
 * この仕様が満たされるかをチェックする
 
 ```
-void verifySpecification(struct Context* context, struct Tree* tree) {
-    assert(!(maxHeight(tree->root, 1) > 2*minHeight(tree->root, 1)));
-        goto meta(context, EnumerateInputs);
+__code verifySpecificationFinish(struct Context* context) {
+    if (context->data[AkashaInfo]->akashaInfo.maxHeight >
+        2*context->data[AkashaInfo]->akashaInfo.minHeight)
+    {
+        context->next = Exit;
+        goto meta(context, ShowTrace);
     }
+    goto meta(context, DuplicateIterator);
+}
 ```
 
 # akasha と CBMC の比較
--- a/presentation/slide.pdf.html	Mon Feb 13 17:39:10 2017 +0900
+++ b/presentation/slide.pdf.html	Mon Feb 13 17:41:26 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-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 {}
   -->
 
@@ -95,7 +95,7 @@
 <ul>
   <li>モデル検査的アプローチ
     <ul>
-      <li>メタ計算ライブラリ akasha による網羅的な実行</li>
+      <li>メタ計算ライブラリ akasha による CbC の網羅的な実行</li>
       <li>非破壊赤黒木の仕様定義と検証</li>
     </ul>
   </li>
@@ -285,7 +285,7 @@
       <li>並列に動作するプログラムの仕様を検証可能</li>
       <li>検証した promela から実行可能な C ソースを生成可能</li>
       <li>仕様は bool になる式を用いた assert</li>
-      <li>promela は C とは記述が異なる</li>
+      <li>デメリット: promela は C とは記述が異なる</li>
     </ul>
   </li>
 </ul>
@@ -333,7 +333,7 @@
 <!-- _S9SLIDE_ -->
 <h1 id="section-6">チェックする仕様</h1>
 <ul>
-  <li>赤黒木のの高さに関する仕様に以下のものがある
+  <li>赤黒木の高さに関する仕様に以下のものがある
     <ul>
       <li>木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる</li>
     </ul>
@@ -342,10 +342,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>