Mercurial > hg > Papers > 2021 > soto-prosym
changeset 9:e02e29a614c9
add mindmap
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 06 Jan 2022 11:18:27 +0900 |
| parents | edabf6c6885d |
| children | 60d4617eac84 |
| files | MindMap/sample.km MindMap/sample.png MindMap/slide.html MindMap/slide.pdf slide/meta_cg_dg.svg slide/slide.md |
| diffstat | 6 files changed, 3502 insertions(+), 31 deletions(-) [+] |
line wrap: on
line diff
--- /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
--- /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 @@ +<!DOCTYPE html><html lang="ja-JP"><head><title>Geas Agda による Left Learning Red Black Tree の検証</title><meta property="og:title" content="Geas Agda による Left Learning Red Black Tree の検証"><meta charset="UTF-8"><meta name="viewport" content="width=device-width,height=device-height,initial-scale=1.0"><meta name="apple-mobile-web-app-capable" content="yes"><meta http-equiv="X-UA-Compatible" content="ie=edge"><meta property="og:type" content="website"><meta name="twitter:card" content="summary"><style>@media screen{body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button{-webkit-tap-highlight-color:transparent;-webkit-appearance:none;-moz-appearance:none;appearance:none;background-color:transparent;border:0;color:inherit;cursor:pointer;font-size:inherit;opacity:.8;outline:none;padding:0;transition:opacity .2s linear}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:disabled,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:disabled,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:disabled{cursor:not-allowed;opacity:.15!important}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover{opacity:1}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:active,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:active,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover:active{opacity:.6}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:not(:disabled),body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:not(:disabled),body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover:not(:disabled){transition:none}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button.bespoke-marp-presenter-info-page-prev{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48cGF0aCBmaWxsPSJub25lIiBzdHJva2U9IiNmZmYiIHN0cm9rZS1saW5lY2FwPSJyb3VuZCIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIgc3Ryb2tlLXdpZHRoPSI1IiBkPSJNNjggOTAgMjggNTBsNDAtNDAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button.bespoke-marp-presenter-info-page-next{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48cGF0aCBmaWxsPSJub25lIiBzdHJva2U9IiNmZmYiIHN0cm9rZS1saW5lY2FwPSJyb3VuZCIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIgc3Ryb2tlLXdpZHRoPSI1IiBkPSJtMzIgOTAgNDAtNDAtNDAtNDAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen]{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS1saW5lam9pbjpyb3VuZDtzdHJva2Utd2lkdGg6NXB4fTwvc3R5bGU+PC9kZWZzPjxyZWN0IGNsYXNzPSJhIiB4PSIxMCIgeT0iMjAiIHdpZHRoPSI4MCIgaGVpZ2h0PSI2MCIgcng9IjUuNjciLz48cGF0aCBjbGFzcz0iYSIgZD0iTTQwIDcwSDIwVjUwbTIwIDBMMjAgNzBtNDAtNDBoMjB2MjBtLTIwIDAgMjAtMjAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button.exit[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button.exit[data-bespoke-marp-osc=fullscreen]{background-image:url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS1saW5lam9pbjpyb3VuZDtzdHJva2Utd2lkdGg6NXB4fTwvc3R5bGU+PC9kZWZzPjxyZWN0IGNsYXNzPSJhIiB4PSIxMCIgeT0iMjAiIHdpZHRoPSI4MCIgaGVpZ2h0PSI2MCIgcng9IjUuNjciLz48cGF0aCBjbGFzcz0iYSIgZD0iTTIwIDUwaDIwdjIwbS0yMCAwIDIwLTIwbTQwIDBINjBWMzBtMjAgMEw2MCA1MCIvPjwvc3ZnPg==")}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter]{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48cGF0aCBkPSJNODcuOCA0Ny41Qzg5IDUwIDg3LjcgNTIgODUgNTJIMzVhOC43IDguNyAwIDAgMS03LjItNC41bC0xNS42LTMxQzExIDE0IDEyLjIgMTIgMTUgMTJoNTBhOC44IDguOCAwIDAgMSA3LjIgNC41ek02MCA1MnYzNm0tMTAgMGgyME00NSA0MmgyMCIgZmlsbD0ibm9uZSIgc3Ryb2tlPSIjZmZmIiBzdHJva2UtbGluZWNhcD0icm91bmQiIHN0cm9rZS1saW5lam9pbj0icm91bmQiIHN0cm9rZS13aWR0aD0iNSIvPjwvc3ZnPg==") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}}.bespoke-marp-note,.bespoke-marp-osc,.bespoke-progress-parent{display:none;transition:none}@media screen{body,html{height:100%;margin:0}body{background:#000;overflow:hidden}svg.bespoke-marp-slide{content-visibility:hidden;opacity:0;pointer-events:none;z-index:-1}svg.bespoke-marp-slide.bespoke-marp-active{content-visibility:visible;opacity:1;pointer-events:auto;z-index:0}svg.bespoke-marp-slide.bespoke-marp-active.bespoke-marp-active-ready *{-webkit-animation-name:__bespoke_marp__!important;animation-name:__bespoke_marp__!important}@supports not (content-visibility:hidden){svg.bespoke-marp-slide[data-bespoke-marp-load=hideable]{display:none}svg.bespoke-marp-slide[data-bespoke-marp-load=hideable].bespoke-marp-active{display:block}}[data-bespoke-marp-fragment=inactive]{visibility:hidden}body[data-bespoke-view=""] .bespoke-marp-parent,body[data-bespoke-view=next] .bespoke-marp-parent{bottom:0;left:0;position:absolute;right:0;top:0}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc{background:rgba(0,0,0,.65);border-radius:7px;bottom:50px;color:#fff;contain:paint;display:block;font-family:Helvetica,Arial,sans-serif;font-size:16px;left:50%;line-height:0;opacity:1;padding:12px;position:absolute;touch-action:manipulation;transform:translateX(-50%);transition:opacity .2s linear;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;white-space:nowrap;will-change:transform;z-index:1}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>*,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>*{margin-left:6px}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>:first-child,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>:first-child{margin-left:0}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>span,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>span{opacity:.8}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>span[data-bespoke-marp-osc=page],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>span[data-bespoke-marp-osc=page]{display:inline-block;min-width:140px;text-align:center}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev]{height:32px;line-height:32px;width:32px}body[data-bespoke-view=""] .bespoke-marp-parent.bespoke-marp-inactive,body[data-bespoke-view=next] .bespoke-marp-parent.bespoke-marp-inactive{cursor:none}body[data-bespoke-view=""] .bespoke-marp-parent.bespoke-marp-inactive>.bespoke-marp-osc,body[data-bespoke-view=next] .bespoke-marp-parent.bespoke-marp-inactive>.bespoke-marp-osc{opacity:0;pointer-events:none}body[data-bespoke-view=""] svg.bespoke-marp-slide,body[data-bespoke-view=next] svg.bespoke-marp-slide{height:100%;left:0;position:absolute;top:0;width:100%}body[data-bespoke-view=""] .bespoke-progress-parent{background:#222;display:flex;height:5px;width:100%}body[data-bespoke-view=""] .bespoke-progress-parent+.bespoke-marp-parent{top:5px}body[data-bespoke-view=""] .bespoke-progress-parent .bespoke-progress-bar{background:#0288d1;flex:0 0 0;transition:flex-basis .2s cubic-bezier(0,1,1,1)}body[data-bespoke-view=next]{background:transparent}body[data-bespoke-view=presenter]{background:#161616}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container{display:grid;font-family:Helvetica,Arial,sans-serif;grid-template:"current next" minmax(140px,1fr) "current note" 2fr "info note" 3em/2fr 1fr;height:100%;left:0;position:absolute;top:0;width:100%}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent{grid-area:current;overflow:hidden;position:relative}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent svg.bespoke-marp-slide{height:calc(100% - 40px);left:20px;pointer-events:none;position:absolute;top:20px;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;width:calc(100% - 40px)}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent svg.bespoke-marp-slide.bespoke-marp-active{filter:drop-shadow(0 3px 10px rgba(0,0,0,.5))}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container{background:#222;cursor:pointer;display:none;grid-area:next;overflow:hidden;position:relative}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container.active{display:block}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container iframe.bespoke-marp-presenter-next{background:transparent;border:0;display:block;filter:drop-shadow(0 3px 10px rgba(0,0,0,.5));height:calc(100% - 40px);left:20px;pointer-events:none;position:absolute;top:20px;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;width:calc(100% - 40px)}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container{background:#222;color:#eee;grid-area:note}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note{word-wrap:break-word;box-sizing:border-box;font-size:1.1em;height:calc(100% - 40px);margin:20px;overflow:auto;padding-right:3px;scrollbar-color:hsla(0,0%,93%,.5) transparent;scrollbar-width:thin;white-space:pre-wrap;width:calc(100% - 40px)}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar{width:6px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar-track{background:transparent}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar-thumb{background:hsla(0,0%,93%,.5);border-radius:6px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note:empty{pointer-events:none}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note.active{display:block}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note p:first-child{margin-top:0}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note p:last-child{margin-bottom:0}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container{align-items:center;box-sizing:border-box;color:#eee;display:flex;flex-wrap:nowrap;grid-area:info;justify-content:center;padding:0 10px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-time,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-timer{box-sizing:border-box;display:block;padding:0 10px;white-space:nowrap;width:100%}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button{height:1.5em;line-height:1.5em;width:1.5em}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page{order:2;text-align:center}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page .bespoke-marp-presenter-info-page-text{display:inline-block;min-width:120px;text-align:center}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-time{color:#999;order:1;text-align:left}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-timer{color:#999;order:3;text-align:right}}@media print{.bespoke-marp-presenter-info-container,.bespoke-marp-presenter-next-container,.bespoke-marp-presenter-note-container{display:none}}</style><style>div#p>svg>foreignObject>section{width:1280px;height:720px;box-sizing:border-box;overflow:hidden;position:relative;scroll-snap-align:center center}div#p>svg>foreignObject>section:after{bottom:0;content:attr(data-marpit-pagination);padding:inherit;pointer-events:none;position:absolute;right:0}div#p>svg>foreignObject>section:not([data-marpit-pagination]):after{display:none}/* Normalization */div#p>svg>foreignObject>section h1{font-size:2em;margin:0.67em 0}div#p>svg>foreignObject>section video::-webkit-media-controls{will-change:transform}@page{size:1280px 720px;margin:0}@media print{body,html{background-color:#fff;margin:0;page-break-inside:avoid;break-inside:avoid-page}div#p>svg>foreignObject>section{page-break-before:always;break-before:page}div#p>svg>foreignObject>section,div#p>svg>foreignObject>section *{-webkit-print-color-adjust:exact!important;animation-delay:0s!important;animation-duration:0s!important;color-adjust:exact!important;transition:none!important}div#p>svg[data-marpit-svg]{display:block;height:100vh;width:100vw}}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{display:block;height:auto;width:100%}@supports (-ms-ime-align:auto){div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{position:static}}div#p>svg>foreignObject>section svg[data-marp-fitting=svg].__reflow__{content:""}@supports (-ms-ime-align:auto){div#p>svg>foreignObject>section svg[data-marp-fitting=svg].__reflow__{position:relative}}div#p>svg>foreignObject>section [data-marp-fitting-svg-content]{display:table;white-space:nowrap;width:-webkit-max-content;width:-moz-max-content;width:max-content}div#p>svg>foreignObject>section [data-marp-fitting-svg-content-wrap]{white-space:pre}div#p>svg>foreignObject>section img[data-marp-twemoji]{background:transparent;height:1em;margin:0 .05em 0 .1em;vertical-align:-.1em;width:1em} +/*! + * Marp default theme. + * + * @theme default + * @author Yuki Hattori + * + * @auto-scaling true + * @size 16:9 1280px 720px + * @size 4:3 960px 720px + */div#p>svg>foreignObject>section{-ms-text-size-adjust:100%;-webkit-text-size-adjust:100%;word-wrap:break-word;background-color:#fff;color:#24292f;font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica,Arial,sans-serif,Apple Color Emoji,Segoe UI Emoji;font-size:16px;line-height:1.5;margin:0}div#p>svg>foreignObject>section{--marpit-root-font-size:16px}div#p>svg>foreignObject>section .octicon{fill:currentColor;display:inline-block;vertical-align:text-bottom}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link:before{background-color:currentColor;content:" ";display:inline-block;height:16px;-webkit-mask-image:url('data:image/svg+xml;charset=utf-8,<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 16 16" aria-hidden="true"><path fill-rule="evenodd" d="M7.775 3.275a.75.75 0 0 0 1.06 1.06l1.25-1.25a2 2 0 1 1 2.83 2.83l-2.5 2.5a2 2 0 0 1-2.83 0 .75.75 0 0 0-1.06 1.06 3.5 3.5 0 0 0 4.95 0l2.5-2.5a3.5 3.5 0 0 0-4.95-4.95l-1.25 1.25zm-4.69 9.64a2 2 0 0 1 0-2.83l2.5-2.5a2 2 0 0 1 2.83 0 .75.75 0 0 0 1.06-1.06 3.5 3.5 0 0 0-4.95 0l-2.5 2.5a3.5 3.5 0 0 0 4.95 4.95l1.25-1.25a.75.75 0 0 0-1.06-1.06l-1.25 1.25a2 2 0 0 1-2.83 0z"/></svg>');mask-image:url('data:image/svg+xml;charset=utf-8,<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 16 16" aria-hidden="true"><path fill-rule="evenodd" d="M7.775 3.275a.75.75 0 0 0 1.06 1.06l1.25-1.25a2 2 0 1 1 2.83 2.83l-2.5 2.5a2 2 0 0 1-2.83 0 .75.75 0 0 0-1.06 1.06 3.5 3.5 0 0 0 4.95 0l2.5-2.5a3.5 3.5 0 0 0-4.95-4.95l-1.25 1.25zm-4.69 9.64a2 2 0 0 1 0-2.83l2.5-2.5a2 2 0 0 1 2.83 0 .75.75 0 0 0 1.06-1.06 3.5 3.5 0 0 0-4.95 0l-2.5 2.5a3.5 3.5 0 0 0 4.95 4.95l1.25-1.25a.75.75 0 0 0-1.06-1.06l-1.25 1.25a2 2 0 0 1-2.83 0z"/></svg>');width:16px}div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section figcaption,div#p>svg>foreignObject>section figure{display:block}div#p>svg>foreignObject>section summary{display:list-item}div#p>svg>foreignObject>section a{background-color:transparent;color:#0969da;text-decoration:none}div#p>svg>foreignObject>section a:active,div#p>svg>foreignObject>section a:hover{outline-width:0}div#p>svg>foreignObject>section abbr[title]{border-bottom:none;-webkit-text-decoration:underline dotted;text-decoration:underline dotted}div#p>svg>foreignObject>section b,div#p>svg>foreignObject>section strong{font-weight:600}div#p>svg>foreignObject>section dfn{font-style:italic}div#p>svg>foreignObject>section h1{border-bottom:1px solid #d8dee4;font-size:2em;font-weight:600;margin:.67em 0;padding-bottom:.3em}div#p>svg>foreignObject>section mark{background-color:#ff0;color:#24292f}div#p>svg>foreignObject>section small{font-size:90%}div#p>svg>foreignObject>section sub,div#p>svg>foreignObject>section sup{font-size:75%;line-height:0;position:relative;vertical-align:baseline}div#p>svg>foreignObject>section sub{bottom:-.25em}div#p>svg>foreignObject>section sup{top:-.5em}div#p>svg>foreignObject>section img{background-color:#fff;border-style:none;box-sizing:content-box;max-width:100%}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section kbd,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section samp{font-family:monospace,monospace;font-size:1em}div#p>svg>foreignObject>section figure{margin:1em 40px}div#p>svg>foreignObject>section hr{background:transparent;background-color:#d0d7de;border:0;box-sizing:content-box;height:.25em;margin:24px 0;overflow:hidden;padding:0}div#p>svg>foreignObject>section [type=reset],div#p>svg>foreignObject>section [type=submit],div#p>svg>foreignObject>section html [type=button]{-webkit-appearance:button}div#p>svg>foreignObject>section [type=button]::-moz-focus-inner,div#p>svg>foreignObject>section [type=reset]::-moz-focus-inner,div#p>svg>foreignObject>section [type=submit]::-moz-focus-inner{border-style:none;padding:0}div#p>svg>foreignObject>section [type=button]:-moz-focusring,div#p>svg>foreignObject>section [type=reset]:-moz-focusring,div#p>svg>foreignObject>section [type=submit]:-moz-focusring{outline:1px dotted ButtonText}div#p>svg>foreignObject>section [type=checkbox],div#p>svg>foreignObject>section [type=radio]{box-sizing:border-box;padding:0}div#p>svg>foreignObject>section [type=number]::-webkit-inner-spin-button,div#p>svg>foreignObject>section [type=number]::-webkit-outer-spin-button{height:auto}div#p>svg>foreignObject>section [type=search]{-webkit-appearance:textfield;outline-offset:-2px}div#p>svg>foreignObject>section [type=search]::-webkit-search-cancel-button,div#p>svg>foreignObject>section [type=search]::-webkit-search-decoration{-webkit-appearance:none}div#p>svg>foreignObject>section ::-webkit-input-placeholder{color:inherit;opacity:.54}div#p>svg>foreignObject>section ::-webkit-file-upload-button{-webkit-appearance:button;font:inherit}div#p>svg>foreignObject>section a:hover{text-decoration:underline}div#p>svg>foreignObject>section hr:after,div#p>svg>foreignObject>section hr:before{content:"";display:table}div#p>svg>foreignObject>section hr:after{clear:both}div#p>svg>foreignObject>section table{border-collapse:collapse;border-spacing:0;display:block;max-width:100%;overflow:auto;width:-webkit-max-content;width:-moz-max-content;width:max-content}div#p>svg>foreignObject>section td,div#p>svg>foreignObject>section th{padding:0}div#p>svg>foreignObject>section details summary{cursor:pointer}div#p>svg>foreignObject>section details:not([open])>:not(summary){display:none!important}div#p>svg>foreignObject>section kbd{background-color:#f6f8fa;border:1px solid rgba(175,184,193,.2);border-radius:6px;box-shadow:inset 0 -1px 0 rgba(175,184,193,.2);color:#24292f;display:inline-block;font:11px ui-monospace,SFMono-Regular,SF Mono,Menlo,Consolas,Liberation Mono,monospace;line-height:10px;padding:3px 5px;vertical-align:middle}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2,div#p>svg>foreignObject>section h3,div#p>svg>foreignObject>section h4,div#p>svg>foreignObject>section h5,div#p>svg>foreignObject>section h6{font-weight:600;line-height:1.25;margin-bottom:16px;margin-top:24px}div#p>svg>foreignObject>section h2{border-bottom:1px solid #d8dee4;font-size:1.5em;font-weight:600;padding-bottom:.3em}div#p>svg>foreignObject>section h3{font-size:1.25em;font-weight:600}div#p>svg>foreignObject>section h4{font-size:1em;font-weight:600}div#p>svg>foreignObject>section h5{font-size:.875em;font-weight:600}div#p>svg>foreignObject>section h6{color:#57606a;font-size:.85em;font-weight:600}div#p>svg>foreignObject>section p{margin-bottom:10px;margin-top:0}div#p>svg>foreignObject>section blockquote{border-left:.25em solid #d0d7de;color:#57606a;margin:0;padding:0 1em}div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section ul{margin-bottom:0;margin-top:0;padding-left:2em}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ul ol{list-style-type:lower-roman}div#p>svg>foreignObject>section ol ol ol,div#p>svg>foreignObject>section ol ul ol,div#p>svg>foreignObject>section ul ol ol,div#p>svg>foreignObject>section ul ul ol{list-style-type:lower-alpha}div#p>svg>foreignObject>section dd{margin-left:0}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section tt{font-family:ui-monospace,SFMono-Regular,SF Mono,Menlo,Consolas,Liberation Mono,monospace;font-size:12px}div#p>svg>foreignObject>section pre{word-wrap:normal;margin-bottom:0;margin-top:0}div#p>svg>foreignObject>section :-ms-input-placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section ::-moz-placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section ::placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section .pl-c{color:#6e7781}div#p>svg>foreignObject>section .pl-c1,div#p>svg>foreignObject>section .pl-s .pl-v{color:#0550ae}div#p>svg>foreignObject>section .pl-e,div#p>svg>foreignObject>section .pl-en{color:#8250df}div#p>svg>foreignObject>section .pl-s .pl-s1,div#p>svg>foreignObject>section .pl-smi{color:#24292f}div#p>svg>foreignObject>section .pl-ent{color:#116329}div#p>svg>foreignObject>section .pl-k{color:#cf222e}div#p>svg>foreignObject>section .pl-pds,div#p>svg>foreignObject>section .pl-s,div#p>svg>foreignObject>section .pl-s .pl-pse .pl-s1,div#p>svg>foreignObject>section .pl-sr,div#p>svg>foreignObject>section .pl-sr .pl-cce,div#p>svg>foreignObject>section .pl-sr .pl-sra,div#p>svg>foreignObject>section .pl-sr .pl-sre{color:#0a3069}div#p>svg>foreignObject>section .pl-smw,div#p>svg>foreignObject>section .pl-v{color:#953800}div#p>svg>foreignObject>section .pl-bu{color:#82071e}div#p>svg>foreignObject>section .pl-ii{background-color:#82071e;color:#f6f8fa}div#p>svg>foreignObject>section .pl-c2{background-color:#cf222e;color:#f6f8fa}div#p>svg>foreignObject>section .pl-sr .pl-cce{color:#116329;font-weight:700}div#p>svg>foreignObject>section .pl-ml{color:#3b2300}div#p>svg>foreignObject>section .pl-mh,div#p>svg>foreignObject>section .pl-mh .pl-en,div#p>svg>foreignObject>section .pl-ms{color:#0550ae;font-weight:700}div#p>svg>foreignObject>section .pl-mi{color:#24292f;font-style:italic}div#p>svg>foreignObject>section .pl-mb{color:#24292f;font-weight:700}div#p>svg>foreignObject>section .pl-md{background-color:#ffebe9;color:#82071e}div#p>svg>foreignObject>section .pl-mi1{background-color:#dafbe1;color:#116329}div#p>svg>foreignObject>section .pl-mc{background-color:#ffd8b5;color:#953800}div#p>svg>foreignObject>section .pl-mi2{background-color:#0550ae;color:#eaeef2}div#p>svg>foreignObject>section .pl-mdr{color:#8250df;font-weight:700}div#p>svg>foreignObject>section .pl-ba{color:#57606a}div#p>svg>foreignObject>section .pl-sg{color:#8c959f}div#p>svg>foreignObject>section .pl-corl{color:#0a3069;text-decoration:underline}div#p>svg>foreignObject>section [data-catalyst]{display:block}div#p>svg>foreignObject>section g-emoji{font-family:Apple Color Emoji,Segoe UI Emoji,Segoe UI Symbol;font-size:1em;font-style:normal!important;font-weight:400;line-height:1;vertical-align:-.075em}div#p>svg>foreignObject>section g-emoji img{height:1em;width:1em}div#p>svg>foreignObject>section:after,div#p>svg>foreignObject>section:before{ + /* content:""; */display:table}div#p>svg>foreignObject>section:after{clear:both}div#p>svg>foreignObject>section>:first-child{margin-top:0!important}div#p>svg>foreignObject>section>:last-child{margin-bottom:0!important}div#p>svg>foreignObject>section a:not([href]){color:inherit;text-decoration:none}div#p>svg>foreignObject>section .absent{color:#cf222e}div#p>svg>foreignObject>section .anchor{float:left;line-height:1;margin-left:-20px;padding-right:4px}div#p>svg>foreignObject>section .anchor:focus{outline:none}div#p>svg>foreignObject>section blockquote,div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section dl,div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section p,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section table,div#p>svg>foreignObject>section ul{margin-bottom:16px;margin-top:0}div#p>svg>foreignObject>section blockquote>:first-child{margin-top:0}div#p>svg>foreignObject>section blockquote>:last-child{margin-bottom:0}div#p>svg>foreignObject>section sup>a:before{content:"["}div#p>svg>foreignObject>section sup>a:after{content:"]"}div#p>svg>foreignObject>section h1 .octicon-link,div#p>svg>foreignObject>section h2 .octicon-link,div#p>svg>foreignObject>section h3 .octicon-link,div#p>svg>foreignObject>section h4 .octicon-link,div#p>svg>foreignObject>section h5 .octicon-link,div#p>svg>foreignObject>section h6 .octicon-link{color:#24292f;vertical-align:middle;visibility:hidden}div#p>svg>foreignObject>section h1:hover .anchor,div#p>svg>foreignObject>section h2:hover .anchor,div#p>svg>foreignObject>section h3:hover .anchor,div#p>svg>foreignObject>section h4:hover .anchor,div#p>svg>foreignObject>section h5:hover .anchor,div#p>svg>foreignObject>section h6:hover .anchor{text-decoration:none}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link{visibility:visible}div#p>svg>foreignObject>section h1 code,div#p>svg>foreignObject>section h1 tt,div#p>svg>foreignObject>section h2 code,div#p>svg>foreignObject>section h2 tt,div#p>svg>foreignObject>section h3 code,div#p>svg>foreignObject>section h3 tt,div#p>svg>foreignObject>section h4 code,div#p>svg>foreignObject>section h4 tt,div#p>svg>foreignObject>section h5 code,div#p>svg>foreignObject>section h5 tt,div#p>svg>foreignObject>section h6 code,div#p>svg>foreignObject>section h6 tt{font-size:inherit;padding:0 .2em}div#p>svg>foreignObject>section ol.no-list,div#p>svg>foreignObject>section ul.no-list{list-style-type:none;padding:0}div#p>svg>foreignObject>section ol[type="1"]{list-style-type:decimal}div#p>svg>foreignObject>section ol[type=a]{list-style-type:lower-alpha}div#p>svg>foreignObject>section ol[type=i]{list-style-type:lower-roman}div#p>svg>foreignObject>section div>ol:not([type]){list-style-type:decimal}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ol ul,div#p>svg>foreignObject>section ul ol,div#p>svg>foreignObject>section ul ul{margin-bottom:0;margin-top:0}div#p>svg>foreignObject>section li>p{margin-top:16px}div#p>svg>foreignObject>section li+li{margin-top:.25em}div#p>svg>foreignObject>section dl{padding:0}div#p>svg>foreignObject>section dl dt{font-size:1em;font-style:italic;font-weight:600;margin-top:16px;padding:0}div#p>svg>foreignObject>section dl dd{margin-bottom:16px;padding:0 16px}div#p>svg>foreignObject>section table th{font-weight:600}div#p>svg>foreignObject>section table td,div#p>svg>foreignObject>section table th{border:1px solid #d0d7de;padding:6px 13px}div#p>svg>foreignObject>section table tr{background-color:#fff;border-top:1px solid #d8dee4}div#p>svg>foreignObject>section table tr:nth-child(2n){background-color:#f6f8fa}div#p>svg>foreignObject>section table img{background-color:transparent}div#p>svg>foreignObject>section img[align=right]{padding-left:20px}div#p>svg>foreignObject>section img[align=left]{padding-right:20px}div#p>svg>foreignObject>section .emoji{background-color:transparent;max-width:none;vertical-align:text-top}div#p>svg>foreignObject>section span.frame,div#p>svg>foreignObject>section span.frame>span{display:block;overflow:hidden}div#p>svg>foreignObject>section span.frame>span{border:1px solid #d0d7de;float:left;margin:13px 0 0;padding:7px;width:auto}div#p>svg>foreignObject>section span.frame span img{display:block;float:left}div#p>svg>foreignObject>section span.frame span span{clear:both;color:#24292f;display:block;padding:5px 0 0}div#p>svg>foreignObject>section span.align-center{clear:both;display:block;overflow:hidden}div#p>svg>foreignObject>section span.align-center>span{display:block;margin:13px auto 0;overflow:hidden;text-align:center}div#p>svg>foreignObject>section span.align-center span img{margin:0 auto;text-align:center}div#p>svg>foreignObject>section span.align-right{clear:both;display:block;overflow:hidden}div#p>svg>foreignObject>section span.align-right>span{display:block;margin:13px 0 0;overflow:hidden;text-align:right}div#p>svg>foreignObject>section span.align-right span img{margin:0;text-align:right}div#p>svg>foreignObject>section span.float-left{display:block;float:left;margin-right:13px;overflow:hidden}div#p>svg>foreignObject>section span.float-left span{margin:13px 0 0}div#p>svg>foreignObject>section span.float-right{display:block;float:right;margin-left:13px;overflow:hidden}div#p>svg>foreignObject>section span.float-right>span{display:block;margin:13px auto 0;overflow:hidden;text-align:right}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section tt{background-color:rgba(175,184,193,.2);border-radius:6px;font-size:85%;margin:0;padding:.2em .4em}div#p>svg>foreignObject>section code br,div#p>svg>foreignObject>section tt br{display:none}div#p>svg>foreignObject>section del code{text-decoration:inherit}div#p>svg>foreignObject>section pre code{font-size:100%}div#p>svg>foreignObject>section pre>code{background:transparent;border:0;margin:0;padding:0;white-space:pre;word-break:normal}div#p>svg>foreignObject>section .highlight{margin-bottom:16px}div#p>svg>foreignObject>section .highlight pre{margin-bottom:0;word-break:normal}div#p>svg>foreignObject>section pre{background-color:#f6f8fa;border-radius:6px;font-size:85%;line-height:1.45;overflow:auto;padding:16px}div#p>svg>foreignObject>section pre code,div#p>svg>foreignObject>section pre tt{word-wrap:normal;background-color:transparent;border:0;display:inline;line-height:inherit;margin:0;max-width:auto;overflow:visible;padding:0}div#p>svg>foreignObject>section .csv-data td,div#p>svg>foreignObject>section .csv-data th{font-size:12px;line-height:1;overflow:hidden;padding:5px;text-align:left;white-space:nowrap}div#p>svg>foreignObject>section .csv-data .blob-num{background:#fff;border:0;padding:10px 8px 9px;text-align:right}div#p>svg>foreignObject>section .csv-data tr{border-top:0}div#p>svg>foreignObject>section .csv-data th{background:#f6f8fa;border-top:0;font-weight:600}div#p>svg>foreignObject>section .footnotes{border-top:1px solid #d0d7de;color:#57606a;font-size:12px}div#p>svg>foreignObject>section div#p>svg>foreignObject>section section.footnotes{--marpit-root-font-size:12px}div#p>svg>foreignObject>section .footnotes ol{padding-left:16px}div#p>svg>foreignObject>section .footnotes li{position:relative}div#p>svg>foreignObject>section .footnotes li:target:before{border:2px solid #0969da;border-radius:6px;bottom:-8px;content:"";left:-24px;pointer-events:none;position:absolute;right:-8px;top:-8px}div#p>svg>foreignObject>section .footnotes li:target{color:#24292f}div#p>svg>foreignObject>section .footnotes .data-footnote-backref g-emoji{font-family:monospace}div#p>svg>foreignObject>section [hidden]{display:none!important}div#p>svg>foreignObject>section ::-webkit-calendar-picker-indicator{filter:invert(50%)}div#p>svg>foreignObject>section .hljs{background:#fff;color:#333;display:block;overflow-x:auto;padding:.5em}div#p>svg>foreignObject>section .hljs-comment,div#p>svg>foreignObject>section .hljs-meta{color:#969896}div#p>svg>foreignObject>section .hljs-emphasis,div#p>svg>foreignObject>section .hljs-quote,div#p>svg>foreignObject>section .hljs-strong,div#p>svg>foreignObject>section .hljs-template-variable,div#p>svg>foreignObject>section .hljs-variable{color:#df5000}div#p>svg>foreignObject>section .hljs-keyword,div#p>svg>foreignObject>section .hljs-selector-tag,div#p>svg>foreignObject>section .hljs-type{color:#d73a49}div#p>svg>foreignObject>section .hljs-attribute,div#p>svg>foreignObject>section .hljs-bullet,div#p>svg>foreignObject>section .hljs-literal,div#p>svg>foreignObject>section .hljs-symbol{color:#0086b3}div#p>svg>foreignObject>section .hljs-name,div#p>svg>foreignObject>section .hljs-section{color:#63a35c}div#p>svg>foreignObject>section .hljs-tag{color:#333}div#p>svg>foreignObject>section .hljs-attr,div#p>svg>foreignObject>section .hljs-selector-attr,div#p>svg>foreignObject>section .hljs-selector-class,div#p>svg>foreignObject>section .hljs-selector-id,div#p>svg>foreignObject>section .hljs-selector-pseudo,div#p>svg>foreignObject>section .hljs-title{color:#6f42c1}div#p>svg>foreignObject>section .hljs-addition{background-color:#eaffea;color:#55a532}div#p>svg>foreignObject>section .hljs-deletion{background-color:#ffecec;color:#bd2c00}div#p>svg>foreignObject>section .hljs-link{text-decoration:underline}div#p>svg>foreignObject>section .hljs-number{color:#005cc5}div#p>svg>foreignObject>section .hljs-string{color:#032f62}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{max-height:563px}div#p>svg>foreignObject>section h1{color:#246;font-size:1.6em}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{border-bottom:none}div#p>svg>foreignObject>section h2{font-size:1.3em}div#p>svg>foreignObject>section h3{font-size:1.1em}div#p>svg>foreignObject>section h4{font-size:1.05em}div#p>svg>foreignObject>section h5{font-size:1em}div#p>svg>foreignObject>section h6{font-size:.9em}div#p>svg>foreignObject>section h1 strong,div#p>svg>foreignObject>section h2 strong,div#p>svg>foreignObject>section h3 strong,div#p>svg>foreignObject>section h4 strong,div#p>svg>foreignObject>section h5 strong,div#p>svg>foreignObject>section h6 strong{color:#48c;font-weight:inherit}div#p>svg>foreignObject>section hr{height:0;padding-top:.25em}div#p>svg>foreignObject>section pre{border:1px solid #999;line-height:1.15;overflow:visible}div#p>svg>foreignObject>section pre code svg[data-marp-fitting=svg]{max-height:529px}div#p>svg>foreignObject>section footer,div#p>svg>foreignObject>section header{color:hsla(0,0%,40%,.75);font-size:18px;left:30px;margin:0;position:absolute}div#p>svg>foreignObject>section header{top:21px}div#p>svg>foreignObject>section footer{bottom:21px}div#p>svg>foreignObject>section{align-items:stretch;background:#fff;display:flex;flex-flow:column nowrap;font-size:29px;height:720px;justify-content:center;padding:78.5px;width:1280px}div#p>svg>foreignObject>section{--marpit-root-font-size:29px}div#p>svg>foreignObject>section>:last-child,div#p>svg>foreignObject>section[data-footer]>:nth-last-child(2){margin-bottom:0}div#p>svg>foreignObject>section>:first-child,div#p>svg>foreignObject>section>header:first-child+*{margin-top:0}div#p>svg>foreignObject>section:after{bottom:21px;color:#777;font-size:24px;padding:0;position:absolute;right:30px}div#p>svg>foreignObject>section:after{--marpit-root-font-size:24px}div#p>svg>foreignObject>section.invert{background-color:#222;color:#e6eaf0}div#p>svg>foreignObject>section.invert:after{color:#999}div#p>svg>foreignObject>section.invert img{background-color:transparent}div#p>svg>foreignObject>section.invert a{color:#50b3ff}div#p>svg>foreignObject>section.invert h1{color:#a3c5e7}div#p>svg>foreignObject>section.invert h2,div#p>svg>foreignObject>section.invert h3,div#p>svg>foreignObject>section.invert h4,div#p>svg>foreignObject>section.invert h5{color:#ebeff5}div#p>svg>foreignObject>section.invert blockquote,div#p>svg>foreignObject>section.invert h6{border-color:#3d3f43;color:#939699}div#p>svg>foreignObject>section.invert h1 strong,div#p>svg>foreignObject>section.invert h2 strong,div#p>svg>foreignObject>section.invert h3 strong,div#p>svg>foreignObject>section.invert h4 strong,div#p>svg>foreignObject>section.invert h5 strong,div#p>svg>foreignObject>section.invert h6 strong{color:#7bf}div#p>svg>foreignObject>section.invert hr{background-color:#3d3f43}div#p>svg>foreignObject>section.invert footer,div#p>svg>foreignObject>section.invert header{color:hsla(0,0%,60%,.75)}div#p>svg>foreignObject>section.invert code,div#p>svg>foreignObject>section.invert kbd{background-color:#111}div#p>svg>foreignObject>section.invert kbd{border-color:#666;box-shadow:inset 0 -1px 0 #555;color:#e6eaf0}div#p>svg>foreignObject>section.invert table tr{background-color:#12181d;border-color:#60657b}div#p>svg>foreignObject>section.invert table tr:nth-child(2n){background-color:#1b2024}div#p>svg>foreignObject>section.invert table td,div#p>svg>foreignObject>section.invert table th{border-color:#5b5e61}div#p>svg>foreignObject>section.invert pre{background-color:#0a0e12;border-color:#777}div#p>svg>foreignObject>section.invert pre code{background-color:transparent}div#p>svg>foreignObject>section[data-color] h1,div#p>svg>foreignObject>section[data-color] h2,div#p>svg>foreignObject>section[data-color] h3,div#p>svg>foreignObject>section[data-color] h4,div#p>svg>foreignObject>section[data-color] h5,div#p>svg>foreignObject>section[data-color] h6{color:currentColor}div#p>svg>foreignObject>section{width:1280px;height:720px}div#p>svg>foreignObject>section{background-color:#FFFFFF;font-size:28px;color:#4b4b4b;font-family:"Droid Sans Mono","Hiragino Maru Gothic ProN";background-image:url("logo.svg");background-position:right 3% bottom 2%;background-repeat:no-repeat;background-attachment:5%;background-size:20% auto}div#p>svg>foreignObject>section{--marpit-root-font-size:28px}div#p>svg>foreignObject>section.title h1{color:#808db5;text-align:center}div#p>svg>foreignObject>section.title p{bottom:25%;width:100%;position:absolute;font-size:25px;color:#4b4b4b;background:linear-gradient(transparent 90%,#ffcc00 0%)}div#p>svg>foreignObject>section.slide h1{width:95%;color:white;background-color:#808db5;position:absolute;left:50px;top:35px}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{columns:initial!important;display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-class="title" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="title" data-marpit-pagination="1" data-marpit-pagination-total="26" style="--paginate:true;--class:title;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による <br /> Left Learning Red Black Tree の検証</h1> + +<p>Uechi Yuto, Shinji Kono 琉球大学</p> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>証明を用いてプログラムの信頼性の向上を目指す</h1> + +<ul> +<li>プログラムの信頼性を高めることは重要な課題である +<ul> +<li>信頼性を高める手法として「モデル検査」や「定理証明」など</li> +</ul> +</li> +<li>当研究室でCbCという言語を開発している +<ul> +<li>C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる</li> +</ul> +</li> +<li>先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った</li> +<li>本研究では Gears Agda にて重要なアルゴリズムの一つである Red Black Tree を検証する</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>CbC について</h1> +<ul> +<li>CbCとは当研究室で開発しているC言語の下位言語 +<ul> +<li>CbC とは C 言語からループ制御構造とサブルーチンコールを取り除き、継続を導入したC 言語の下位言語</li> +<li>継続呼び出しは引数付き goto 文で表現される。</li> +<li>処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語</li> +</ul> +</li> +<li>CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Agda の基本</h1> +<ul> +<li>Agdaとは定理証明支援器であり、関数型言語である</li> +<li>Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述できる +<ul> +<li>これが Curry-Howard 対応となる</li> +</ul> +</li> +<li>型の定義部分で、入力と出力の型を定義できる +<ul> +<li>input → output のようになる</li> +</ul> +</li> +<li>関数の定義は = を用いて行う +<ul> +<li>関数名の後、 = の前で受け取る引数を記述します</li> +</ul> +</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>sample1 : (A : Set ) → Set +sample1 a = a + +sample2 : (A : Set ) → (B : Set ) → Set +sample2 a b = b +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="5" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Agda の基本 record</h1> +<ul> +<li>2つのものが同時に存在すること</li> +<li>Record 型とはオブジェクトあるいは構造体のようなもの</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>record Env : Set where + field + varn : N + vari : N +open Env +</span></span></foreignObject></svg></code></pre> +<p>記述する際の基本的な例を以下に挙げる</p> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>record {varx = zero ; vary = suc zero} +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Agda の基本 data</h1> +<ul> +<li>一つでも存在すること</li> +<li>どちらかが成り立つ型を Data 型 で書く</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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 +</span></span></foreignObject></svg></code></pre> +<p>記述する際の基本的な例を以下に挙げる</p> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>datasample : bt → N +datasample leaf = zero +datasample (node key value left right) = suc zero +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="7" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Agda の基本 短縮記法</h1> +<ul> +<li>with を使用することでその変数のパターンマッチすることもできる</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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 } +</span></span></foreignObject></svg></code></pre> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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) } +</span></span></foreignObject></svg></code></pre> +<ul> +<li>... | `を使用することで関数の定義部分を省略できる</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>patternmatch-extraction' : env → N +patternmatch-extraction' env with varn env +... | zero = vari env +... | suc n = patternmatch-default' record { varn = n ; vari = suc (vari env) } +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="8" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda の記法</h1> +<ul> +<li>Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない +<ul> +<li>Agda で実装を行う際には再帰呼び出しを行わないようにする。</li> +</ul> +</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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 }) +</span></span></foreignObject></svg></code></pre> +<ul> +<li><code>→ t</code> で Set に遷移させるようにし、この後に関数が続くことと、関数を tail call していることで Continuation を定義している</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="9" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda と Gears CbC の対応 x</h1> +<ul> +<li> +<p>証明のしやすいGears Agda で実装を行いながらContext単位で同時に検証も行う</p> +</li> +<li> +<p>Gears Agda は検証向きの実装となり、CbCでは高速な実行向きとなる</p> +</li> +<li> +<p>Gears Agda での検証がCbCによる高速な実行の信頼性となる</p> +</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="10" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Normal level と Meta Level を用いた信頼性の向上</h1> +<p>CbCのプログラムの実行部分は以下の2つから構成される</p> +<ul> +<li>Normal Level は軽量継続で関数型プログラミングとなる +<ul> +<li>atomicってなんだろう</li> +<li>ポインタの操作はここでは行わず Meta Level にて行う</li> +</ul> +</li> +<li>Meta Level では信頼性を保証するために必要な計算を行う +<ul> +<li>メモリやCPUなどの資源管理</li> +<li>context</li> +<li>証明</li> +<li>並列実行（他のプロセスとの干渉）</li> +<li>monad</li> +</ul> +</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="11" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>s</h1> +<div src="meta-cg-dg.pdf"> </div> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="12" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Hoare Logic について</h1> +<ul> +<li>Hoare Logic とは C.A.R Hoare, R.W Floyd が考案したプログラムの検証の手法</li> +<li>「プログラムの事前条件 (P) が成立しているときコマンド (C) 実行して停止すると事後条件 (Q) が成り立つ」というもの +<ul> +<li>CbC の実行を継続するという性質に非常に相性が良い</li> +</ul> +</li> +</ul> +<p>pre/post condition を Gears Agda では Meta Input Data Gear として<br /> +プログラム中に遷移させていくことで、プログラムが終始仕様に沿った動きをしている<br /> +ことを検証する</p> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="13" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による検証の例（実装）</h1> +<ul> +<li>while program の検証を例に挙げる +<ul> +<li>以下は実装部分のコードとなる</li> +</ul> +</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>{-# 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 +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="14" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による検証の例（検証付き実装）</h1> +<ul> +<li>先ほど実装した while program に対して証明を付ける</li> +<li>loop を接続する Meta Gear も用意する</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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 +</span></span></foreignObject></svg></code></pre> +<ul> +<li>入力として仕様の証明を受け取る</li> +<li>出力として次の関数に仕様の証明を渡す</li> +<li>Hoare Conditionがプログラムの開始から停止するまで接続されていれば証明は完成 +<ul> +<li>Meta Gear にて証明を値としてあたえているため</li> +</ul> +</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="15" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>test との違い</h1> +<ul> +<li>test では実数を与えた際の出力が仕様に沿ったものであるかを検証する +<ul> +<li>コーナーケースで仕様に沿った動きをしていない場合を考慮できない</li> +</ul> +</li> +<li>今回の定理証明を用いた証明では実数を必要としない +<ul> +<li>そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる</li> +</ul> +</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="16" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による BinaryTree の実装</h1> +<ul> +<li>Agdaが変数への再代入を許していないためそのままでは木構造を実装できない +<ul> +<li>木構造を辿る際に現在いるノード以下の木構造をそのまま stack に格納する</li> +<li>replace / delete などの操作を行った後に stack を参照し Tree を再構築する</li> +<li>CbCへの変換の時に問題になりそうな予感</li> +</ul> +</li> +<li>ここの説明いらないかも？</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による BinaryTree の実装 find node</h1> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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) +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="18" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による BinaryTree の実装 replace node</h1> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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 +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="19" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による BinaryTree の実装 loop connecter</h1> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap> +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="20" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による Binary Tree の検証 Invariant</h1> +<p>具体的な例を一つ挙げて、Invariantの説明を行う</p> +<ul> +<li>Binary Tree の性質である、左の子のkeyは親より小さく、<br /> +右の子のkeyは親より大きいことを検証</li> +<li>Stack に格納されているTreeはその次のStackの減少列になっているか</li> +<li>Tree を正しく入れ替えられているか</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="21" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による Binary Tree の検証 Invariant</h1> +<ul> +<li>Tree Invariant</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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₄)) +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="22" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による Binary Tree の検証 Invariant</h1> +<ul> +<li>Stack Invariant</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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) +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="23" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による Binary Tree の検証 Invariant</h1> +<ul> +<li>Replace Invariant</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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) +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="24" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>Gears Agda による Binary Tree の検証</h1> +<p>Binary Tree の実装に対して上述した3つのInvariantを<br /> +Meta Data Gear として渡しながら実行できるように記述する</p> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>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 +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="25" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="25" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>今後の研究方針</h1> +<ul> +<li>現在は Binary Tree の検証までしか行えていないが、<br /> +今回定義した条件はそのまま Red Black Tree の検証に使用できるはず</li> +<li>今後は Gears Agda による実装と条件の追加をおこなう</li> +<li>モデル検査</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-class="slide" data-theme="default" data-style="section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="26" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + background-color: #FFFFFF; + font-size: 28px; + color: #4b4b4b; + font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; + background-image: url("logo.svg"); + background-position: right 3% bottom 2%; + background-repeat: no-repeat; + background-attachment: 5%; + background-size: 20% auto; +} + + section.title h1 { + color: #808db5; + text-align: center; + } + + section.title p { + bottom: 25%; + width: 100%; + position: absolute; + font-size: 25px; + color: #4b4b4b; + background: linear-gradient(transparent 90%, #ffcc00 0%); + } + +section.slide h1 { + width: 95%; + color: white; + background-color: #808db5; + position: absolute; + left: 50px; + top: 35px; +} +;--heading-divider:1;" data-size="16:9"> +<h1>まとめ</h1> +<ul> +<li>Gears Agda にて Binary Tree を検証することができた +<ul> +<li>Gears Agda における Termination を使用しない実装の仕方を確率した</li> +<li>Hoare Logic による検証もできるようになった</li> +<li>今後は Red Black Tree の検証をすすめる</li> +</ul> +</li> +<li>モデル検査をしたい</li> +</ul> +<p>英語版も欲しい</p> +<p>condition を テンプレみたいに作ってかきやすくする話</p> +</section> +<script>!function(){"use strict";const t="marpitSVGPolyfill:setZoomFactor,",e=Symbol();let r,o;function n(n){const i="object"==typeof n&&n.target||document,a="object"==typeof n?n.zoom:n;window[e]||(Object.defineProperty(window,e,{configurable:!0,value:!0}),window.addEventListener("message",(({data:e,origin:r})=>{if(r===window.origin)try{if(e&&"string"==typeof e&&e.startsWith(t)){const[,t]=e.split(","),r=Number.parseFloat(t);Number.isNaN(r)||(o=r)}}catch(t){console.error(t)}})));let l=!1;Array.from(i.querySelectorAll("svg[data-marpit-svg]"),(t=>{var e,n,i,s;t.style.transform||(t.style.transform="translateZ(0)");const c=a||o||t.currentScale||1;r!==c&&(r=c,l=c);const d=t.getBoundingClientRect(),{length:u}=t.children;for(let r=0;r<u;r+=1){const o=t.children[r],a=o.getScreenCTM();if(a){const t=null!==(n=null===(e=o.x)||void 0===e?void 0:e.baseVal.value)&&void 0!==n?n:0,r=null!==(s=null===(i=o.y)||void 0===i?void 0:i.baseVal.value)&&void 0!==s?s:0,l=o.firstElementChild,{style:u}=l;u.transformOrigin||(u.transformOrigin=`${-t}px ${-r}px`),u.transform=`scale(${c}) matrix(${a.a}, ${a.b}, ${a.c}, ${a.d}, ${a.e-d.left}, ${a.f-d.top}) translateZ(0.0001px)`}}})),!1!==l&&Array.from(i.querySelectorAll("iframe"),(({contentWindow:e})=>{null==e||e.postMessage(`${t}${l}`,"null"===window.origin?"*":window.origin)}))}r=1,o=void 0;const i=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function a({once:t=!1,target:e=document}={}){const r="Apple Computer, Inc."===navigator.vendor?[n]:[];let o=!t;const a=()=>{for(const t of r)t({target:e});!function(t=document){Array.from(t.querySelectorAll('svg[data-marp-fitting="svg"]'),(t=>{var e;const r=t.firstChild,o=r.firstChild,{scrollWidth:n,scrollHeight:a}=o;let l,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(l=null===(e=t.parentElement)||void 0===e?void 0:e.parentElement),t.hasAttribute("data-marp-fitting-math")&&(l=t.parentElement),l){const t=getComputedStyle(l),e=Math.ceil(l.clientWidth-parseFloat(t.paddingLeft||"0")-parseFloat(t.paddingRight||"0"));e&&(s=e)}const c=Math.max(n,s),d=Math.max(a,1),u=`0 0 ${c} ${d}`;i(r,"width",`${c}`),i(r,"height",`${d}`),i(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),i(t,"viewBox",u)&&t.classList.toggle("__reflow__")}))}(e),o&&window.requestAnimationFrame(a)};return a(),()=>{o=!1}}const l=Symbol(),s=document.currentScript;((t=document)=>{if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");if(t[l])return t[l];const e=a({target:t}),r=()=>{e(),delete t[l]};Object.defineProperty(t,l,{configurable:!0,value:r})})(s?s.getRootNode():document)}(); +</script></foreignObject></svg></div><div class="bespoke-marp-note" data-index="1" tabindex="0"><p>研究目的</p></div><div class="bespoke-marp-note" data-index="13" tabindex="0"><p>コードの解説 +あとで…</p></div><div class="bespoke-marp-note" data-index="16" tabindex="0"><p>findは全部書いても大丈夫そう</p></div><div class="bespoke-marp-note" data-index="17" tabindex="0"><p>これは途中省略してよさそう</p></div><div class="bespoke-marp-note" data-index="20" tabindex="0"><p>コードの解説 +省略した方がたぶん絶対良い +right と left なんかはほとんど対照的なので省略とかでよさそう +あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう</p></div><script>/*!! License: https://unpkg.com/@marp-team/marp-cli@1.5.0/lib/bespoke.js.LICENSE.txt */ +!function(){"use strict";const e=document.body,t=(...e)=>history.replaceState(...e),n="presenter",r="next",o=["",n,r],a="data-bespoke-marp-",i=(e,{protocol:t,host:n,pathname:r,hash:o}=location)=>{const a=e.toString();return`${t}//${n}${r}${a?"?":""}${a}${o}`},s=()=>e.dataset.bespokeView,l=e=>new URLSearchParams(location.search).get(e),c=(e,n={})=>{var r;const o={location,setter:t,...n},a=new URLSearchParams(o.location.search);for(const t of Object.keys(e)){const n=e[t];"string"==typeof n?a.set(t,n):a.delete(t)}try{o.setter({...null!==(r=window.history.state)&&void 0!==r?r:{}},"",i(a,o.location))}catch(e){console.error(e)}},d=(()=>{const e="bespoke-marp";try{return localStorage.setItem(e,e),localStorage.removeItem(e),!0}catch(e){return!1}})(),f=e=>{try{return localStorage.getItem(e)}catch(e){return null}},u=(e,t)=>{try{return localStorage.setItem(e,t),!0}catch(e){return!1}},m=e=>{try{return localStorage.removeItem(e),!0}catch(e){return!1}},g=(e,t)=>{const n="aria-hidden";t?e.setAttribute(n,"true"):e.removeAttribute(n)},p=e=>{e.parent.classList.add("bespoke-marp-parent"),e.slides.forEach((e=>e.classList.add("bespoke-marp-slide"))),e.on("activate",(t=>{const n="bespoke-marp-active",r=t.slide,o=r.classList,a=!o.contains(n);if(e.slides.forEach((e=>{e.classList.remove(n),g(e,!0)})),o.add(n),g(r,!1),a){const e=`${n}-ready`;o.add(e),document.body.clientHeight,o.remove(e)}}))},v=e=>{let t=0,n=0;Object.defineProperty(e,"fragments",{enumerable:!0,value:e.slides.map((e=>[null,...e.querySelectorAll("[data-marpit-fragment]")]))});const r=r=>void 0!==e.fragments[t][n+r],o=(r,o)=>{t=r,n=o,e.fragments.forEach(((e,t)=>{e.forEach(((e,n)=>{if(null==e)return;const i=t<r||t===r&&n<=o;e.setAttribute(`${a}fragment`,(i?"":"in")+"active");const s=`${a}current-fragment`;t===r&&n===o?e.setAttribute(s,"current"):e.removeAttribute(s)}))})),e.fragmentIndex=o;const i={slide:e.slides[r],index:r,fragments:e.fragments[r],fragmentIndex:o};e.fire("fragment",i)};e.on("next",(({fragment:a=!0})=>{if(a){if(r(1))return o(t,n+1),!1;const a=t+1;e.fragments[a]&&o(a,0)}else{const r=e.fragments[t].length;if(n+1<r)return o(t,r-1),!1;const a=e.fragments[t+1];a&&o(t+1,a.length-1)}})),e.on("prev",(({fragment:a=!0})=>{if(r(-1)&&a)return o(t,n-1),!1;const i=t-1;e.fragments[i]&&o(i,e.fragments[i].length-1)})),e.on("slide",(({index:t,fragment:n})=>{let r=0;if(void 0!==n){const o=e.fragments[t];if(o){const{length:e}=o;r=-1===n?e-1:Math.min(Math.max(n,0),e-1)}}o(t,r)})),o(0,0)},h=document,y=()=>!(!h.fullscreenEnabled&&!h.webkitFullscreenEnabled),x=()=>!(!h.fullscreenElement&&!h.webkitFullscreenElement),w=e=>{e.fullscreen=()=>{y()&&(async()=>{return x()?null===(e=h.exitFullscreen||h.webkitExitFullscreen)||void 0===e?void 0:e.call(h):((e=h.body)=>{var t;return null===(t=e.requestFullscreen||e.webkitRequestFullscreen)||void 0===t?void 0:t.call(e)})();var e})()},document.addEventListener("keydown",(t=>{"f"!==t.key&&"F11"!==t.key||t.altKey||t.ctrlKey||t.metaKey||!y()||(e.fullscreen(),t.preventDefault())}))},b="bespoke-marp-inactive",k=(e=2e3)=>({parent:t,fire:n})=>{const r=t.classList,o=e=>n(`marp-${e?"":"in"}active`);let a;const i=()=>{a&&clearTimeout(a),a=setTimeout((()=>{r.add(b),o()}),e),r.contains(b)&&(r.remove(b),o(!0))};for(const e of["mousedown","mousemove","touchend"])document.addEventListener(e,i);setTimeout(i,0)},E=["AUDIO","BUTTON","INPUT","SELECT","TEXTAREA","VIDEO"],L=e=>{e.parent.addEventListener("keydown",(e=>{if(!e.target)return;const t=e.target;(E.includes(t.nodeName)||"true"===t.contentEditable)&&e.stopPropagation()}))},$=e=>{window.addEventListener("load",(()=>{for(const t of e.slides){const e=t.querySelector("[data-marp-fitting]")?"":"hideable";t.setAttribute(`${a}load`,e)}}))},P=({interval:e=250}={})=>t=>{document.addEventListener("keydown",(e=>{if(" "===e.key&&e.shiftKey)t.prev();else if("ArrowLeft"===e.key||"ArrowUp"===e.key||"PageUp"===e.key)t.prev({fragment:!e.shiftKey});else if(" "!==e.key||e.shiftKey)if("ArrowRight"===e.key||"ArrowDown"===e.key||"PageDown"===e.key)t.next({fragment:!e.shiftKey});else if("End"===e.key)t.slide(t.slides.length-1,{fragment:-1});else{if("Home"!==e.key)return;t.slide(0)}else t.next();e.preventDefault()}));let n,r,o=0;t.parent.addEventListener("wheel",(a=>{let i=!1;const s=(e,t)=>{e&&(i=i||((e,t)=>((e,t)=>{const n="X"===t?"Width":"Height";return e[`client${n}`]<e[`scroll${n}`]})(e,t)&&((e,t)=>{const{overflow:n}=e,r=e[`overflow${t}`];return"auto"===n||"scroll"===n||"auto"===r||"scroll"===r})(getComputedStyle(e),t))(e,t)),(null==e?void 0:e.parentElement)&&s(e.parentElement,t)};if(0!==a.deltaX&&s(a.target,"X"),0!==a.deltaY&&s(a.target,"Y"),i)return;a.preventDefault();const l=Math.sqrt(a.deltaX**2+a.deltaY**2);if(void 0!==a.wheelDelta){if(void 0===a.webkitForce&&Math.abs(a.wheelDelta)<40)return;if(a.deltaMode===a.DOM_DELTA_PIXEL&&l<4)return}else if(a.deltaMode===a.DOM_DELTA_PIXEL&&l<12)return;r&&clearTimeout(r),r=setTimeout((()=>{n=0}),e);const c=Date.now()-o<e,d=l<=n;if(n=l,c||d)return;let f;(a.deltaX>0||a.deltaY>0)&&(f="next"),(a.deltaX<0||a.deltaY<0)&&(f="prev"),f&&(t[f](),o=Date.now())}))},S=(e=".bespoke-marp-osc")=>{const t=document.querySelector(e);if(!t)return()=>{};const n=(e,n)=>{t.querySelectorAll(`[${a}osc=${JSON.stringify(e)}]`).forEach(n)};return y()||n("fullscreen",(e=>e.style.display="none")),d||n("presenter",(e=>{e.disabled=!0,e.title="Presenter view is disabled due to restricted localStorage."})),e=>{t.addEventListener("click",(t=>{if(t.target instanceof HTMLElement){const{bespokeMarpOsc:n}=t.target.dataset;n&&t.target.blur();const r={fragment:!t.shiftKey};"next"===n?e.next(r):"prev"===n?e.prev(r):"fullscreen"===n?null==e||e.fullscreen():"presenter"===n&&e.openPresenterView()}})),e.parent.appendChild(t),e.on("activate",(({index:t})=>{n("page",(n=>n.textContent=`Page ${t+1} of ${e.slides.length}`))})),e.on("fragment",(({index:t,fragments:r,fragmentIndex:o})=>{n("prev",(e=>e.disabled=0===t&&0===o)),n("next",(n=>n.disabled=t===e.slides.length-1&&o===r.length-1))})),e.on("marp-active",(()=>g(t,!1))),e.on("marp-inactive",(()=>g(t,!0))),y()&&(e=>{for(const t of["","webkit"])h.addEventListener(t+"fullscreenchange",e)})((()=>n("fullscreen",(e=>e.classList.toggle("exit",y()&&x())))))}},I=e=>{window.addEventListener("message",(t=>{if(t.origin!==window.origin)return;const[n,r]=t.data.split(":");if("navigate"===n){const[t,n]=r.split(",");let o=Number.parseInt(t,10),a=Number.parseInt(n,10)+1;a>=e.fragments[o].length&&(o+=1,a=0),e.slide(o,{fragment:a})}}))};var T=["area","base","br","col","command","embed","hr","img","input","keygen","link","meta","param","source","track","wbr"];let A=e=>String(e).replace(/[&<>"']/g,(e=>`&${C[e]};`)),C={"&":"amp","<":"lt",">":"gt",'"':"quot","'":"apos"},N="dangerouslySetInnerHTML",K={className:"class",htmlFor:"for"},O={};function D(e,t){let n=[],r="";t=t||{};for(let e=arguments.length;e-- >2;)n.push(arguments[e]);if("function"==typeof e)return t.children=n.reverse(),e(t);if(e){if(r+="<"+e,t)for(let e in t)!1!==t[e]&&null!=t[e]&&e!==N&&(r+=` ${K[e]?K[e]:A(e)}="${A(t[e])}"`);r+=">"}if(-1===T.indexOf(e)){if(t[N])r+=t[N].__html;else for(;n.length;){let e=n.pop();if(e)if(e.pop)for(let t=e.length;t--;)n.push(e[t]);else r+=!0===O[e]?e:A(e)}r+=e?`</${e}>`:""}return O[r]=!0,r}const M=({children:e})=>D(null,null,...e),q="bespoke-marp-presenter-",_={container:`${q}container`,next:`${q}next`,nextContainer:`${q}next-container`,noteContainer:`${q}note-container`,infoContainer:`${q}info-container`,infoPage:`${q}info-page`,infoPageText:`${q}info-page-text`,infoPagePrev:`${q}info-page-prev`,infoPageNext:`${q}info-page-next`,infoTime:`${q}info-time`,infoTimer:`${q}info-timer`},U=e=>{const{title:t}=document;document.title="[Presenter view]"+(t?` - ${t}`:"");const n={},r=e=>(n[e]=n[e]||document.querySelector(`.${e}`),n[e]);document.body.appendChild((e=>{const t=document.createElement("div");return t.className=_.container,t.appendChild(e),t.insertAdjacentHTML("beforeend",D(M,null,D("div",{class:_.nextContainer},D("iframe",{class:_.next,src:"?view=next"})),D("div",{class:_.noteContainer}),D("div",{class:_.infoContainer},D("div",{class:_.infoPage},D("button",{class:_.infoPagePrev,tabindex:"-1",title:"Previous"},"Previous"),D("span",{class:_.infoPageText}),D("button",{class:_.infoPageNext,tabindex:"-1",title:"Next"},"Next")),D("time",{class:_.infoTime,title:"Current time"}),D("div",{class:_.infoTimer})))),t})(e.parent)),(e=>{r(_.nextContainer).addEventListener("click",(()=>e.next()));const t=r(_.next),n=(o=t,(e,t)=>{var n;return null===(n=o.contentWindow)||void 0===n?void 0:n.postMessage(`navigate:${e},${t}`,"null"===window.origin?"*":window.origin)});var o;t.addEventListener("load",(()=>{r(_.nextContainer).classList.add("active"),n(e.slide(),e.fragmentIndex),e.on("fragment",(({index:e,fragmentIndex:t})=>n(e,t)))}));const a=document.querySelectorAll(".bespoke-marp-note");a.forEach((e=>{e.addEventListener("keydown",(e=>e.stopPropagation())),r(_.noteContainer).appendChild(e)})),e.on("activate",(()=>a.forEach((t=>t.classList.toggle("active",t.dataset.index==e.slide()))))),e.on("activate",(({index:t})=>{r(_.infoPageText).textContent=`${t+1} / ${e.slides.length}`}));const i=r(_.infoPagePrev),s=r(_.infoPageNext);i.addEventListener("click",(t=>{i.blur(),e.prev({fragment:!t.shiftKey})})),s.addEventListener("click",(t=>{s.blur(),e.next({fragment:!t.shiftKey})})),e.on("fragment",(({index:t,fragments:n,fragmentIndex:r})=>{i.disabled=0===t&&0===r,s.disabled=t===e.slides.length-1&&r===n.length-1}));const l=()=>r(_.infoTime).textContent=(new Date).toLocaleTimeString();l(),setInterval(l,250)})(e)},V=e=>{if(!(e=>e.syncKey&&"string"==typeof e.syncKey)(e))throw new Error("The current instance of Bespoke.js is invalid for Marp bespoke presenter plugin.");Object.defineProperties(e,{openPresenterView:{enumerable:!0,value:X},presenterUrl:{enumerable:!0,get:F}}),d&&document.addEventListener("keydown",(t=>{"p"!==t.key||t.altKey||t.ctrlKey||t.metaKey||(t.preventDefault(),e.openPresenterView())}))};function X(){const{max:e,floor:t}=Math,n=e(t(.85*window.innerWidth),640),r=e(t(.85*window.innerHeight),360);return window.open(this.presenterUrl,q+this.syncKey,`width=${n},height=${r},menubar=no,toolbar=no`)}function F(){const e=new URLSearchParams(location.search);return e.set("view","presenter"),e.set("sync",this.syncKey),i(e)}const B=e=>{const t=s();return t===r&&e.appendChild(document.createElement("span")),{"":V,[n]:U,[r]:I}[t]},R=e=>{e.on("activate",(t=>{document.querySelectorAll(".bespoke-progress-parent > .bespoke-progress-bar").forEach((n=>{n.style.flexBasis=100*t.index/(e.slides.length-1)+"%"}))}))},j=e=>{const t=Number.parseInt(e,10);return Number.isNaN(t)?null:t},H=(e={})=>{const t={history:!0,...e};return e=>{let n=!0;const r=e=>{const t=n;try{return n=!0,e()}finally{n=t}},o=(t={fragment:!0})=>{((t,n)=>{const{min:r,max:o}=Math,{fragments:a,slides:i}=e,s=o(0,r(t,i.length-1)),l=o(0,r(n||0,a[s].length-1));s===e.slide()&&l===e.fragmentIndex||e.slide(s,{fragment:l})})((j(location.hash.slice(1))||1)-1,t.fragment?j(l("f")||""):null)};e.on("fragment",(({index:e,fragmentIndex:r})=>{n||c({f:0===r||r.toString()},{location:{...location,hash:`#${e+1}`},setter:(...e)=>t.history?history.pushState(...e):history.replaceState(...e)})})),setTimeout((()=>{o(),window.addEventListener("hashchange",(()=>r((()=>{o({fragment:!1}),c({f:void 0})})))),window.addEventListener("popstate",(()=>{n||r((()=>o()))})),n=!1}),0)}},Y=(e={})=>{var n;const r=e.key||(null===(n=window.history.state)||void 0===n?void 0:n.marpBespokeSyncKey)||Math.random().toString(36).slice(2),o=`bespoke-marp-sync-${r}`;var a;a={marpBespokeSyncKey:r},c({},{setter:(e,...n)=>t({...e,...a},...n)});const i=()=>{const e=f(o);return e?JSON.parse(e):Object.create(null)},s=e=>{const t=i(),n={...t,...e(t)};return u(o,JSON.stringify(n)),n},l=()=>{window.removeEventListener("pageshow",l),s((e=>({reference:(e.reference||0)+1})))};return e=>{l(),Object.defineProperty(e,"syncKey",{value:r,enumerable:!0});let t=!0;setTimeout((()=>{e.on("fragment",(e=>{t&&s((()=>({index:e.index,fragmentIndex:e.fragmentIndex})))}))}),0),window.addEventListener("storage",(n=>{if(n.key===o&&n.oldValue&&n.newValue){const r=JSON.parse(n.oldValue),o=JSON.parse(n.newValue);if(r.index!==o.index||r.fragmentIndex!==o.fragmentIndex)try{t=!1,e.slide(o.index,{fragment:o.fragmentIndex})}finally{t=!0}}}));const n=()=>{const{reference:e}=i();void 0===e||e<=1?m(o):s((()=>({reference:e-1})))};window.addEventListener("pagehide",(e=>{e.persisted&&window.addEventListener("pageshow",l),n()})),e.on("destroy",n)}},{PI:J,abs:W,sqrt:z,atan2:G}=Math,Q={passive:!0},Z=({slope:e=-.7,swipeThreshold:t=30}={})=>n=>{let r;const o=n.parent,a=e=>{const t=o.getBoundingClientRect();return{x:e.pageX-(t.left+t.right)/2,y:e.pageY-(t.top+t.bottom)/2}};o.addEventListener("touchstart",(({touches:e})=>{r=1===e.length?a(e[0]):void 0}),Q),o.addEventListener("touchmove",(e=>{if(r)if(1===e.touches.length){e.preventDefault();const t=a(e.touches[0]),n=t.x-r.x,o=t.y-r.y;r.delta=z(W(n)**2+W(o)**2),r.radian=G(n,o)}else r=void 0})),o.addEventListener("touchend",(o=>{if(r){if(r.delta&&r.delta>=t&&r.radian){const t=(r.radian-e+J)%(2*J)-J;n[t<0?"next":"prev"](),o.stopPropagation()}r=void 0}}),Q)},ee="_tA",te=e=>{const t=document.documentTransition;if(!t)return;let n;e._tP=!1;const r=(n,{back:r,cond:o})=>a=>{const i=e.slides[e.slide()].querySelector("section[data-transition]");if(!i)return!0;const s=document.querySelector(".bespoke-marp-osc"),l=s?[s]:void 0;if(e._tP){if(a._tA){e._tP=!1;try{t.start({sharedElements:l}).catch((()=>{}))}catch(e){}return!0}}else{if(!o(a))return!0;e._tP=t.prepare({rootTransition:a.back||r?i.dataset.transitionBack:i.dataset.transition,sharedElements:l}).then((()=>n(a))).catch((()=>n(a)))}return!1};e.on("prev",r((t=>e.prev({...t,[ee]:!0})),{back:!0,cond:e=>{var t;return e.index>0&&!((null===(t=e.fragment)||void 0===t||t)&&n.fragmentIndex>0)}})),e.on("next",r((t=>e.next({...t,[ee]:!0})),{cond:t=>t.index+1<e.slides.length&&!(n.fragmentIndex+1<n.fragments.length)})),setTimeout((()=>{e.on("slide",r((t=>e.slide(t.index,{...t,[ee]:!0})),{cond:t=>{const n=e.slide();return t.index!==n&&(t.back=t.index<n,!0)}}))}),0),e.on("fragment",(e=>{n=e}))};let ne;const re=()=>(void 0===ne&&(ne="wakeLock"in navigator&&navigator.wakeLock),ne),oe=async()=>{const e=re();if(e)try{return await e.request("screen")}catch(e){console.warn(e)}return null},ae=async()=>{if(!re())return;let e;const t=()=>{e&&"visible"===document.visibilityState&&oe()};for(const e of["visibilitychange","fullscreenchange"])document.addEventListener(e,t);return e=await oe(),e};((t=document.getElementById("p"))=>{(()=>{const t=l("view");e.dataset.bespokeView=t===r||t===n?t:""})();const a=(e=>{const t=l(e);return c({[e]:void 0}),t})("sync")||void 0;var i,d,f,u,m,g,h,y,x,b,E,I;i=t,d=((...e)=>{const t=o.findIndex((e=>s()===e));return e.map((([e,n])=>e[t]&&n)).filter((e=>e))})([[1,1,0],Y({key:a})],[[1,1,1],B(t)],[[1,1,0],L],[[1,1,1],p],[[1,0,0],k()],[[1,1,1],$],[[1,1,1],H({history:!1})],[[1,1,0],P()],[[1,1,0],w],[[1,0,0],R],[[1,1,0],Z()],[[1,0,0],S()],[[1,0,0],te],[[1,1,1],v],[[1,1,0],ae]),u=1===(i.parent||i).nodeType?i.parent||i:document.querySelector(i.parent||i),m=[].filter.call("string"==typeof i.slides?u.querySelectorAll(i.slides):i.slides||u.children,(function(e){return"SCRIPT"!==e.nodeName})),g={},h=function(e,t){return(t=t||{}).index=m.indexOf(e),t.slide=e,t},b=function(e,t){m[e]&&(f&&x("deactivate",h(f,t)),f=m[e],x("activate",h(f,t)))},E=function(e,t){var n=m.indexOf(f)+e;x(e>0?"next":"prev",h(f,t))&&b(n,t)},I={off:y=function(e,t){g[e]=(g[e]||[]).filter((function(e){return e!==t}))},on:function(e,t){return(g[e]||(g[e]=[])).push(t),y.bind(null,e,t)},fire:x=function(e,t){return(g[e]||[]).reduce((function(e,n){return e&&!1!==n(t)}),!0)},slide:function(e,t){if(!arguments.length)return m.indexOf(f);x("slide",h(m[e],t))&&b(e,t)},next:E.bind(null,1),prev:E.bind(null,-1),parent:u,slides:m,destroy:function(e){x("destroy",h(f,e)),g={}}},(d||[]).forEach((function(e){e(I)})),f||b(0)})()}();</script></body></html> \ No newline at end of file
--- /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 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" viewBox="17.5 287.5 585.3511 421.08984" width="585.3511" height="421.08984"> + <defs> + <font-face font-family="Helvetica" font-size="9" units-per-em="1000" underline-position="-75.68359" underline-thickness="49.316406" slope="0" x-height="522.9492" cap-height="717.28516" ascent="770.0195" descent="-229.98047" font-weight="400"> + <font-face-src> + <font-face-name name="Helvetica"/> + </font-face-src> + </font-face> + <font-face font-family="Helvetica Neue" font-size="12" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400"> + <font-face-src> + <font-face-name name="HelveticaNeue"/> + </font-face-src> + </font-face> + <font-face font-family="Helvetica" font-size="12" units-per-em="1000" underline-position="-75.68359" underline-thickness="49.316406" slope="0" x-height="522.9492" cap-height="717.28516" ascent="770.0195" descent="-229.98047" font-weight="400"> + <font-face-src> + <font-face-name name="Helvetica"/> + </font-face-src> + </font-face> + <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"> + <g> + <path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> + </g> + </marker> + </defs> + <metadata> Produced by OmniGraffle 7.19.2\n2022-01-06 02:09:09 +0000</metadata> + <g id="Canvas_1" stroke-opacity="1" stroke="none" stroke-dasharray="none" fill="none" fill-opacity="1"> + <title>Canvas 1</title> + <rect fill="white" x="17.5" y="287.5" width="585.3511" height="421.08984"/> + <g id="Canvas_1_Layer_1"> + <title>Layer 1</title> + <g id="Graphic_3"> + <text transform="translate(507.9492 692.58984)" fill="#945200"> + <tspan font-family="Helvetica" font-size="9" font-weight="400" fill="#945200" x="0" y="9"> </tspan> + </text> + </g> + <g id="Group_94"> + <g id="Graphic_96"> + <rect x="18" y="378" width="130.17553" height="90" fill="white"/> + <path d="M 18 378 L 148.17553 378 L 148.17553 468 L 18 468 Z" stroke="#ff9300" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/> + </g> + <g id="Graphic_95"> + <text transform="translate(38.798856 392)" fill="#c25800"> + <tspan font-family="Helvetica Neue" font-size="12" font-weight="400" fill="#c25800" x=".6286934" y="11">Meta Data Gear</tspan> + </text> + </g> + </g> + <g id="Group_91"> + <g id="Graphic_93"> + <rect x="472.17553" y="378" width="130.17553" height="90" fill="white"/> + <path d="M 472.17553 378 L 602.3511 378 L 602.3511 468 L 472.17553 468 Z" stroke="#ff9300" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/> + </g> + <g id="Graphic_92"> + <text transform="translate(492.9744 392)" fill="#c25800"> + <tspan font-family="Helvetica Neue" font-size="12" font-weight="400" fill="#c25800" x=".6286934" y="11">Meta Data Gear</tspan> + </text> + </g> + </g> + <g id="Graphic_121"> + <ellipse cx="310.17553" cy="436.5" rx="45.8794865380515" ry="22.5000359527927" fill="white"/> + <ellipse cx="310.17553" cy="436.5" rx="45.8794865380515" ry="22.5000359527927" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(278.472 429.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="2.353922" y="11">Code Gear</tspan> + </text> + </g> + <g id="Graphic_83"> + <rect x="45.65788" y="414" width="75.51765" height="45" fill="white"/> + <rect x="45.65788" y="414" width="75.51765" height="45" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(50.65788 429.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="5.07914" y="11">Data Gear</tspan> + </text> + </g> + <g id="Line_118"> + <line x1="121.67553" y1="436.5" x2="254.3961" y2="436.5" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="butt" stroke-linejoin="miter" stroke-width="1"/> + </g> + <g id="Graphic_120"> + <rect x="499.17553" y="414" width="75.51765" height="45" fill="white"/> + <rect x="499.17553" y="414" width="75.51765" height="45" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(504.17553 429.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="5.07914" y="11">Data Gear</tspan> + </text> + </g> + <g id="Line_116"> + <line x1="356.05497" y1="436.5" x2="488.77553" y2="436.5" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="butt" stroke-linejoin="miter" stroke-width="1"/> + </g> + <g id="Graphic_117"> + <ellipse cx="418.437" cy="436.5" rx="45.4435686903338" ry="22.5000359527927" fill="white"/> + <path d="M 450.57035 420.5901 C 468.3172 429.3769 468.3172 443.6231 450.57035 452.4099 C 432.82357 461.1967 404.0504 461.1967 386.3036 452.4099 C 368.55674 443.6231 368.55674 429.3769 386.3036 420.5901 C 404.0504 411.8033 432.82357 411.8033 450.57035 420.5901" stroke="#ff9300" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/> + <text transform="translate(387.0822 422.5)" fill="#c25800"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="#c25800" x="18.01593" y="11">Meta </tspan> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="#c25800" x="2.005188" y="25">Code Gear</tspan> + </text> + </g> + <g id="Graphic_103"> + <ellipse cx="310.17553" cy="310.5" rx="44.2896033411883" ry="22.5000359527927" fill="white"/> + <ellipse cx="310.17553" cy="310.5" rx="44.2896033411883" ry="22.5000359527927" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(279.7439 303.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="1.082016" y="11">Code Gear</tspan> + </text> + </g> + <g id="Graphic_104"> + <rect x="45.65788" y="288" width="75.51765" height="45" fill="white"/> + <rect x="45.65788" y="288" width="75.51765" height="45" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(50.65788 303.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="5.07914" y="11">Data Gear</tspan> + </text> + </g> + <g id="Line_105"> + <line x1="121.67553" y1="310.5" x2="255.98598" y2="310.5" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="butt" stroke-linejoin="miter" stroke-width="1"/> + </g> + <g id="Graphic_106"> + <rect x="499.17553" y="288" width="75.51765" height="45" fill="white"/> + <rect x="499.17553" y="288" width="75.51765" height="45" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(504.17553 303.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="5.07914" y="11">Data Gear</tspan> + </text> + </g> + <g id="Line_107"> + <line x1="354.4651" y1="310.5" x2="488.77553" y2="310.5" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="butt" stroke-linejoin="miter" stroke-width="1"/> + </g> + <g id="Graphic_122"> + <ellipse cx="200.39427" cy="436.5" rx="45.4435686903337" ry="22.5000359527927" fill="white"/> + <path d="M 232.52763 420.5901 C 250.2745 429.3769 250.2745 443.6231 232.52763 452.4099 C 214.78086 461.1967 186.00767 461.1967 168.2609 452.4099 C 150.51403 443.6231 150.51403 429.3769 168.2609 420.5901 C 186.00767 411.8033 214.78086 411.8033 232.52763 420.5901" stroke="#ff9300" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/> + <text transform="translate(169.03947 422.5)" fill="#c25800"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="#c25800" x="18.01593" y="11">Meta </tspan> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="#c25800" x="2.005188" y="25">Code Gear</tspan> + </text> + </g> + </g> + </g> +</svg>
--- 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 + # 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) +``` + +<!-- +findは全部書いても大丈夫そう +--> + +# 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₄)) +``` + +<!-- +コードの解説 +省略した方がたぶん絶対良い +right と left なんかはほとんど対照的なので省略とかでよさそう +あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう +--> + + +# 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 を テンプレみたいに作ってかきやすくする話 +