diff -r 26563097333c -r 8a84cda440f3 presentation/slide.html --- 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 @@ @@ -129,7 +129,22 @@

モデル検査的アプローチについての流れ

本発表ではモデル検査的アプローチについて中心に見ていきます

修士論文の内部の比率は半分半分くらい
定理証明の方は説明する内容が多くて複雑
モデル検査的アプローチは過去論文を提出したもの +
- なのでそちらをメインで発表します
+

+ + +

+ +

モデル検査的アプローチについての流れ

Continuation based C (CbC) 言語について
CbC における CodeSegment と DataSegment を用いたプログラミングスタイル

CodeSegment とは
- 処理の単位
- 処理の単位であり、入力と出力を持つ
- 結合や分割が容易
- 入力と出力を持つ
CodeSegment どうしを接続することによりプログラム全体を作る
CodeSegment どうしを接続することによりプログラム全体を作る +
- 関数呼び出しと違って戻ってこない(goto)
+

__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+

@@ -186,11 +209,16 @@

__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+

メタ計算

とある計算を実現するための計算
ネットワーク接続、例外処理、メモリ確保、並列処理など

赤黒木

データの保存に用いる二分木
特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る @@ -256,7 +284,7 @@

rbtree

@@ -271,11 +299,14 @@

put

goto meta(context, Put);
+

仕様の記述とその確認

「バランスが取れている」とは何かを表現できる必要がある
+
```
assert(x < 10);
+
```
+

@@ -326,36 +360,21 @@ - -

- -

メタ計算ライブラリ akasha

メタ計算としてプログラムの状態を数え上げる -
- goto された時に挿入される要素の組み合わせを全て列挙して実行する
- その度に仕様の式は成り立つかをチェックする
-
ノーマルレベルのコードを検証用に変更せず検証可能

- -

akashaPut

assert(x < 10);
+

チェックする仕様

赤黒木の高さに関する仕様に以下のものがある
- 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
以下のように assert を用いて CbC で定義できる
この仕様が満たされるかをチェックする
以下のような条件式を仕様として CbC で定義、検証できる

__code verifySpecificationFinish(struct Context* context) {
@@ -373,6 +392,27 @@


 
 
+メタ計算ライブラリ akasha
+
+  メタ計算としてプログラムの状態を数え上げる
+    
+      goto された時に挿入される要素の組み合わせを全て列挙して実行する
+        
+          赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……
+        
+      
+      その度に仕様の式は成り立つかをチェックする
+    
+  
+  ノーマルレベルのコードを検証用に変更せず検証可能
+
+
+
+
+
+
+
+
 akasha と CBMC の比較
 
   akasha は有限の要素数の組み合わせをチェックする
@@ -395,18 +435,6 @@
 
 
 
-定理証明的なアプローチの流れ
-
-  プログラムを証明するにはどうするのか
-  証明支援系 Agda における証明
-  Agda による CbC の定義
-  Agda を用いて CbC のコードを証明する
-
-
-
-
-
-
 定理証明を Continuation based C へ適用するには
 
   任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
@@ -475,7 +503,7 @@
   部分型を使う
     
       Java におけるインターフェース、Haskell における型クラス
-      「このデータにはこのフィールドさえあれば良い」
+      「このフィールドXがあればデータ型Tとみなして良い」
     
   
 
@@ -493,11 +521,16 @@
   
 
 
+cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+
 main : ds1
 main = goto cs0 (record {a = 100 ; b = 50})
 
 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)})
 
 
 
@@ -553,6 +586,30 @@
   赤黒木の挿入に関する性質を証明する
 
 
