# HG changeset patch # User soto # Date 1641435507 -32400 # Node ID e02e29a614c92f27dee666e72ebebecbb2f5748a # Parent edabf6c6885d68c1185755e1a93d7e5bcdf22dbe add mindmap diff -r edabf6c6885d -r e02e29a614c9 MindMap/sample.km --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/MindMap/sample.km Thu Jan 06 11:18:27 2022 +0900 @@ -0,0 +1,1014 @@ +{ + "root": { + "data": { + "id": "cgxlfherlow0", + "created": 1641370916386, + "text": "Geas Agda による Red Black Tree の検証", + "expandState": "expand", + "font-family": "arial,helvetica,sans-serif", + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlfx0m2z40", + "created": 1641370950359, + "text": "検証を考慮したプログラミング", + "expandState": "collapse", + "font-family": "arial,helvetica,sans-serif", + "font-size": 48, + "layout": null + }, + "children": [ + { + "data": { + "id": "cgxlgipyuxs0", + "created": 1641370997605, + "text": "normal level", + "expandState": "expand", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlhrjs4k00", + "created": 1641371095186, + "text": "軽量継続", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxli256q000", + "created": 1641371118248, + "text": "ポインタなし", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlim5c3sg0", + "created": 1641371161793, + "text": "atomic", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxllg38ymg0", + "created": 1641371383698, + "text": "関数型", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxllmgvr800", + "created": 1641371397583, + "text": "input", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxllqrjogw0", + "created": 1641371406935, + "text": "output", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + } + ] + }, + { + "data": { + "id": "cgxlgq5zx1s0", + "created": 1641371013811, + "text": "meta level", + "expandState": "expand", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxliu7bxrk0", + "created": 1641371179328, + "text": "context", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxllxthvds0", + "created": 1641371422291, + "text": "すべてのData Gear", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlm47uykg0", + "created": 1641371436220, + "text": "すべてのCode Gear", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlmkb2o800", + "created": 1641371471243, + "text": "process", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxlj2hbn9k0", + "created": 1641371197346, + "text": "証明", + "expandState": "expand", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxljjm4m9s0", + "created": 1641371234642, + "text": "Hoare Condition", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxljmev1280", + "created": 1641371240733, + "text": "Invariant", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlmsv14oo0", + "created": 1641371489864, + "text": "meta Input Data Gear", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + } + ] + }, + { + "data": { + "id": "cgxlkgz1ygo0", + "created": 1641371307257, + "text": "memory 管理", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlkly512o0", + "created": 1641371318086, + "text": "並列実行", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlkqjjn4g0", + "created": 1641371328087, + "text": "ポインタ", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxll4ohduw0", + "created": 1641371358861, + "text": "monad", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxlgvirsns0", + "created": 1641371025468, + "text": "実装記述", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlhfa33qg0", + "created": 1641371068478, + "text": "Gears Agda", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlnho65fs0", + "created": 1641371543868, + "text": "Agdaでの決まった形式", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlnq7nxyg0", + "created": 1641371562461, + "text": "→ t", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxloa4qg0w0", + "created": 1641371605820, + "text": "証明しやすい記述", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxlhipmiew0", + "created": 1641371075948, + "text": "CbC", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlk75b1fs0", + "created": 1641371285867, + "text": "Cと同じ実行速度", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlnvokqhk0", + "created": 1641371574368, + "text": "__code goto", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlofzu3co0", + "created": 1641371618584, + "text": "実行効率が良いように記述", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + } + ] + }, + { + "data": { + "id": "cgxlgzsut080", + "created": 1641371034785, + "text": "実装+証明", + "expandState": "expand", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxloqvtips0", + "created": 1641371642286, + "text": "Gears Agda 上でnormal level で Hoare Condition をつけた形で記述", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlphv589s0", + "created": 1641371701018, + "text": "loop を接続する Meta Gear を用意する", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlptuvpso0", + "created": 1641371727124, + "text": "停止性の証明も行う", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxlq1suwxc0", + "created": 1641371744416, + "text": "Hoare Condition が接続されれば証明は完成", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlqsfels00", + "created": 1641371802376, + "text": "Meta Gear を証明を値として与えているから", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxlub15o9s0", + "created": 1641372077966, + "text": "並列実行の証明は複数のContextのinter leave", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxlrlr5ly00", + "created": 1641371866213, + "text": "仕様記述", + "expandState": "expand", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlrwcghhs0", + "created": 1641371889269, + "text": "Agdaの命題", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxls3hnasg0", + "created": 1641371904820, + "text": "Agdaの型", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxlsaknc3s0", + "created": 1641371920239, + "text": "仕様記述の証明", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlshszaw00", + "created": 1641371935980, + "text": "Agdaの型を持つ値", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxltkpfp340", + "created": 1641372020660, + "text": "入力の仕様の証明を受け取る", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxltxiycpk0", + "created": 1641372048566, + "text": "出力の仕様の証明を次に渡す", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + } + ] + }, + { + "data": { + "id": "cgxlwcze89k0", + "created": 1641372238941, + "text": "実装と検証", + "expandState": "collapse", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlwtaxcnk0", + "created": 1641372274466, + "text": "While program", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlzhv4sv40", + "created": 1641372484659, + "text": "for文で入力が出力に渡ることを確認", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxlx190h6o0", + "created": 1641372291765, + "text": "Binary Tree", + "expandState": "expand", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlx59xw140", + "created": 1641372300528, + "text": "find node", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlx7sexjs0", + "created": 1641372305999, + "text": "replace node", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlxfx8zig0", + "created": 1641372323705, + "text": "Invariant の変換", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxlxy8w0fk0", + "created": 1641372363591, + "text": "Loop Connecter", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxlyewlruw0", + "created": 1641372399854, + "text": "Loopする際にはConnecter経由で呼び出す", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxlysjjq000", + "created": 1641372429539, + "text": "減少列を使用して停止性を示す", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + } + ] + }, + { + "data": { + "id": "cgxm0g75t5s0", + "created": 1641372559397, + "text": "Invariant", + "expandState": "collapse", + "font-family": "arial,helvetica,sans-serif", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm18bzu5k0", + "created": 1641372620639, + "text": "While program", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm1fji0ko0", + "created": 1641372636331, + "text": "loop変数と計算結果の和", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxm200laq00", + "created": 1641372680900, + "text": "Binary Tree", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm24fcyyg0", + "created": 1641372690500, + "text": "Binary Tree の性質", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm2awbkfk0", + "created": 1641372704586, + "text": "Dataであらわしている", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxm2j23bzk0", + "created": 1641372722349, + "text": "Tree をたどったstack", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm2s45f2w0", + "created": 1641372742065, + "text": "Treeの減少列", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxm34s3yow0", + "created": 1641372769635, + "text": "replace tree", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm3af7vm80", + "created": 1641372781916, + "text": "2つのtreeが値の置き換え", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + } + ] + }, + { + "data": { + "id": "cgxm41iane80", + "created": 1641372840875, + "text": "DataでInvariantを表す", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm4iqegso0", + "created": 1641372878371, + "text": "AgdaでのSet", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm4uktr5c0", + "created": 1641372904155, + "text": "Program が生成可能なData の集合全体", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + } + ] + } + ] + }, + { + "data": { + "id": "cgxlvb49n1c0", + "created": 1641372156518, + "text": "目標", + "expandState": "collapse", + "font-family": "arial,helvetica,sans-serif", + "font-size": 48, + "layout": null + }, + "children": [ + { + "data": { + "id": "cgxlvdxrz4o0", + "created": 1641372162655, + "text": "xv6をGears Agdaで記述してCbCに変換", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxm64t605k0", + "created": 1641373004791, + "text": "発表の目次", + "expandState": "collapse", + "layout": null, + "font-family": "arial,helvetica,sans-serif", + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm7egd5hk0", + "created": 1641373104149, + "text": "CbCとGears Agda", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxm7tbvjz40", + "created": 1641373136530, + "text": "Meta level と normal level", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxm87010zs0", + "created": 1641373166288, + "text": "実装と証明", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxm8jn6fyw0", + "created": 1641373193809, + "text": "While Program", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm8pumifk0", + "created": 1641373207320, + "text": "normal level の記述", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxm8ylm8v40", + "created": 1641373226367, + "text": "Hoare Conditionをつけたもの", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxm9ltb9ew0", + "created": 1641373276898, + "text": "test との違い", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxm9rsei0w0", + "created": 1641373289904, + "text": "testでは実数をあたえる", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxmcjx6v5s0", + "created": 1641373507871, + "text": "Gears Agdaでは未定義でもよい", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + } + ] + }, + { + "data": { + "id": "cgxm8nq0bjs0", + "created": 1641373202688, + "text": "Binary Tree", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxmbe451tk0", + "created": 1641373416867, + "text": "find node", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxmbgwimnk0", + "created": 1641373422936, + "text": "replace node", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxmbjnl5qw0", + "created": 1641373428927, + "text": "loop connecter", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxmbpi8cqg0", + "created": 1641373441664, + "text": "Invariant", + "layout": null, + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxmbr88feg0", + "created": 1641373445413, + "text": "Binary tree", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxmbw4mq740", + "created": 1641373456079, + "text": "Stack node", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxmbybtr8o0", + "created": 1641373460867, + "text": "replace node", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + } + ] + }, + { + "data": { + "id": "cgxma4pz0ao0", + "created": 1641373318055, + "text": "将来", + "layout": null, + "font-family": "arial,helvetica,sans-serif", + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxmabj26zs0", + "created": 1641373332875, + "text": "Red Black Tree", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxmagqkeww0", + "created": 1641373344212, + "text": "Delete", + "layout": null, + "font-family": "arial,helvetica,sans-serif", + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxmajosn4g0", + "created": 1641373350636, + "text": "並列実行", + "expandState": "expand", + "layout": null, + "font-family": "arial,helvetica,sans-serif", + "font-size": 48 + }, + "children": [ + { + "data": { + "id": "cgxmap0xtvk0", + "created": 1641373362254, + "text": "Syncronized que", + "layout": null, + "font-size": 48 + }, + "children": [] + }, + { + "data": { + "id": "cgxmb2mfwww0", + "created": 1641373391852, + "text": "モデル検査との結合", + "layout": null, + "font-size": 48 + }, + "children": [] + } + ] + }, + { + "data": { + "id": "cgxmamno3oo0", + "created": 1641373357098, + "text": "xv.6", + "layout": null, + "font-family": "arial,helvetica,sans-serif", + "font-size": 48 + }, + "children": [] + } + ] + } + ] + } + ] + }, + "template": "default", + "theme": "fresh-blue", + "version": "1.4.43" +} \ No newline at end of file diff -r edabf6c6885d -r e02e29a614c9 MindMap/sample.png Binary file MindMap/sample.png has changed diff -r edabf6c6885d -r e02e29a614c9 MindMap/slide.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/MindMap/slide.html Thu Jan 06 11:18:27 2022 +0900 @@ -0,0 +1,2173 @@ +Geas Agda による Left Learning Red Black Tree の検証
+

