# HG changeset patch # User atton # Date 1486969298 -32400 # Node ID 5cca315b0230297e49b5917092c46ed946806ffc # Parent 2e30ed0e26330848774f4a45082027c67dea2b0a Writing slide... diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/images/akashaPut.pdf Binary file presentation/images/akashaPut.pdf has changed diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/images/akashaPut.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/akashaPut.svg Mon Feb 13 16:01:38 2017 +0900 @@ -0,0 +1,162 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/images/csds.pdf Binary file presentation/images/csds.pdf has changed diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/images/csds.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/csds.svg Mon Feb 13 16:01:38 2017 +0900 @@ -0,0 +1,107 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/images/goto.pdf Binary file presentation/images/goto.pdf has changed diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/images/goto.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/goto.svg Mon Feb 13 16:01:38 2017 +0900 @@ -0,0 +1,111 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/images/meta.pdf Binary file presentation/images/meta.pdf has changed diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/images/meta.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/meta.svg Mon Feb 13 16:01:38 2017 +0900 @@ -0,0 +1,162 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/images/put.pdf Binary file presentation/images/put.pdf has changed diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/images/put.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/put.svg Mon Feb 13 16:01:38 2017 +0900 @@ -0,0 +1,117 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/slide.html --- a/presentation/slide.html Mon Feb 13 15:44:45 2017 +0900 +++ b/presentation/slide.html Mon Feb 13 16:01:38 2017 +0900 @@ -86,7 +86,7 @@ @@ -129,12 +129,26 @@
+

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

+ + + +
+
+

Continuation based C

@@ -151,9 +165,10 @@
  • CodeSegment どうしを接続することによりプログラム全体を作る
    • -
  • TODO: 図
    • +

    goto

    +
    @@ -167,26 +182,28 @@
  • 接続元の Output DataSegment は接続先の Input DataSegment
    • -
  • TODO: 図
    • +

    csds

    +
    -

    メタ計算

    +

    メタ計算

    +

    meta

    +
    @@ -213,23 +230,6 @@
    -

    C言語との対応

    - - - -
    -
    -

    並列に信頼性高く動作する GearsOS

    -

    赤黒木

    +

    赤黒木

    +

    put

    +
    -

    仕様の記述とその確認

    +

    仕様の記述とその確認

    -

    チェックする仕様

    +

    チェックする仕様

    +
    void verifySpecification(struct Context* context, struct Tree* tree) {
+    assert(!(maxHeight(tree->root, 1) > 2*minHeight(tree->root, 1)));
+        goto meta(context, EnumerateInputs);
+    }
+
    +
    @@ -369,61 +387,84 @@
    -

    定理証明

    +

    定理証明的なアプローチの流れ

    + + + +
    +
    + +

    定理証明を Continuation based C へ適用するには

    -

    証明支援系 Agda

    +

    Agda と DataSegment

    +
    __code cs0(int a, int b){
+  goto cs1(a+b);
+}
+
    +
    record ds0 : Set where