+
+
+
+
+発表履歴
+
+  Agda 入門.
+    
+      オープンソースカンファレンス 2014 Okinawa, May 2014.
+    
+  
+  形式手法を学び始めて思うことと、形式手法を広めるには(2p).
+    
+      情報処理学会ソフトウェア工学研究会 (IPSJ SIGSE) ウィンターワークショップ 2015・ イン・宜野湾 (WWS2015), Jan 2015.
+    
+  
+  Continuation based C を用いたプログラムの検証手法(6p).
+    
+      2016 年並列/分散/協調処理に関する『松本』サマー・ワークショップ (SWoPP2016)
+      情報処理学会・プログラミング研究会 第 110 回プログラミング研究会 (PRO-2016-2) Aug 2016.
+    
+  
+
+
 
 
 
diff -r 26563097333c -r 8a84cda440f3 presentation/slide.md
--- a/presentation/slide.md	Mon Feb 13 17:41:26 2017 +0900
+++ b/presentation/slide.md	Tue Feb 14 11:31:08 2017 +0900
@@ -21,6 +21,12 @@
     * 型システムを通して CbC の形式的な定義を得る
     * SingleLinkedStack の性質の証明
 
+# 本発表ではモデル検査的アプローチについて中心に見ていきます
+* 修士論文の内部の比率は半分半分くらい
+* 定理証明の方は説明する内容が多くて複雑
+* モデル検査的アプローチは過去論文を提出したもの
+    *  なのでそちらをメインで発表します
+
 # モデル検査的アプローチについての流れ
 * Continuation based C (CbC) 言語について
 * CbC における CodeSegment と DataSegment を用いたプログラミングスタイル
@@ -37,13 +43,19 @@
 
 # CodeSegment
 * CodeSegment とは
-    * 処理の単位
+    * 処理の単位であり、入力と出力を持つ
     * 結合や分割が容易
-    * 入力と出力を持つ
 * CodeSegment どうしを接続することによりプログラム全体を作る
+    * 関数呼び出しと違って戻ってこない(goto)
 
 ![cs](./images/cs.svg){:width="50%"}
 
+```
+__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+```
+
 
 # DataSegment
 * DataSegment とは
@@ -53,6 +65,12 @@
 
 ![ds](./images/ds.svg){:width="50%"}
 
+```
+__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+```
+
 # メタ計算
 * とある計算を実現するための計算
 * ネットワーク接続、例外処理、メモリ確保、並列処理など
@@ -87,15 +105,20 @@
     * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)
     * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定
 
-![rbtree](./images/rbtree.svg){:width="50%"}
+![rbtree](./images/rbtree.svg){:width="35%"}
 
 # GearsOS における赤黒木の利用例(ノードの挿入)
 * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto
 * goto する前に Meta CodeSegment が実行されて木に挿入する
 * GearsOS では木の実装のためにスタックを用いて経路情報を保持している
 
+
 ![put](./images/put.svg){:width="50%"}
 
+```
+goto meta(context, Put);
+```
+
 # 仕様の記述とその確認
 * 「バランスが取れている」とは何かを表現できる必要がある
     * 実行可能な CbC の式を使った assert になる
@@ -110,6 +133,10 @@
     * 仕様は bool になる式を用いた assert
     * デメリット: promela は C とは記述が異なる
 
+```
+assert(x < 10);
+```
+
 # 既存のモデル検査器 CBMC
 * CBMC
     * 検証対象のCソースを変更しないでも良い
@@ -118,19 +145,14 @@
     * 仕様は bool になる式を用いた assert
     * 有限ステップ検証する有界モデル検査器
 
-# メタ計算ライブラリ akasha
-* メタ計算としてプログラムの状態を数え上げる
-    * goto された時に挿入される要素の組み合わせを全て列挙して実行する
-    * その度に仕様の式は成り立つかをチェックする
-* ノーマルレベルのコードを検証用に変更せず検証可能
-
-![akashaPut](./images/akashaPut.svg){:width="51%"}
+```
+assert(x < 10);
+```
 
 # チェックする仕様
 * 赤黒木の高さに関する仕様に以下のものがある
     * 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
-* 以下のように assert を用いて CbC で定義できる
-* この仕様が満たされるかをチェックする
+* 以下のような条件式を仕様として CbC で定義、検証できる
 
 ```
 __code verifySpecificationFinish(struct Context* context) {
@@ -144,6 +166,15 @@
 }
 ```
 
