Mercurial > hg > Papers > 2016 > atton-ipsjpro

changeset 63:60faf7f9d741

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update slide
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 08 Aug 2016 22:11:48 +0900
parents 3439a1f7e79f
children f5cad08f76b5
files presentation/slide.html presentation/slide.md presentation/slide.pdf.html
diffstat 3 files changed, 19 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/presentation/slide.html	Fri Aug 05 18:47:03 2016 +0900
+++ b/presentation/slide.html	Mon Aug 08 22:11:48 2016 +0900
@@ -86,7 +86,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.0 (2015-12-25) [x86_64-darwin14]
-                on 2016-08-05 18:35:45 +0900 with Markdown engine kramdown (1.9.0)
+                on 2016-08-08 09:27:07 +0900 with Markdown engine kramdown (1.9.0)
                   using options {}
   -->
 
@@ -313,7 +313,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="meta-code-segment-">Meta Code Segment を使った検証</h1>
+<h1 id="meta-code-segment-">Meta Code Segment を使った例</h1>
 <ul>
   <li><code>meta</code> を切り替えることでノーマルレベルの計算を拡張する
     <ul>
--- a/presentation/slide.md	Fri Aug 05 18:47:03 2016 +0900
+++ b/presentation/slide.md	Mon Aug 08 22:11:48 2016 +0900
@@ -134,7 +134,7 @@
 ```
 
 
-# Meta Code Segment を使った検証
+# Meta Code Segment を使った例
 * `meta` を切り替えることでノーマルレベルの計算を拡張する
     * `goto` した回数を数える
 
@@ -178,9 +178,22 @@
     * 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙
     * 挿入後の木はきちんとバランスしているかチェックする
 * CbC のメタ計算 Akasha では要素数13個までチェックできた
-    * 13の階乗で62億通りを1,2時間ほど
+    * 13の階乗の62億通りを1,2時間ほど
 * 実装にわざとバグを入れた場合にはバランスしない入力例を返した
 
+# Akasha による赤黒木の検証方法
+* 挿入される可能性のある全ての要素を持つ循環リストを作成
+* 木に対して要素を1つ挿入する
+    * 挿入した要素を排除した循環リストを作成
+    * 挿入後に作成された木を保存する
+    * 挿入後の木がバランスされているかをチェックする
+    * 反例用に挿入した要素を記録
+* 全ての要素を挿入したら
+    * 保存していた木と循環リストを再現して深さを高くする
+    * 循環リストの head を1つ進める
+    * 循環リストの head と tail が同じになったら深さを高くする
+* 最初の循環リストの head と tail が同じになったら終了
+
 # C Bounded Model Checker
 * Carnegie Mellon University で開発されている記号実行モデルチェッカ
     * C, C++, Java に対応
--- a/presentation/slide.pdf.html	Fri Aug 05 18:47:03 2016 +0900
+++ b/presentation/slide.pdf.html	Mon Aug 08 22:11:48 2016 +0900
@@ -70,7 +70,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.0 (2015-12-25) [x86_64-darwin14]
-                on 2016-08-05 18:35:45 +0900 with Markdown engine kramdown (1.9.0)
+                on 2016-08-08 09:27:07 +0900 with Markdown engine kramdown (1.9.0)
                   using options {}
   -->
 
@@ -297,7 +297,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="meta-code-segment-">Meta Code Segment を使った検証</h1>
+<h1 id="meta-code-segment-">Meta Code Segment を使った例</h1>
 <ul>
   <li><code>meta</code> を切り替えることでノーマルレベルの計算を拡張する
     <ul>