+  field
+    a : Int
+    b : Int
+
    +
    -

    Agda 上に CbC を記述するには?

    +

    Agda と CodeSegment

    + +
    __code cs0(int a, int b){
+  goto cs1(a+b);
+}
+
    +
    cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
    + + +
    +
    + +

    メタレベルの型付け

    + @@ -432,71 +473,19 @@
    -

    メタレベルの型付け

    - - - -
    -
    - -

    部分型

    +

    Agda 上のメタ計算

    - - -
    -
    - -

    入力の部分型

    -

    # 出力の部分型

    - - -
    -
    - -

    部分型で何ができたか?

    - @@ -505,17 +494,17 @@
    -

    SingleLinkedStack の証明

    +

    Agda 上に CbC を記述した成果

    @@ -524,32 +513,7 @@
    -

    Agda を用いた証明手法

    - - - -
    -
    - -

    まとめ

    +

    まとめ

    -

    今後の課題

    +

    今後の課題

    diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/slide.md --- a/presentation/slide.md Mon Feb 13 15:44:45 2017 +0900 +++ b/presentation/slide.md Mon Feb 13 16:01:38 2017 +0900 @@ -41,14 +41,17 @@ * 結合や分割が容易 * 入力と出力を持つ * CodeSegment どうしを接続することによりプログラム全体を作る -* TODO: 図 + +![goto](./images/goto.svg){:width="50%"} + # DataSegment * DataSegment とは * データの単位 * CodeSegment の入出力にあたる * 接続元の Output DataSegment は接続先の Input DataSegment -* TODO: 図 + +![csds](./images/csds.svg){:width="50%"} # メタ計算 * とある計算を実現するための計算 @@ -56,7 +59,8 @@ * CbC は通常レベルの計算とメタ計算を分離して考える * 通常レベルではポインタは出てこない、など * CodeSegment の接続部分に処理を追加することで実現 -* TODO: 図 + +![meta](./images/meta.svg){:width="50%"} # Meta CodeSegment * メタ計算を行なう CodeSegment @@ -86,7 +90,8 @@ * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto * goto する前に Meta CodeSegment が実行されて木に挿入する * GearsOS では木の実装のためにスタックを用いて経路情報を保持している -* TODO: 図 + +![put](./images/put.svg){:width="50%"} # 仕様の記述とその確認 * 「バランスが取れている」とは何かを表現できる必要がある @@ -115,10 +120,21 @@ * goto された時に挿入される要素の組み合わせを全て列挙して実行する * その度に仕様の式は成り立つかをチェックする * ノーマルレベルのコードを検証用に変更せず検証可能 -* TODO: 図 + +![akashaPut](./images/akashaPut.svg){:width="51%"} # チェックする仕様 -* TODO: たかさについて +* 赤黒木のの高さに関する仕様に以下のものがある + * 木をルートから辿った際に最も長い経路は最も短い経路の高々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); + } +``` # akasha と CBMC の比較 * akasha は有限の要素数の組み合わせをチェックする @@ -131,7 +147,10 @@ * 固定の要素数までの仕様検査で十分なのか? # 定理証明的なアプローチの流れ -* +* プログラムを証明するにはどうするのか +* 証明支援系 Agda における証明 +* Agda による CbC の定義 +* Agda を用いて CbC のコードを証明する # 定理証明を Continuation based C へ適用するには * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい @@ -141,9 +160,33 @@ * しかし CbC の形式的な定義が無いために今はできない * Agda 上に CbC を定義することで形式的な定義を得る -# Agda における CodeSegment と DataSegment +# Agda と DataSegment +* CbC の DataSegment は Agda のレコード型 + +``` +__code cs0(int a, int b){ + goto cs1(a+b); +} +``` +``` +record ds0 : Set where + field + a : Int + b : Int +``` + # Agda と CodeSegment -# Agda と DataSegment +* CbC の CodeSegment は、Agda の関数型(Input を取って Output を返す) + +``` +__code cs0(int a, int b){ + goto cs1(a+b); +} +``` +``` +cs0 : CodeSegment ds0 ds1 +cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) +``` # メタレベルの型付け * メタ計算とは通常のレベルとは区別された計算 @@ -154,8 +197,18 @@ * Java におけるインターフェース、Haskell における型クラス * 「このデータにはこのフィールドさえあれば良い」 -# Agda 上の Meta CodeSegment -# Agda 上の Meta DataSegment +# Agda 上のメタ計算 +* ノーマルレベルの型を保持したままメタレベルの計算を利用できる + * cs0 の定義はメタ計算用に変更しなくても良い + +``` +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)}) +``` # Agda 上に CbC を記述した成果 * 部分型で CbC の型付けができた diff -r 2e30ed0e2633 -r 5cca315b0230 presentation/slide.pdf.html --- a/presentation/slide.pdf.html Mon Feb 13 15:44:45 2017 +0900 +++ b/presentation/slide.pdf.html Mon Feb 13 16:01:38 2017 +0900 @@ -70,7 +70,7 @@ @@ -113,12 +113,26 @@
    +

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

    + + + +
    +
    +

    Continuation based C

    @@ -135,9 +149,10 @@
  • CodeSegment どうしを接続することによりプログラム全体を作る
    • -
  • TODO: 図
    • +

    goto

    +
    @@ -151,26 +166,28 @@
  • 接続元の Output DataSegment は接続先の Input DataSegment
    • -
  • TODO: 図
    • +

    csds

    +
    -

    メタ計算

    +

    メタ計算

    +

    meta

    +
    @@ -197,23 +214,6 @@
    -

    C言語との対応

    - - - -
    -
    -

    並列に信頼性高く動作する GearsOS

    -

    赤黒木

    +

    赤黒木

    +

    put

    +
    -

    仕様の記述とその確認

    +

    仕様の記述とその確認

    -

    チェックする仕様

    +

    チェックする仕様

    +
    void verifySpecification(struct Context* context, struct Tree* tree) {
+    assert(!(maxHeight(tree->root, 1) > 2*minHeight(tree->root, 1)));
+        goto meta(context, EnumerateInputs);
+    }
+
    +
    @@ -353,61 +371,84 @@
    -

    定理証明

    +

    定理証明的なアプローチの流れ

    + + + +
    +
    + +

    定理証明を Continuation based C へ適用するには

    -

    証明支援系 Agda

    +

    Agda と DataSegment

    +
    __code cs0(int a, int b){
+  goto cs1(a+b);
+}
+
    +
    record ds0 : Set where
+  field
+    a : Int
+    b : Int
+
    +
    -

    Agda 上に CbC を記述するには?

    +

    Agda と CodeSegment

    + +
    __code cs0(int a, int b){
+  goto cs1(a+b);
+}
+
    +
    cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
    + + +
    +
    + +

    メタレベルの型付け

    + @@ -416,71 +457,19 @@
    -

    メタレベルの型付け

    - - - -
    -
    - -

    部分型

    +

    Agda 上のメタ計算

    - - -
    -
    - -

    入力の部分型

    -

    # 出力の部分型

    - - -
    -
    - -

    部分型で何ができたか?

    - @@ -489,17 +478,17 @@
    -

    SingleLinkedStack の証明

    +

    Agda 上に CbC を記述した成果

    @@ -508,32 +497,7 @@
    -

    Agda を用いた証明手法

    - - - -
    -
    - -

    まとめ

    +

    まとめ

    -

    今後の課題

    +

    今後の課題