+# メタ計算ライブラリ akasha
+* メタ計算としてプログラムの状態を数え上げる
+    * goto された時に挿入される要素の組み合わせを全て列挙して実行する
+        * 赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……
+    * その度に仕様の式は成り立つかをチェックする
+* ノーマルレベルのコードを検証用に変更せず検証可能
+
+![akashaPut](./images/akashaPut.svg){:width="51%"}
+
 # akasha と CBMC の比較
 * akasha は有限の要素数の組み合わせをチェックする
     * 要素数が13個までならどの順で木に挿入しても良い
@@ -154,12 +185,6 @@
     * akasha は返した
 * 固定の要素数までの仕様検査で十分なのか?
 
-# 定理証明的なアプローチの流れ
-* プログラムを証明するにはどうするのか
-* 証明支援系 Agda における証明
-* Agda による CbC の定義
-* Agda を用いて CbC のコードを証明する
-
 # 定理証明を Continuation based C へ適用するには
 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
 * そのままプログラムの性質を保証してやる
@@ -206,19 +231,25 @@
 * メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い
 * 部分型を使う
     * Java におけるインターフェース、Haskell における型クラス
-    * 「このデータにはこのフィールドさえあれば良い」
+    * 「このフィールドXがあればデータ型Tとみなして良い」
 
 # Agda 上のメタ計算
 * ノーマルレベルの型を保持したままメタレベルの計算を利用できる
     * cs0 の定義はメタ計算用に変更しなくても良い
 
 ```
+cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+```
+
+```
 main : ds1
 main = goto cs0 (record {a = 100 ; b = 50})
 ```
 ```
 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)})
 ```
 
 # Agda 上に CbC を記述した成果
@@ -244,5 +275,14 @@
 * 型情報から stub を自動生成すkる
 * 赤黒木の挿入に関する性質を証明する
 
+# 発表履歴
+* Agda 入門.
+    * オープンソースカンファレンス 2014 Okinawa, May 2014.
+* 形式手法を学び始めて思うことと、形式手法を広めるには(2p).
+    * 情報処理学会ソフトウェア工学研究会 (IPSJ SIGSE) ウィンターワークショップ 2015・ イン・宜野湾 (WWS2015), Jan 2015.
+* Continuation based C を用いたプログラムの検証手法(6p).
+    * 2016 年並列/分散/協調処理に関する『松本』サマー・ワークショップ (SWoPP2016)
+    * 情報処理学会・プログラミング研究会 第 110 回プログラミング研究会 (PRO-2016-2) Aug 2016.
+
 
 
diff -r 26563097333c -r 8a84cda440f3 presentation/slide.pdf.html
--- a/presentation/slide.pdf.html	Mon Feb 13 17:41:26 2017 +0900
+++ b/presentation/slide.pdf.html	Tue Feb 14 11:31:08 2017 +0900
@@ -70,7 +70,7 @@
 
 
@@ -113,7 +113,22 @@
 
 
 
-モデル検査的アプローチについての流れ
+本発表ではモデル検査的アプローチについて中心に見ていきます
+
+  修士論文の内部の比率は半分半分くらい
+  定理証明の方は説明する内容が多くて複雑
+  モデル検査的アプローチは過去論文を提出したもの
+    
+      なのでそちらをメインで発表します
+    
+  
+
+
+
+
+
+
+モデル検査的アプローチについての流れ
 
   Continuation based C (CbC) 言語について
   CbC における CodeSegment と DataSegment を用いたプログラミングスタイル
@@ -143,16 +158,24 @@
 
   CodeSegment とは
     
-      処理の単位
+      処理の単位であり、入力と出力を持つ
       結合や分割が容易
-      入力と出力を持つ
     
   
-  CodeSegment どうしを接続することによりプログラム全体を作る
+  CodeSegment どうしを接続することによりプログラム全体を作る
+    
+      関数呼び出しと違って戻ってこない(goto)
+    
+  
 
 
 
 
+__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+
+
 
 
 