Gears Agda による
Left Learning Red Black Tree の検証

+ +

Uechi Yuto, Shinji Kono 琉球大学

+
+
+

証明を用いてプログラムの信頼性の向上を目指す

+ +
    +
  • プログラムの信頼性を高めることは重要な課題である +
      +
    • 信頼性を高める手法として「モデル検査」や「定理証明」など
      • +
    +
    • +
  • 当研究室でCbCという言語を開発している +
      +
    • C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
      • +
    +
    • +
  • 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った
    • +
  • 本研究では Gears Agda にて重要なアルゴリズムの一つである Red Black Tree を検証する
    • +
+
+
+

CbC について

+
    +
  • CbCとは当研究室で開発しているC言語の下位言語 +
      +
    • CbC とは C 言語からループ制御構造とサブルーチンコールを取り除き、継続を導入したC 言語の下位言語
      • +
    • 継続呼び出しは引数付き goto 文で表現される。
      • +
    • 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
      • +
    +
    • +
  • CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。
    • +
+
+
+

Agda の基本

+
    +
  • Agdaとは定理証明支援器であり、関数型言語である
    • +
  • Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述できる +
      +
    • これが Curry-Howard 対応となる
      • +
    +
    • +
  • 型の定義部分で、入力と出力の型を定義できる +
      +
    • input → output のようになる
      • +
    +
    • +
  • 関数の定義は = を用いて行う +
      +
    • 関数名の後、 = の前で受け取る引数を記述します
      • +
    +
    • +