@@ -170,11 +193,16 @@
 
 
 
+__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+
+
 
 
 
 
-メタ計算
+メタ計算
 
   とある計算を実現するための計算
   ネットワーク接続、例外処理、メモリ確保、並列処理など
@@ -228,7 +256,7 @@
 
 
 
-赤黒木
+赤黒木
 
   データの保存に用いる二分木
   特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
@@ -240,7 +268,7 @@
   
 
 
-
+
 
 
 
@@ -255,11 +283,14 @@
 
 
 
+goto meta(context, Put);
+
+
 
 
 
 
-仕様の記述とその確認
+仕様の記述とその確認
 
   「バランスが取れている」とは何かを表現できる必要がある
     
@@ -290,6 +321,9 @@
   
 
 
+assert(x < 10);
+
+
 
 
 
@@ -310,36 +344,21 @@
   
 
 
-
-
-
-
-メタ計算ライブラリ akasha
-
-  メタ計算としてプログラムの状態を数え上げる
-    
-      goto された時に挿入される要素の組み合わせを全て列挙して実行する
-      その度に仕様の式は成り立つかをチェックする
-    
-  
-  ノーマルレベルのコードを検証用に変更せず検証可能
-
-
-
+assert(x < 10);
+
 
 
 
 
 
-チェックする仕様
+チェックする仕様
 
   赤黒木の高さに関する仕様に以下のものがある
     
       木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
     
   
-  以下のように assert を用いて CbC で定義できる
-  この仕様が満たされるかをチェックする
+  以下のような条件式を仕様として CbC で定義、検証できる
 
 
 __code verifySpecificationFinish(struct Context* context) {
@@ -357,6 +376,27 @@
 

 
 
+メタ計算ライブラリ akasha
+
+  メタ計算としてプログラムの状態を数え上げる
+    
+      goto された時に挿入される要素の組み合わせを全て列挙して実行する
+        
+          赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……
+        
+      
+      その度に仕様の式は成り立つかをチェックする
+    
+  
+  ノーマルレベルのコードを検証用に変更せず検証可能
+
+
+
+
+
+
+
+
 akasha と CBMC の比較
 
   akasha は有限の要素数の組み合わせをチェックする
@@ -379,18 +419,6 @@
 
 
 
-定理証明的なアプローチの流れ
-
-  プログラムを証明するにはどうするのか
-  証明支援系 Agda における証明
-  Agda による CbC の定義
-  Agda を用いて CbC のコードを証明する
-
-
-
-
-
-
 定理証明を Continuation based C へ適用するには
 
   任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
@@ -459,7 +487,7 @@
   部分型を使う
     
       Java におけるインターフェース、Haskell における型クラス
-      「このデータにはこのフィールドさえあれば良い」
+      「このフィールドXがあればデータ型Tとみなして良い」
     
   
 
@@ -477,11 +505,16 @@
   
 
 
+cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+
 main : ds1
 main = goto cs0 (record {a = 100 ; b = 50})
 
 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)})
 
 
 
@@ -537,6 +570,30 @@
   赤黒木の挿入に関する性質を証明する
 
 
+
+
+
+
+発表履歴
+
+  Agda 入門.
+    
+      オープンソースカンファレンス 2014 Okinawa, May 2014.
+    
+  
+  形式手法を学び始めて思うことと、形式手法を広めるには(2p).
+    
+      情報処理学会ソフトウェア工学研究会 (IPSJ SIGSE) ウィンターワークショップ 2015・ イン・宜野湾 (WWS2015), Jan 2015.
+    
+  
+  Continuation based C を用いたプログラムの検証手法(6p).
+    
+      2016 年並列/分散/協調処理に関する『松本』サマー・ワークショップ (SWoPP2016)
+      情報処理学会・プログラミング研究会 第 110 回プログラミング研究会 (PRO-2016-2) Aug 2016.
+    
+  
+
+