+
sample1 : (A : Set ) → Set
+sample1 a = a
+
+sample2 : (A : Set ) → (B : Set ) → Set
+sample2 a b = b
+
+
+
+

Agda の基本 record

+
    +
  • 2つのものが同時に存在すること
    • +
  • Record 型とはオブジェクトあるいは構造体のようなもの
    • +
+
record Env  : Set where
+  field
+    varn : N
+    vari : N
+open Env
+
+

記述する際の基本的な例を以下に挙げる

+
record {varx = zero ; vary = suc zero}
+
+
+
+

Agda の基本 data

+
    +
  • 一つでも存在すること
    • +
  • どちらかが成り立つ型を Data 型 で書く
    • +
+
data bt {n : Level} (A : Set n) : Set n where
+  leaf : bt A
+  node : (key : N) → (value : A) → (left : bt A ) → (right : bt A ) → bt A
+
+

記述する際の基本的な例を以下に挙げる

+
datasample : bt → N
+datasample leaf = zero
+datasample (node key value left right) = suc zero
+
+
+
+

Agda の基本 短縮記法

+
    +
  • with を使用することでその変数のパターンマッチすることもできる
    • +
+
patternmatch-default : Env → N
+patternmatch-default record { varn = zero ; vari = i } = i
+patternmatch-default record { varn = suc n ; vari = i } = patternmatch-default record { varn = n ; vari = suc i }
+
+
patternmatch-extraction : env → N
+patternmatch-extraction env with varn env
+patternmatch-extraction zero = vari env
+patternmatch-extraction suc n = patternmatch-extraction record { varn = n ; vari = suc (vari env) }
+
+
    +
  • ... | `を使用することで関数の定義部分を省略できる
    • +
+
patternmatch-extraction' : env → N
+patternmatch-extraction' env with varn env
+... | zero = vari env
+... | suc n = patternmatch-default' record { varn = n ; vari = suc (vari env) }
+
+
+
+

Gears Agda の記法

+
    +
  • Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない +
      +
    • Agda で実装を行う際には再帰呼び出しを行わないようにする。
      • +
    +
    • +
+
plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
+plus-com env next exit with vary env
+... | zero = exit (record { varx = varx env ; vary = vary env })
+... | suc y = next (record { varx = suc (varx env) ; vary = y })
+
+
    +
  • → t で Set に遷移させるようにし、この後に関数が続くことと、関数を tail call していることで Continuation を定義している
    • +
+
+
+

Gears Agda と Gears CbC の対応 x

+
    +
  • +

    証明のしやすいGears Agda で実装を行いながらContext単位で同時に検証も行う

    +
    • +
  • +

    Gears Agda は検証向きの実装となり、CbCでは高速な実行向きとなる

    +
    • +
  • +

    Gears Agda での検証がCbCによる高速な実行の信頼性となる

    +
    • +
+
+
+

Normal level と Meta Level を用いた信頼性の向上

+

CbCのプログラムの実行部分は以下の2つから構成される

+
    +
  • Normal Level は軽量継続で関数型プログラミングとなる +
      +
    • atomicってなんだろう
      • +
    • ポインタの操作はここでは行わず Meta Level にて行う
      • +
    +
    • +
  • Meta Level では信頼性を保証するために必要な計算を行う +
      +
    • メモリやCPUなどの資源管理
      • +
    • context
      • +
    • 証明
      • +
    • 並列実行（他のプロセスとの干渉）
      • +
    • monad
      • +
    +
    • +
+
+
+

s

+<div src="meta-cg-dg.pdf"> </div> +
+
+

Hoare Logic について

+
    +
  • Hoare Logic とは C.A.R Hoare, R.W Floyd が考案したプログラムの検証の手法
    • +
  • 「プログラムの事前条件 (P) が成立しているときコマンド (C) 実行して停止すると事後条件 (Q) が成り立つ」というもの +
      +
    • CbC の実行を継続するという性質に非常に相性が良い
      • +
    +
    • +
+

pre/post condition を Gears Agda では Meta Input Data Gear として
+プログラム中に遷移させていくことで、プログラムが終始仕様に沿った動きをしている
+ことを検証する

+
+
+

Gears Agda による検証の例（実装）

+
    +
  • while program の検証を例に挙げる +
      +
    • 以下は実装部分のコードとなる
      • +
    +
    • +
+
{-# TERMINATING #-}
+whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+
+
+
+

Gears Agda による検証の例（検証付き実装）

+
    +
  • 先ほど実装した while program に対して証明を付ける
    • +
  • loop を接続する Meta Gear も用意する
    • +
+
TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) 
+  → {Invraiant : Index → Set } → ( reduce : Index → N) 
+  → (loop : (r : Index) → Invraiant r 
+    → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) 
+  → (r : Index) → (p : Invraiant r) → t
+
+
    +
  • 入力として仕様の証明を受け取る
    • +
  • 出力として次の関数に仕様の証明を渡す
    • +
  • Hoare Conditionがプログラムの開始から停止するまで接続されていれば証明は完成 +
      +
    • Meta Gear にて証明を値としてあたえているため
      • +
    +
    • +
+
+
+

test との違い

+
    +
  • test では実数を与えた際の出力が仕様に沿ったものであるかを検証する +
      +
    • コーナーケースで仕様に沿った動きをしていない場合を考慮できない
      • +
    +
    • +
  • 今回の定理証明を用いた証明では実数を必要としない +
      +
    • そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる
      • +
    +
    • +
+
+
+

Gears Agda による BinaryTree の実装

+
    +
  • Agdaが変数への再代入を許していないためそのままでは木構造を実装できない +
      +
    • 木構造を辿る際に現在いるノード以下の木構造をそのまま stack に格納する
      • +
    • replace / delete などの操作を行った後に stack を参照し Tree を再構築する
      • +
    • CbCへの変換の時に問題になりそうな予感
      • +
    +
    • +
  • ここの説明いらないかも？
    • +
+
+
+

Gears Agda による BinaryTree の実装 find node

+
find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
+  → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t
+find key leaf st _ exit = exit leaf st
+find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
+find key n st _ exit | tri≈ ¬a b ¬c = exit n st
+find key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st)
+find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
+
+
+
+

Gears Agda による BinaryTree の実装 replace node

+
replace : {n m : Level} {A : Set n} {t : Set m} 
+  → (key : N) → (value : A) → bt A → List (bt A) 
+  → (next : N → A → bt A → List (bt A) → t ) 
+  → (exit : bt A → t) → t
+replace key value repl [] next exit = exit repl    -- can't happen
+replace key value repl (leaf ∷ []) next exit = exit repl    
+replace key value repl (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right ) 
+... | tri≈ ¬a b ¬c = exit (node key₁ value  left right ) 
+... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl ) 
+replace key value repl (leaf ∷ st) next exit = next key value repl st    
+replace key value repl (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st
+... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st
+
+
+
+

Gears Agda による BinaryTree の実装 loop connecter

+

+
+
+
+

Gears Agda による Binary Tree の検証 Invariant

+

具体的な例を一つ挙げて、Invariantの説明を行う

+
    +
  • Binary Tree の性質である、左の子のkeyは親より小さく、
    +右の子のkeyは親より大きいことを検証
    • +
  • Stack に格納されているTreeはその次のStackの減少列になっているか
    • +
  • Tree を正しく入れ替えられているか
    • +
+
+
+

Gears Agda による Binary Tree の検証 Invariant

+
    +
  • Tree Invariant
    • +
+
data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
+    t-leaf : treeInvariant leaf 
+    t-single : (key : N) → (value : A) →  treeInvariant (node key value leaf leaf) 
+    t-right : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) 
+      → treeInvariant (node key₁ value₁ t₁ t₂)
+      → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) 
+    t-left  : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) 
+      → treeInvariant (node key value t₁ t₂)
+      → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) 
+    t-node  : {key key₁ key₂ : N} → {value value₁ value₂ : A} 
+      → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂)
+      → treeInvariant (node key value t₁ t₂) 
+      → treeInvariant (node key₂ value₂ t₃ t₄)
+      → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 
+
+
+
+

Gears Agda による Binary Tree の検証 Invariant

+
    +
  • Stack Invariant
    • +
+
data stackInvariant {n : Level} {A : Set n} (key : N) : (top orig : bt A) 
+  → (stack : List (bt A)) → Set n where
+    s-single : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
+    s-right : {tree tree0 tree₁ : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} 
+      → key₁ < key  → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st 
+      → stackInvariant key tree tree0 (tree ∷ st)
+    s-left :  {tree₁ tree0 tree : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} 
+      → key  < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st 
+      → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
+
+
+
+

Gears Agda による Binary Tree の検証 Invariant

+
    +
  • Replace Invariant
    • +
+
data replacedTree {n : Level} {A : Set n} (key : N) (value : A) : (before after : bt A) → Set n where
+    r-leaf : replacedTree key value leaf (node key value leaf leaf)
+    r-node : {value₁ : A} → {t t₁ : bt A} 
+      → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 
+    r-right : {k : N } {v1 : A} → {t t1 t2 : bt A}
+          → k < key →  replacedTree key value t2 t 
+          →  replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) 
+    r-left : {k : N } {v1 : A} → {t t1 t2 : bt A}
+          → key < k →  replacedTree key value t1 t 
+          → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 
+
+
+
+

Gears Agda による Binary Tree の検証

+

Binary Tree の実装に対して上述した3つのInvariantを
+Meta Data Gear として渡しながら実行できるように記述する

+
findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A)
+  → treeInvariant env ∧ stackInvariant env
+  → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t
+
+
+
+

今後の研究方針

+
    +
  • 現在は Binary Tree の検証までしか行えていないが、
    +今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
    • +
  • 今後は Gears Agda による実装と条件の追加をおこなう
    • +
  • モデル検査
    • +
+
+
+

まとめ

+
    +
  • Gears Agda にて Binary Tree を検証することができた +
      +
    • Gears Agda における Termination を使用しない実装の仕方を確率した
      • +
    • Hoare Logic による検証もできるようになった
      • +
    • 今後は Red Black Tree の検証をすすめる
      • +
    +
    • +
  • モデル検査をしたい
    • +
+

英語版も欲しい

+

condition を テンプレみたいに作ってかきやすくする話

+
+

研究目的

コードの解説 +あとで…

findは全部書いても大丈夫そう

これは途中省略してよさそう

コードの解説 +省略した方がたぶん絶対良い +right と left なんかはほとんど対照的なので省略とかでよさそう +あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう

\ No newline at end of file diff -r edabf6c6885d -r e02e29a614c9 MindMap/slide.pdf Binary file MindMap/slide.pdf has changed diff -r edabf6c6885d -r e02e29a614c9 slide/meta_cg_dg.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/meta_cg_dg.svg Thu Jan 06 11:18:27 2022 +0900 @@ -0,0 +1,131 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + Produced by OmniGraffle 7.19.2\n2022-01-06 02:09:09 +0000 + + Canvas 1 + + + Layer 1 + + + + + + + + + + + + + Meta Data Gear + + + + + + + + + + + Meta Data Gear + + + + + + + + Code Gear + + + + + + + Data Gear + + + + + + + + + + Data Gear + + + + + + + + + + Meta + Code Gear + + + + + + + Code Gear + + + + + + + Data Gear + + + + + + + + + + Data Gear + + + + + + + + + + Meta + Code Gear + + + + + diff -r edabf6c6885d -r e02e29a614c9 slide/slide.md --- a/slide/slide.md Wed Jan 05 17:15:56 2022 +0900 +++ b/slide/slide.md Thu Jan 06 11:18:27 2022 +0900 @@ -60,6 +60,13 @@ - 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った - 本研究では Gears Agda にて重要なアルゴリズムの一つである Red Black Tree を検証する +# CbC について +- CbCとは当研究室で開発しているC言語の下位言語 + - CbC とは C 言語からループ制御構造とサブルーチンコールを取り除き、継続を導入したC 言語の下位言語 + - 継続呼び出しは引数付き goto 文で表現される。 + - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語 +- CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。 + # Agda の基本 - Agdaとは定理証明支援器であり、関数型言語である @@ -136,13 +143,6 @@ ``` -# CbC について -- CbCとは当研究室で開発しているC言語の下位言語 - - CbC とは C 言語からループ制御構造とサブルーチンコールを取り除き、継続を導入したC 言語の下位言語 - - 継続呼び出しは引数付き goto 文で表現される。 - - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語 -- CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。 - # Gears Agda の記法 - Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない @@ -156,25 +156,41 @@ - `→ t` で Set に遷移させるようにし、この後に関数が続くことと、関数を tail call していることで Continuation を定義している -# Gears Agda と Gears CbC の対応 -- Gears Agda で実装を行い、同時に検証も行う -- これを CbC に変換する +# Gears Agda と Gears CbC の対応 x +- 証明のしやすいGears Agda で実装を行いながらContext単位で同時に検証も行う - Gears Agda は検証向きの実装となり、CbCでは高速な実行向きとなる - Gears Agda での検証がCbCによる高速な実行の信頼性となる +# Normal level と Meta Level を用いた信頼性の向上 +CbCのプログラムの実行部分は以下の2つから構成される +- Normal Level は軽量継続で関数型プログラミングとなる + - atomicってなんだろう + - ポインタの操作はここでは行わず Meta Level にて行う +- Meta Level では信頼性を保証するために必要な計算を行う + - メモリやCPUなどの資源管理 + - context + - 証明 + - 並列実行（他のプロセスとの干渉） + - monad + +# s +![bg right:80%](meta_cg_dg.svg) # Hoare Logic について -- Hoare Logic とは C.A.R Hoare、R.W Floyd が考案したプログラムの検証の手法 -- 「プログラムの事前条件 (P) が成立しているとき、コマンド (C) 実行して停止 -すると事後条件 (Q) が成り立つ」というもの +- Hoare Logic とは C.A.R Hoare, R.W Floyd が考案したプログラムの検証の手法 +- 「プログラムの事前条件 (P) が成立しているときコマンド (C) 実行して停止すると事後条件 (Q) が成り立つ」というもの - CbC の実行を継続するという性質に非常に相性が良い -pre/post conditionの +pre/post condition を Gears Agda では Meta Input Data Gear として +プログラム中に遷移させていくことで、プログラムが終始仕様に沿った動きをしている +ことを検証する + + # Gears Agda による検証の例（実装） -- 例として while program の検証をする - - まずは実装部分 +- while program の検証を例に挙げる + - 以下は実装部分のコードとなる ``` {-# TERMINATING #-} whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t @@ -183,29 +199,165 @@ whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next ``` -# Binary Tree について - + +# Gears Agda による検証の例（検証付き実装） +- 先ほど実装した while program に対して証明を付ける +- loop を接続する Meta Gear も用意する +``` +TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) + → {Invraiant : Index → Set } → ( reduce : Index → N) + → (loop : (r : Index) → Invraiant r + → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) + → (r : Index) → (p : Invraiant r) → t +``` +- 入力として仕様の証明を受け取る +- 出力として次の関数に仕様の証明を渡す +- Hoare Conditionがプログラムの開始から停止するまで接続されていれば証明は完成 + - Meta Gear にて証明を値としてあたえているため + + + +# test との違い +- test では実数を与えた際の出力が仕様に沿ったものであるかを検証する + - コーナーケースで仕様に沿った動きをしていない場合を考慮できない +- 今回の定理証明を用いた証明では実数を必要としない + - そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる + + +# Gears Agda による BinaryTree の実装 +- Agdaが変数への再代入を許していないためそのままでは木構造を実装できない + - 木構造を辿る際に現在いるノード以下の木構造をそのまま stack に格納する + - replace / delete などの操作を行った後に stack を参照し Tree を再構築する + - CbCへの変換の時に問題になりそうな予感 +- ここの説明いらないかも？ + + +# Gears Agda による BinaryTree の実装 find node +``` +find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) + → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t +find key leaf st _ exit = exit leaf st +find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁ +find key n st _ exit | tri≈ ¬a b ¬c = exit n st +find key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st) +find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) +``` + + + +# Gears Agda による BinaryTree の実装 replace node +``` +replace : {n m : Level} {A : Set n} {t : Set m} + → (key : N) → (value : A) → bt A → List (bt A) + → (next : N → A → bt A → List (bt A) → t ) + → (exit : bt A → t) → t +replace key value repl [] next exit = exit repl -- can't happen +replace key value repl (leaf ∷ []) next exit = exit repl +replace key value repl (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right ) +... | tri≈ ¬a b ¬c = exit (node key₁ value left right ) +... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl ) +replace key value repl (leaf ∷ st) next exit = next key value repl st +replace key value repl (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st +... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st +... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st +``` + -# Gears Agda による Binary Tree の実装 -Agda が再代入を許していないことから -stackを用いてエスケープしている説明が必要 + + + +# Gears Agda による BinaryTree の実装 loop connecter +``` + +``` + +# Gears Agda による Binary Tree の検証 Invariant +具体的な例を一つ挙げて、Invariantの説明を行う +- Binary Tree の性質である、左の子のkeyは親より小さく、 +右の子のkeyは親より大きいことを検証 +- Stack に格納されているTreeはその次のStackの減少列になっているか +- Tree を正しく入れ替えられているか + +# Gears Agda による Binary Tree の検証 Invariant +- Tree Invariant +``` +data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where + t-leaf : treeInvariant leaf + t-single : (key : N) → (value : A) → treeInvariant (node key value leaf leaf) + t-right : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) + → treeInvariant (node key₁ value₁ t₁ t₂) + → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) + t-left : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) + → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) + t-node : {key key₁ key₂ : N} → {value value₁ value₂ : A} + → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂) + → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₂ value₂ t₃ t₄) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) +``` + + + + +# Gears Agda による Binary Tree の検証 Invariant +- Stack Invariant +``` +data stackInvariant {n : Level} {A : Set n} (key : N) : (top orig : bt A) + → (stack : List (bt A)) → Set n where + s-single : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ []) + s-right : {tree tree0 tree₁ : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} + → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st + → stackInvariant key tree tree0 (tree ∷ st) + s-left : {tree₁ tree0 tree : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} + → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st + → stackInvariant key tree₁ tree0 (tree₁ ∷ st) +``` + +# Gears Agda による Binary Tree の検証 Invariant +- Replace Invariant +``` +data replacedTree {n : Level} {A : Set n} (key : N) (value : A) : (before after : bt A) → Set n where + r-leaf : replacedTree key value leaf (node key value leaf leaf) + r-node : {value₁ : A} → {t t₁ : bt A} + → replacedTree key value (node key value₁ t t₁) (node key value t t₁) + r-right : {k : N } {v1 : A} → {t t1 t2 : bt A} + → k < key → replacedTree key value t2 t + → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) + r-left : {k : N } {v1 : A} → {t t1 t2 : bt A} + → key < k → replacedTree key value t1 t + → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) +``` # Gears Agda による Binary Tree の検証 - -# これで検証を行えているのかの説明 -Hoare Logic で -Hoare Condition が接続されていること - -不変条件なににするか -BTの不変条件３つを説明 - +Binary Tree の実装に対して上述した3つのInvariantを +Meta Data Gear として渡しながら実行できるように記述する +``` +findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A) + → treeInvariant env ∧ stackInvariant env + → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t +``` # 今後の研究方針 - 現在は Binary Tree の検証までしか行えていないが、 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず - 今後は Gears Agda による実装と条件の追加をおこなう -- モデル検査のこと、CbC変換のことも話してもよい +- モデル検査 # まとめ - Gears Agda にて Binary Tree を検証することができた @@ -216,4 +368,5 @@ 英語版も欲しい -condition を テンプレみたいに作ってかきやすくする話 \ No newline at end of file +condition を テンプレみたいに作ってかきやすくする話 +