Mercurial > hg > Papers > 2019 > ryokka-sigss
changeset 11:17b7605a5deb
add figures, some slides
| author | ryokka |
|---|---|
| date | Sun, 13 Jan 2019 23:42:16 +0900 |
| parents | a87fec07fd78 |
| children | e8fe28afe61e |
| files | ryokka-sigss.mm slide/pic/cgdg-small.pdf slide/pic/cgdg-small.svg slide/pic/cgdg.svg slide/pic/codeGear_dataGear.pdf slide/pic/codeGear_dataGear.xbb slide/s6/themes/blank.css slide/slide.html slide/slide.md |
| diffstat | 9 files changed, 969 insertions(+), 333 deletions(-) [+] |
line wrap: on
line diff
--- a/ryokka-sigss.mm Sun Jan 13 03:51:48 2019 +0900 +++ b/ryokka-sigss.mm Sun Jan 13 23:42:16 2019 +0900 @@ -174,20 +174,42 @@ <node CREATED="1545031065628" ID="ID_457628232" MODIFIED="1545031085235" TEXT="証明をメタ計算の引数の受け渡しとして記述できた"/> </node> <node CREATED="1547296659423" ID="ID_1905231255" MODIFIED="1547296666872" POSITION="right" TEXT="Slide"> -<node CREATED="1547296673449" ID="ID_326097753" MODIFIED="1547296725921" TEXT="研究目的"/> +<node CREATED="1547296673449" ID="ID_326097753" MODIFIED="1547296725921" TEXT="研究目的"> +<node CREATED="1547386601688" ID="ID_658328866" MODIFIED="1547386671077" TEXT="OS とか アプリケーションの信頼性が高いことは重要である"/> +<node CREATED="1547386619947" ID="ID_464524492" MODIFIED="1547386747105" TEXT="検証をすることで動作を保証する→信頼性up"/> +<node CREATED="1547386632438" ID="ID_230254962" MODIFIED="1547387120710" TEXT="検証の手法として HoareLogic がある"> +<node CREATED="1547386919569" ID="ID_272380556" MODIFIED="1547387106641" TEXT="プログラム"/> +</node> +<node CREATED="1547387112461" ID="ID_1701764044" MODIFIED="1547387260803" TEXT="この方法は実際のプログラミング言語で使用できずあまりひろまっていない"/> +<node CREATED="1547387263080" ID="ID_721622245" MODIFIED="1547387313432" TEXT="当研究室では信頼性の高い OS として Gears OS を開発している"/> +</node> <node CREATED="1547296864709" ID="ID_450376854" MODIFIED="1547296873020" TEXT="Gears, GearsOS"> <node CREATED="1547297456269" ID="ID_1531966210" MODIFIED="1547297464129" TEXT="Gears って？"> -<node CREATED="1547297464134" ID="ID_870199224" MODIFIED="1547297644701" TEXT="当研究室で提案しているodeGear、 DataGear という単位でプログラミング"/> +<node CREATED="1547297464134" ID="ID_870199224" MODIFIED="1547298069746" TEXT="当研究室で提案しているodeGear、 DataGear という単位"/> <node CREATED="1547297503002" ID="ID_1634638250" MODIFIED="1547297649262" TEXT="処理の単位をGodeGear、 Dataの単位を DataGear とする"/> <node CREATED="1547297543828" ID="ID_833081910" MODIFIED="1547297650102" TEXT="CodeGear を継続してプログラミングをする"/> <node CREATED="1547297490386" ID="ID_901165581" MODIFIED="1547297720096" TEXT="継続は通常の言語の関数呼び出しとは異なり、現在の環境を破棄して次の CodeGear に遷移する"/> </node> -<node CREATED="1547297561929" ID="ID_271914428" MODIFIED="1547297580283" TEXT="GearsOS って？"> -<node CREATED="1547297725953" ID="ID_1462232623" MODIFIED="1547297725953" TEXT=""/> +<node CREATED="1547297561929" ID="ID_271914428" MODIFIED="1547298108614" TEXT="GearsOS って？"> +<icon BUILTIN="button_cancel"/> +<node CREATED="1547297725953" ID="ID_1462232623" MODIFIED="1547297756465" TEXT="先述の Gears という単位を用いて記述されているOS"/> +<node CREATED="1547297762474" ID="ID_466083659" MODIFIED="1547298056338" TEXT="信頼性の保証や拡張性をメタレベルの計算で実現することを目標に開発している"/> </node> </node> <node CREATED="1547296726482" ID="ID_1016327903" MODIFIED="1547296883972" TEXT="Gears と Agda"> -<node CREATED="1547297445639" ID="ID_38829678" MODIFIED="1547297451879" TEXT="Agda"/> +<node CREATED="1547297445639" ID="ID_38829678" MODIFIED="1547297451879" TEXT="Agda"> +<node CREATED="1547298122147" ID="ID_285257604" MODIFIED="1547298126197" TEXT="Agdaって？"/> +<node CREATED="1547298126865" ID="ID_741550943" MODIFIED="1547298133660" TEXT="どうやって書くものなの？"/> +<node CREATED="1547298224210" ID="ID_152235889" MODIFIED="1547298229439" TEXT="証明とか"> +<node CREATED="1547298191391" ID="ID_1481861598" MODIFIED="1547298305152" TEXT="証明の記述"/> +<node CREATED="1547298305512" ID="ID_884856006" MODIFIED="1547298310985" TEXT="証明の仕方"/> +<node CREATED="1547298311733" ID="ID_790203150" MODIFIED="1547298328602" TEXT="Reasoning の話"/> +</node> +</node> +<node CREATED="1547298136301" ID="ID_1183092589" MODIFIED="1547298142540" TEXT="Agda での Gears"> +<node CREATED="1547298143717" ID="ID_1947013376" MODIFIED="1547298211447" TEXT="CodeGear と DataGear の記述と対応"/> +<node CREATED="1547298183847" ID="ID_1681965835" MODIFIED="1547298261833" TEXT="CodeGear の証明"/> +</node> </node> <node CREATED="1547296742331" ID="ID_124842298" MODIFIED="1547296853787" TEXT="HoareLogic の説明 (in Agda)"> <node CREATED="1547297092738" ID="ID_547653717" MODIFIED="1547297100873" TEXT="HoareLogic の説明"/>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/pic/cgdg-small.svg Sun Jan 13 23:42:16 2019 +0900 @@ -0,0 +1,270 @@ +<?xml version="1.0" encoding="UTF-8"?> +<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="605.980469pt" height="219.6172pt" viewBox="0 0 605.980469 219.6172" version="1.1"> +<defs> +<g> +<symbol overflow="visible" id="glyph0-0"> +<path style="stroke:none;" d="M 4.90625 -7.984375 L 1.21875 -7.984375 L 1.21875 -0.5625 L 4.90625 -0.5625 Z M 5.515625 -8.546875 L 5.515625 -0.015625 L 0.609375 -0.015625 L 0.609375 -8.546875 Z M 5.515625 -8.546875 "/> +</symbol> +<symbol overflow="visible" id="glyph0-1"> +<path style="stroke:none;" d="M 0.953125 -8.5625 L 0.953125 0 L 2.046875 0 L 2.046875 -7.125 L 2.0625 -7.125 L 4.734375 0 L 5.71875 0 L 8.390625 -7.125 L 8.40625 -7.125 L 8.40625 0 L 9.484375 0 L 9.484375 -8.5625 L 7.9375 -8.5625 L 5.21875 -1.375 L 2.515625 -8.5625 Z M 0.953125 -8.5625 "/> +</symbol> +<symbol overflow="visible" id="glyph0-2"> +<path style="stroke:none;" d="M 5.078125 -3.703125 L 1.515625 -3.703125 C 1.523438 -3.941406 1.570312 -4.164062 1.65625 -4.375 C 1.75 -4.582031 1.867188 -4.765625 2.015625 -4.921875 C 2.171875 -5.085938 2.351562 -5.21875 2.5625 -5.3125 C 2.78125 -5.40625 3.019531 -5.453125 3.28125 -5.453125 C 3.539062 -5.453125 3.773438 -5.40625 3.984375 -5.3125 C 4.203125 -5.21875 4.390625 -5.09375 4.546875 -4.9375 C 4.703125 -4.78125 4.820312 -4.59375 4.90625 -4.375 C 5 -4.164062 5.054688 -3.941406 5.078125 -3.703125 Z M 6.0625 -1.96875 L 5.046875 -1.96875 C 4.960938 -1.5625 4.78125 -1.253906 4.5 -1.046875 C 4.226562 -0.847656 3.875 -0.75 3.4375 -0.75 C 3.101562 -0.75 2.8125 -0.804688 2.5625 -0.921875 C 2.320312 -1.035156 2.117188 -1.1875 1.953125 -1.375 C 1.796875 -1.5625 1.679688 -1.773438 1.609375 -2.015625 C 1.535156 -2.265625 1.503906 -2.523438 1.515625 -2.796875 L 6.15625 -2.796875 C 6.175781 -3.171875 6.140625 -3.566406 6.046875 -3.984375 C 5.960938 -4.398438 5.8125 -4.78125 5.59375 -5.125 C 5.375 -5.476562 5.082031 -5.769531 4.71875 -6 C 4.351562 -6.226562 3.894531 -6.34375 3.34375 -6.34375 C 2.925781 -6.34375 2.535156 -6.265625 2.171875 -6.109375 C 1.816406 -5.953125 1.507812 -5.726562 1.25 -5.4375 C 0.988281 -5.144531 0.785156 -4.800781 0.640625 -4.40625 C 0.503906 -4.019531 0.4375 -3.59375 0.4375 -3.125 C 0.445312 -2.644531 0.515625 -2.207031 0.640625 -1.8125 C 0.765625 -1.414062 0.953125 -1.070312 1.203125 -0.78125 C 1.453125 -0.488281 1.753906 -0.265625 2.109375 -0.109375 C 2.472656 0.046875 2.90625 0.125 3.40625 0.125 C 4.113281 0.125 4.695312 -0.046875 5.15625 -0.390625 C 5.625 -0.742188 5.925781 -1.269531 6.0625 -1.96875 Z M 6.0625 -1.96875 "/> +</symbol> +<symbol overflow="visible" id="glyph0-3"> +<path style="stroke:none;" d="M 2.1875 -6.203125 L 2.1875 -8.0625 L 1.15625 -8.0625 L 1.15625 -6.203125 L 0.109375 -6.203125 L 0.109375 -5.296875 L 1.15625 -5.296875 L 1.15625 -1.359375 C 1.15625 -1.066406 1.179688 -0.832031 1.234375 -0.65625 C 1.296875 -0.476562 1.382812 -0.34375 1.5 -0.25 C 1.625 -0.15625 1.78125 -0.0859375 1.96875 -0.046875 C 2.15625 -0.015625 2.378906 0 2.640625 0 L 3.421875 0 L 3.421875 -0.90625 L 2.953125 -0.90625 C 2.796875 -0.90625 2.664062 -0.910156 2.5625 -0.921875 C 2.457031 -0.929688 2.378906 -0.957031 2.328125 -1 C 2.273438 -1.039062 2.238281 -1.09375 2.21875 -1.15625 C 2.195312 -1.226562 2.1875 -1.328125 2.1875 -1.453125 L 2.1875 -5.296875 L 3.421875 -5.296875 L 3.421875 -6.203125 Z M 2.1875 -6.203125 "/> +</symbol> +<symbol overflow="visible" id="glyph0-4"> +<path style="stroke:none;" d="M 6.265625 -0.03125 C 6.085938 0.0703125 5.84375 0.125 5.53125 0.125 C 5.269531 0.125 5.0625 0.0507812 4.90625 -0.09375 C 4.75 -0.238281 4.671875 -0.476562 4.671875 -0.8125 C 4.390625 -0.476562 4.0625 -0.238281 3.6875 -0.09375 C 3.3125 0.0507812 2.910156 0.125 2.484375 0.125 C 2.203125 0.125 1.9375 0.09375 1.6875 0.03125 C 1.4375 -0.03125 1.21875 -0.128906 1.03125 -0.265625 C 0.84375 -0.398438 0.695312 -0.578125 0.59375 -0.796875 C 0.488281 -1.015625 0.4375 -1.28125 0.4375 -1.59375 C 0.4375 -1.945312 0.492188 -2.234375 0.609375 -2.453125 C 0.734375 -2.679688 0.890625 -2.863281 1.078125 -3 C 1.273438 -3.144531 1.5 -3.253906 1.75 -3.328125 C 2.007812 -3.398438 2.269531 -3.457031 2.53125 -3.5 C 2.8125 -3.5625 3.078125 -3.601562 3.328125 -3.625 C 3.578125 -3.65625 3.796875 -3.695312 3.984375 -3.75 C 4.179688 -3.800781 4.335938 -3.875 4.453125 -3.96875 C 4.566406 -4.070312 4.625 -4.222656 4.625 -4.421875 C 4.625 -4.640625 4.582031 -4.816406 4.5 -4.953125 C 4.414062 -5.085938 4.304688 -5.191406 4.171875 -5.265625 C 4.035156 -5.335938 3.882812 -5.382812 3.71875 -5.40625 C 3.5625 -5.4375 3.398438 -5.453125 3.234375 -5.453125 C 2.804688 -5.453125 2.445312 -5.367188 2.15625 -5.203125 C 1.875 -5.035156 1.71875 -4.722656 1.6875 -4.265625 L 0.671875 -4.265625 C 0.691406 -4.648438 0.769531 -4.972656 0.90625 -5.234375 C 1.050781 -5.503906 1.242188 -5.71875 1.484375 -5.875 C 1.722656 -6.039062 1.992188 -6.160156 2.296875 -6.234375 C 2.609375 -6.304688 2.941406 -6.34375 3.296875 -6.34375 C 3.578125 -6.34375 3.851562 -6.320312 4.125 -6.28125 C 4.40625 -6.25 4.65625 -6.171875 4.875 -6.046875 C 5.101562 -5.921875 5.285156 -5.742188 5.421875 -5.515625 C 5.554688 -5.296875 5.625 -5.003906 5.625 -4.640625 L 5.625 -1.453125 C 5.625 -1.210938 5.640625 -1.035156 5.671875 -0.921875 C 5.703125 -0.804688 5.796875 -0.75 5.953125 -0.75 C 6.035156 -0.75 6.140625 -0.769531 6.265625 -0.8125 Z M 4.609375 -3.203125 C 4.484375 -3.109375 4.316406 -3.035156 4.109375 -2.984375 C 3.898438 -2.941406 3.679688 -2.90625 3.453125 -2.875 C 3.222656 -2.851562 2.988281 -2.820312 2.75 -2.78125 C 2.519531 -2.75 2.3125 -2.691406 2.125 -2.609375 C 1.945312 -2.535156 1.800781 -2.421875 1.6875 -2.265625 C 1.570312 -2.117188 1.515625 -1.921875 1.515625 -1.671875 C 1.515625 -1.503906 1.546875 -1.359375 1.609375 -1.234375 C 1.679688 -1.117188 1.769531 -1.023438 1.875 -0.953125 C 1.988281 -0.890625 2.113281 -0.835938 2.25 -0.796875 C 2.394531 -0.765625 2.550781 -0.75 2.71875 -0.75 C 3.050781 -0.75 3.335938 -0.796875 3.578125 -0.890625 C 3.816406 -0.984375 4.007812 -1.097656 4.15625 -1.234375 C 4.3125 -1.378906 4.425781 -1.53125 4.5 -1.6875 C 4.570312 -1.851562 4.609375 -2.007812 4.609375 -2.15625 Z M 4.609375 -3.203125 "/> +</symbol> +<symbol overflow="visible" id="glyph0-5"> +<path style="stroke:none;" d=""/> +</symbol> +<symbol overflow="visible" id="glyph0-6"> +<path style="stroke:none;" d="M 2.078125 -0.953125 L 2.078125 -7.609375 L 4 -7.609375 C 4.519531 -7.609375 4.960938 -7.53125 5.328125 -7.375 C 5.691406 -7.226562 5.984375 -7.015625 6.203125 -6.734375 C 6.429688 -6.453125 6.597656 -6.109375 6.703125 -5.703125 C 6.804688 -5.296875 6.859375 -4.835938 6.859375 -4.328125 C 6.859375 -3.804688 6.800781 -3.359375 6.6875 -2.984375 C 6.582031 -2.609375 6.445312 -2.296875 6.28125 -2.046875 C 6.113281 -1.804688 5.921875 -1.613281 5.703125 -1.46875 C 5.492188 -1.320312 5.28125 -1.207031 5.0625 -1.125 C 4.84375 -1.050781 4.632812 -1.003906 4.4375 -0.984375 C 4.25 -0.960938 4.09375 -0.953125 3.96875 -0.953125 Z M 0.9375 -8.5625 L 0.9375 0 L 3.875 0 C 4.582031 0 5.195312 -0.0976562 5.71875 -0.296875 C 6.238281 -0.492188 6.664062 -0.78125 7 -1.15625 C 7.34375 -1.539062 7.59375 -2.007812 7.75 -2.5625 C 7.90625 -3.125 7.984375 -3.765625 7.984375 -4.484375 C 7.984375 -5.859375 7.628906 -6.878906 6.921875 -7.546875 C 6.210938 -8.222656 5.195312 -8.5625 3.875 -8.5625 Z M 0.9375 -8.5625 "/> +</symbol> +<symbol overflow="visible" id="glyph0-7"> +<path style="stroke:none;" d="M 7.34375 -1.0625 L 7.640625 0 L 8.359375 0 L 8.359375 -4.515625 L 4.609375 -4.515625 L 4.609375 -3.546875 L 7.34375 -3.546875 C 7.363281 -3.160156 7.3125 -2.796875 7.1875 -2.453125 C 7.070312 -2.109375 6.894531 -1.8125 6.65625 -1.5625 C 6.414062 -1.3125 6.125 -1.113281 5.78125 -0.96875 C 5.4375 -0.820312 5.039062 -0.75 4.59375 -0.75 C 4.113281 -0.75 3.691406 -0.84375 3.328125 -1.03125 C 2.960938 -1.21875 2.65625 -1.46875 2.40625 -1.78125 C 2.164062 -2.101562 1.976562 -2.46875 1.84375 -2.875 C 1.71875 -3.289062 1.65625 -3.722656 1.65625 -4.171875 C 1.65625 -4.628906 1.707031 -5.078125 1.8125 -5.515625 C 1.925781 -5.953125 2.101562 -6.335938 2.34375 -6.671875 C 2.582031 -7.015625 2.882812 -7.289062 3.25 -7.5 C 3.625 -7.707031 4.070312 -7.8125 4.59375 -7.8125 C 4.914062 -7.8125 5.21875 -7.769531 5.5 -7.6875 C 5.78125 -7.613281 6.03125 -7.5 6.25 -7.34375 C 6.476562 -7.195312 6.671875 -7.003906 6.828125 -6.765625 C 6.984375 -6.535156 7.085938 -6.253906 7.140625 -5.921875 L 8.28125 -5.921875 C 8.195312 -6.429688 8.046875 -6.863281 7.828125 -7.21875 C 7.609375 -7.570312 7.335938 -7.863281 7.015625 -8.09375 C 6.691406 -8.332031 6.320312 -8.503906 5.90625 -8.609375 C 5.5 -8.710938 5.0625 -8.765625 4.59375 -8.765625 C 3.914062 -8.765625 3.320312 -8.640625 2.8125 -8.390625 C 2.300781 -8.140625 1.875 -7.800781 1.53125 -7.375 C 1.195312 -6.957031 0.941406 -6.460938 0.765625 -5.890625 C 0.597656 -5.328125 0.515625 -4.734375 0.515625 -4.109375 C 0.515625 -3.554688 0.601562 -3.019531 0.78125 -2.5 C 0.96875 -1.976562 1.238281 -1.515625 1.59375 -1.109375 C 1.945312 -0.710938 2.375 -0.394531 2.875 -0.15625 C 3.382812 0.0703125 3.957031 0.1875 4.59375 0.1875 C 5.101562 0.1875 5.601562 0.09375 6.09375 -0.09375 C 6.59375 -0.289062 7.007812 -0.613281 7.34375 -1.0625 Z M 7.34375 -1.0625 "/> +</symbol> +<symbol overflow="visible" id="glyph0-8"> +<path style="stroke:none;" d="M 0.734375 -6.203125 L 0.734375 0 L 1.75 0 L 1.75 -2.765625 C 1.75 -3.160156 1.785156 -3.507812 1.859375 -3.8125 C 1.941406 -4.125 2.070312 -4.390625 2.25 -4.609375 C 2.425781 -4.828125 2.660156 -4.988281 2.953125 -5.09375 C 3.242188 -5.207031 3.59375 -5.265625 4 -5.265625 L 4 -6.34375 C 3.445312 -6.363281 2.988281 -6.253906 2.625 -6.015625 C 2.269531 -5.773438 1.96875 -5.398438 1.71875 -4.890625 L 1.6875 -4.890625 L 1.6875 -6.203125 Z M 0.734375 -6.203125 "/> +</symbol> +<symbol overflow="visible" id="glyph1-0"> +<path style="stroke:none;" d="M 0.390625 0 L 0.390625 -8.609375 L 7.21875 -8.609375 L 7.21875 0 Z M 6.140625 -1.078125 L 6.140625 -7.53125 L 1.46875 -7.53125 L 1.46875 -1.078125 Z M 6.140625 -1.078125 "/> +</symbol> +<symbol overflow="visible" id="glyph1-1"> +<path style="stroke:none;" d="M 4.546875 -8.84375 C 5.628906 -8.84375 6.472656 -8.554688 7.078125 -7.984375 C 7.679688 -7.410156 8.015625 -6.757812 8.078125 -6.03125 L 6.9375 -6.03125 C 6.8125 -6.582031 6.554688 -7.019531 6.171875 -7.34375 C 5.785156 -7.664062 5.242188 -7.828125 4.546875 -7.828125 C 3.703125 -7.828125 3.019531 -7.53125 2.5 -6.9375 C 1.976562 -6.34375 1.71875 -5.429688 1.71875 -4.203125 C 1.71875 -3.191406 1.953125 -2.367188 2.421875 -1.734375 C 2.890625 -1.109375 3.59375 -0.796875 4.53125 -0.796875 C 5.382812 -0.796875 6.039062 -1.128906 6.5 -1.796875 C 6.726562 -2.140625 6.90625 -2.597656 7.03125 -3.171875 L 8.15625 -3.171875 C 8.0625 -2.265625 7.726562 -1.503906 7.15625 -0.890625 C 6.46875 -0.148438 5.546875 0.21875 4.390625 0.21875 C 3.390625 0.21875 2.550781 -0.0820312 1.875 -0.6875 C 0.976562 -1.488281 0.53125 -2.722656 0.53125 -4.390625 C 0.53125 -5.660156 0.863281 -6.703125 1.53125 -7.515625 C 2.257812 -8.398438 3.265625 -8.84375 4.546875 -8.84375 Z M 4.3125 -8.84375 Z M 4.3125 -8.84375 "/> +</symbol> +<symbol overflow="visible" id="glyph1-2"> +<path style="stroke:none;" d="M 3.265625 -0.6875 C 3.960938 -0.6875 4.441406 -0.945312 4.703125 -1.46875 C 4.960938 -2 5.09375 -2.585938 5.09375 -3.234375 C 5.09375 -3.828125 5 -4.304688 4.8125 -4.671875 C 4.507812 -5.242188 4 -5.53125 3.28125 -5.53125 C 2.632812 -5.53125 2.164062 -5.285156 1.875 -4.796875 C 1.582031 -4.304688 1.4375 -3.710938 1.4375 -3.015625 C 1.4375 -2.347656 1.582031 -1.789062 1.875 -1.34375 C 2.164062 -0.90625 2.628906 -0.6875 3.265625 -0.6875 Z M 3.3125 -6.453125 C 4.113281 -6.453125 4.789062 -6.179688 5.34375 -5.640625 C 5.90625 -5.109375 6.1875 -4.316406 6.1875 -3.265625 C 6.1875 -2.253906 5.941406 -1.414062 5.453125 -0.75 C 4.960938 -0.09375 4.203125 0.234375 3.171875 0.234375 C 2.304688 0.234375 1.617188 -0.0546875 1.109375 -0.640625 C 0.597656 -1.234375 0.34375 -2.019531 0.34375 -3 C 0.34375 -4.050781 0.609375 -4.890625 1.140625 -5.515625 C 1.679688 -6.140625 2.40625 -6.453125 3.3125 -6.453125 Z M 3.265625 -6.421875 Z M 3.265625 -6.421875 "/> +</symbol> +<symbol overflow="visible" id="glyph1-3"> +<path style="stroke:none;" d="M 1.4375 -3.0625 C 1.4375 -2.394531 1.578125 -1.832031 1.859375 -1.375 C 2.148438 -0.925781 2.609375 -0.703125 3.234375 -0.703125 C 3.722656 -0.703125 4.125 -0.910156 4.4375 -1.328125 C 4.757812 -1.742188 4.921875 -2.347656 4.921875 -3.140625 C 4.921875 -3.929688 4.753906 -4.515625 4.421875 -4.890625 C 4.097656 -5.273438 3.703125 -5.46875 3.234375 -5.46875 C 2.703125 -5.46875 2.269531 -5.265625 1.9375 -4.859375 C 1.601562 -4.453125 1.4375 -3.851562 1.4375 -3.0625 Z M 3.03125 -6.390625 C 3.507812 -6.390625 3.910156 -6.285156 4.234375 -6.078125 C 4.421875 -5.960938 4.632812 -5.757812 4.875 -5.46875 L 4.875 -8.640625 L 5.890625 -8.640625 L 5.890625 0 L 4.9375 0 L 4.9375 -0.875 C 4.695312 -0.488281 4.40625 -0.207031 4.0625 -0.03125 C 3.726562 0.132812 3.34375 0.21875 2.90625 0.21875 C 2.207031 0.21875 1.601562 -0.0703125 1.09375 -0.65625 C 0.582031 -1.25 0.328125 -2.03125 0.328125 -3 C 0.328125 -3.914062 0.5625 -4.707031 1.03125 -5.375 C 1.5 -6.050781 2.164062 -6.390625 3.03125 -6.390625 Z M 3.03125 -6.390625 "/> +</symbol> +<symbol overflow="visible" id="glyph1-4"> +<path style="stroke:none;" d="M 3.390625 -6.421875 C 3.835938 -6.421875 4.269531 -6.316406 4.6875 -6.109375 C 5.101562 -5.898438 5.421875 -5.628906 5.640625 -5.296875 C 5.847656 -4.972656 5.988281 -4.601562 6.0625 -4.1875 C 6.125 -3.894531 6.15625 -3.429688 6.15625 -2.796875 L 1.546875 -2.796875 C 1.566406 -2.160156 1.71875 -1.648438 2 -1.265625 C 2.28125 -0.878906 2.71875 -0.6875 3.3125 -0.6875 C 3.863281 -0.6875 4.300781 -0.867188 4.625 -1.234375 C 4.8125 -1.441406 4.945312 -1.6875 5.03125 -1.96875 L 6.0625 -1.96875 C 6.039062 -1.738281 5.953125 -1.484375 5.796875 -1.203125 C 5.640625 -0.921875 5.46875 -0.6875 5.28125 -0.5 C 4.957031 -0.1875 4.554688 0.0195312 4.078125 0.125 C 3.828125 0.1875 3.539062 0.21875 3.21875 0.21875 C 2.4375 0.21875 1.773438 -0.0625 1.234375 -0.625 C 0.691406 -1.195312 0.421875 -1.992188 0.421875 -3.015625 C 0.421875 -4.023438 0.691406 -4.84375 1.234375 -5.46875 C 1.785156 -6.101562 2.503906 -6.421875 3.390625 -6.421875 Z M 5.0625 -3.640625 C 5.019531 -4.097656 4.921875 -4.460938 4.765625 -4.734375 C 4.484375 -5.242188 4.003906 -5.5 3.328125 -5.5 C 2.835938 -5.5 2.425781 -5.320312 2.09375 -4.96875 C 1.769531 -4.625 1.597656 -4.179688 1.578125 -3.640625 Z M 3.28125 -6.421875 Z M 3.28125 -6.421875 "/> +</symbol> +<symbol overflow="visible" id="glyph1-5"> +<path style="stroke:none;" d=""/> +</symbol> +<symbol overflow="visible" id="glyph1-6"> +<path style="stroke:none;" d="M 4.640625 -8.828125 C 5.441406 -8.828125 6.140625 -8.671875 6.734375 -8.359375 C 7.585938 -7.910156 8.109375 -7.125 8.296875 -6 L 7.15625 -6 C 7.007812 -6.625 6.710938 -7.082031 6.265625 -7.375 C 5.828125 -7.664062 5.273438 -7.8125 4.609375 -7.8125 C 3.804688 -7.8125 3.132812 -7.507812 2.59375 -6.90625 C 2.050781 -6.3125 1.78125 -5.421875 1.78125 -4.234375 C 1.78125 -3.210938 2.003906 -2.378906 2.453125 -1.734375 C 2.898438 -1.097656 3.628906 -0.78125 4.640625 -0.78125 C 5.421875 -0.78125 6.066406 -1.003906 6.578125 -1.453125 C 7.085938 -1.898438 7.347656 -2.628906 7.359375 -3.640625 L 4.671875 -3.640625 L 4.671875 -4.609375 L 8.4375 -4.609375 L 8.4375 0 L 7.6875 0 L 7.40625 -1.109375 C 7.019531 -0.671875 6.671875 -0.367188 6.359375 -0.203125 C 5.847656 0.0859375 5.195312 0.234375 4.40625 0.234375 C 3.394531 0.234375 2.519531 -0.0976562 1.78125 -0.765625 C 0.976562 -1.585938 0.578125 -2.722656 0.578125 -4.171875 C 0.578125 -5.609375 0.96875 -6.753906 1.75 -7.609375 C 2.488281 -8.421875 3.453125 -8.828125 4.640625 -8.828125 Z M 4.4375 -8.84375 Z M 4.4375 -8.84375 "/> +</symbol> +<symbol overflow="visible" id="glyph1-7"> +<path style="stroke:none;" d="M 1.578125 -1.671875 C 1.578125 -1.367188 1.6875 -1.128906 1.90625 -0.953125 C 2.132812 -0.773438 2.398438 -0.6875 2.703125 -0.6875 C 3.078125 -0.6875 3.4375 -0.769531 3.78125 -0.9375 C 4.375 -1.226562 4.671875 -1.695312 4.671875 -2.34375 L 4.671875 -3.1875 C 4.535156 -3.113281 4.363281 -3.046875 4.15625 -2.984375 C 3.957031 -2.929688 3.757812 -2.894531 3.5625 -2.875 L 2.9375 -2.796875 C 2.550781 -2.742188 2.257812 -2.660156 2.0625 -2.546875 C 1.738281 -2.367188 1.578125 -2.078125 1.578125 -1.671875 Z M 4.140625 -3.796875 C 4.378906 -3.828125 4.539062 -3.929688 4.625 -4.109375 C 4.664062 -4.203125 4.6875 -4.335938 4.6875 -4.515625 C 4.6875 -4.867188 4.554688 -5.125 4.296875 -5.28125 C 4.046875 -5.445312 3.6875 -5.53125 3.21875 -5.53125 C 2.664062 -5.53125 2.273438 -5.382812 2.046875 -5.09375 C 1.910156 -4.925781 1.820312 -4.679688 1.78125 -4.359375 L 0.796875 -4.359375 C 0.816406 -5.128906 1.066406 -5.664062 1.546875 -5.96875 C 2.035156 -6.269531 2.597656 -6.421875 3.234375 -6.421875 C 3.972656 -6.421875 4.570312 -6.28125 5.03125 -6 C 5.488281 -5.71875 5.71875 -5.28125 5.71875 -4.6875 L 5.71875 -1.078125 C 5.71875 -0.972656 5.738281 -0.882812 5.78125 -0.8125 C 5.832031 -0.75 5.929688 -0.71875 6.078125 -0.71875 C 6.117188 -0.71875 6.164062 -0.71875 6.21875 -0.71875 C 6.28125 -0.726562 6.347656 -0.738281 6.421875 -0.75 L 6.421875 0.03125 C 6.253906 0.0703125 6.125 0.0976562 6.03125 0.109375 C 5.945312 0.128906 5.832031 0.140625 5.6875 0.140625 C 5.320312 0.140625 5.0625 0.0078125 4.90625 -0.25 C 4.8125 -0.382812 4.75 -0.578125 4.71875 -0.828125 C 4.5 -0.546875 4.1875 -0.300781 3.78125 -0.09375 C 3.382812 0.113281 2.945312 0.21875 2.46875 0.21875 C 1.882812 0.21875 1.40625 0.0390625 1.03125 -0.3125 C 0.664062 -0.664062 0.484375 -1.109375 0.484375 -1.640625 C 0.484375 -2.222656 0.664062 -2.675781 1.03125 -3 C 1.394531 -3.320312 1.867188 -3.519531 2.453125 -3.59375 Z M 3.265625 -6.421875 Z M 3.265625 -6.421875 "/> +</symbol> +<symbol overflow="visible" id="glyph1-8"> +<path style="stroke:none;" d="M 0.796875 -6.28125 L 1.8125 -6.28125 L 1.8125 -5.1875 C 1.882812 -5.40625 2.082031 -5.664062 2.40625 -5.96875 C 2.726562 -6.269531 3.097656 -6.421875 3.515625 -6.421875 C 3.535156 -6.421875 3.566406 -6.414062 3.609375 -6.40625 C 3.660156 -6.40625 3.742188 -6.398438 3.859375 -6.390625 L 3.859375 -5.28125 C 3.796875 -5.289062 3.738281 -5.296875 3.6875 -5.296875 C 3.632812 -5.296875 3.578125 -5.296875 3.515625 -5.296875 C 2.984375 -5.296875 2.570312 -5.125 2.28125 -4.78125 C 2 -4.445312 1.859375 -4.054688 1.859375 -3.609375 L 1.859375 0 L 0.796875 0 Z M 0.796875 -6.28125 "/> +</symbol> +<symbol overflow="visible" id="glyph1-9"> +<path style="stroke:none;" d="M 4.21875 -1 C 4.613281 -1 4.9375 -1.039062 5.1875 -1.125 C 5.644531 -1.269531 6.019531 -1.5625 6.3125 -2 C 6.539062 -2.34375 6.703125 -2.785156 6.796875 -3.328125 C 6.859375 -3.660156 6.890625 -3.960938 6.890625 -4.234375 C 6.890625 -5.304688 6.675781 -6.132812 6.25 -6.71875 C 5.832031 -7.3125 5.148438 -7.609375 4.203125 -7.609375 L 2.140625 -7.609375 L 2.140625 -1 Z M 0.96875 -8.609375 L 4.453125 -8.609375 C 5.640625 -8.609375 6.554688 -8.1875 7.203125 -7.34375 C 7.785156 -6.59375 8.078125 -5.625 8.078125 -4.4375 C 8.078125 -3.519531 7.90625 -2.691406 7.5625 -1.953125 C 6.957031 -0.648438 5.914062 0 4.4375 0 L 0.96875 0 Z M 0.96875 -8.609375 "/> +</symbol> +<symbol overflow="visible" id="glyph1-10"> +<path style="stroke:none;" d="M 0.984375 -8.03125 L 2.046875 -8.03125 L 2.046875 -6.28125 L 3.046875 -6.28125 L 3.046875 -5.421875 L 2.046875 -5.421875 L 2.046875 -1.3125 C 2.046875 -1.09375 2.125 -0.945312 2.28125 -0.875 C 2.351562 -0.832031 2.488281 -0.8125 2.6875 -0.8125 C 2.738281 -0.8125 2.789062 -0.8125 2.84375 -0.8125 C 2.90625 -0.820312 2.972656 -0.828125 3.046875 -0.828125 L 3.046875 0 C 2.929688 0.03125 2.804688 0.0507812 2.671875 0.0625 C 2.546875 0.0820312 2.40625 0.09375 2.25 0.09375 C 1.757812 0.09375 1.425781 -0.03125 1.25 -0.28125 C 1.070312 -0.53125 0.984375 -0.859375 0.984375 -1.265625 L 0.984375 -5.421875 L 0.140625 -5.421875 L 0.140625 -6.28125 L 0.984375 -6.28125 Z M 0.984375 -8.03125 "/> +</symbol> +<symbol overflow="visible" id="glyph1-11"> +<path style="stroke:none;" d="M 0.890625 -8.609375 L 2.5625 -8.609375 L 5.03125 -1.328125 L 7.484375 -8.609375 L 9.140625 -8.609375 L 9.140625 0 L 8.03125 0 L 8.03125 -5.078125 C 8.03125 -5.253906 8.03125 -5.546875 8.03125 -5.953125 C 8.039062 -6.359375 8.046875 -6.796875 8.046875 -7.265625 L 5.59375 0 L 4.4375 0 L 1.96875 -7.265625 L 1.96875 -7 C 1.96875 -6.789062 1.972656 -6.46875 1.984375 -6.03125 C 1.992188 -5.601562 2 -5.285156 2 -5.078125 L 2 0 L 0.890625 0 Z M 0.890625 -8.609375 "/> +</symbol> +</g> +<clipPath id="clip1"> + <path d="M 0 0 L 605.980469 0 L 605.980469 219.617188 L 0 219.617188 Z M 0 0 "/> +</clipPath> +</defs> +<g id="surface1"> +<g clip-path="url(#clip1)" clip-rule="nonzero"> +<rect x="0" y="0" width="605.980469" height="219.6172" style="fill:rgb(100%,100%,100%);fill-opacity:1;stroke:none;"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(100%,57.647705%,0%);stroke-opacity:1;stroke-dasharray:4,4;stroke-miterlimit:10;" d="M 178.9375 310.179688 C 204.355469 327.753906 204.355469 356.246094 178.9375 373.820312 C 153.519531 391.394531 112.304687 391.394531 86.886719 373.820312 C 61.46875 356.246094 61.46875 327.753906 86.886719 310.179688 C 112.304687 292.605469 153.519531 292.605469 178.9375 310.179688 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph0-1" x="31.232479" y="126.332001"/> + <use xlink:href="#glyph0-2" x="41.684479" y="126.332001"/> + <use xlink:href="#glyph0-3" x="48.128479" y="126.332001"/> + <use xlink:href="#glyph0-4" x="51.908479" y="126.332001"/> + <use xlink:href="#glyph0-5" x="58.352479" y="126.332001"/> + <use xlink:href="#glyph0-6" x="61.688479" y="126.332001"/> + <use xlink:href="#glyph0-4" x="70.136479" y="126.332001"/> + <use xlink:href="#glyph0-3" x="76.580479" y="126.332001"/> + <use xlink:href="#glyph0-4" x="80.360479" y="126.332001"/> + <use xlink:href="#glyph0-5" x="86.804479" y="126.332001"/> + <use xlink:href="#glyph0-7" x="90.140479" y="126.332001"/> + <use xlink:href="#glyph0-2" x="99.248479" y="126.332001"/> + <use xlink:href="#glyph0-4" x="105.692479" y="126.332001"/> + <use xlink:href="#glyph0-8" x="112.136479" y="126.332001"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(100%,57.647705%,0%);stroke-opacity:1;stroke-dasharray:4,4;stroke-miterlimit:10;" d="M 633.113281 310.179688 C 658.53125 327.753906 658.53125 356.246094 633.113281 373.820312 C 607.695312 391.394531 566.480469 391.394531 541.0625 373.820312 C 515.644531 356.246094 515.644531 327.753906 541.0625 310.179688 C 566.480469 292.605469 607.695312 292.605469 633.113281 310.179688 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph0-1" x="485.407969" y="126.332001"/> + <use xlink:href="#glyph0-2" x="495.859969" y="126.332001"/> + <use xlink:href="#glyph0-3" x="502.303969" y="126.332001"/> + <use xlink:href="#glyph0-4" x="506.083969" y="126.332001"/> + <use xlink:href="#glyph0-5" x="512.527969" y="126.332001"/> + <use xlink:href="#glyph0-6" x="515.863969" y="126.332001"/> + <use xlink:href="#glyph0-4" x="524.311969" y="126.332001"/> + <use xlink:href="#glyph0-3" x="530.755969" y="126.332001"/> + <use xlink:href="#glyph0-4" x="534.535969" y="126.332001"/> + <use xlink:href="#glyph0-5" x="540.979969" y="126.332001"/> + <use xlink:href="#glyph0-7" x="544.315969" y="126.332001"/> + <use xlink:href="#glyph0-2" x="553.423969" y="126.332001"/> + <use xlink:href="#glyph0-4" x="559.867969" y="126.332001"/> + <use xlink:href="#glyph0-8" x="566.311969" y="126.332001"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 316.421875 333 L 391.9375 333 L 391.9375 378 L 316.421875 378 Z M 316.421875 333 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-1" x="266.810659" y="163.5"/> + <use xlink:href="#glyph1-2" x="275.477059" y="163.5"/> + <use xlink:href="#glyph1-3" x="282.151459" y="163.5"/> + <use xlink:href="#glyph1-4" x="288.825859" y="163.5"/> + <use xlink:href="#glyph1-5" x="295.500259" y="163.5"/> + <use xlink:href="#glyph1-6" x="298.838659" y="163.5"/> + <use xlink:href="#glyph1-4" x="308.177059" y="163.5"/> + <use xlink:href="#glyph1-7" x="314.851459" y="163.5"/> + <use xlink:href="#glyph1-8" x="321.525859" y="163.5"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 159.941406 339.589844 C 174.6875 348.375 174.6875 362.625 159.941406 371.410156 C 145.195312 380.195312 121.289062 380.195312 106.542969 371.410156 C 91.796875 362.625 91.796875 348.375 106.542969 339.589844 C 121.289062 330.804688 145.195312 330.804688 159.941406 339.589844 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-9" x="62.547809" y="156.5"/> + <use xlink:href="#glyph1-7" x="71.214209" y="156.5"/> + <use xlink:href="#glyph1-10" x="77.888609" y="156.5"/> + <use xlink:href="#glyph1-7" x="81.227009" y="156.5"/> + <use xlink:href="#glyph1-5" x="87.901409" y="156.5"/> +</g> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-6" x="61.882769" y="170.5"/> + <use xlink:href="#glyph1-4" x="71.216369" y="170.5"/> + <use xlink:href="#glyph1-7" x="77.885969" y="170.5"/> + <use xlink:href="#glyph1-8" x="84.555569" y="170.5"/> +</g> +<path style="fill:none;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 171.5 355.5 L 306.519531 355.5 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 314.519531 355.5 L 306.519531 352.5 L 306.519531 358.5 Z M 314.519531 355.5 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 613.457031 339.589844 C 628.203125 348.375 628.203125 362.625 613.457031 371.410156 C 598.710937 380.195312 574.804687 380.195312 560.058594 371.410156 C 545.3125 362.625 545.3125 348.375 560.058594 339.589844 C 574.804687 330.804688 598.710937 330.804688 613.457031 339.589844 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-9" x="516.065439" y="156.5"/> + <use xlink:href="#glyph1-7" x="524.731839" y="156.5"/> + <use xlink:href="#glyph1-10" x="531.406239" y="156.5"/> + <use xlink:href="#glyph1-7" x="534.744639" y="156.5"/> + <use xlink:href="#glyph1-5" x="541.419039" y="156.5"/> +</g> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-6" x="515.400399" y="170.5"/> + <use xlink:href="#glyph1-4" x="524.733999" y="170.5"/> + <use xlink:href="#glyph1-7" x="531.403599" y="170.5"/> + <use xlink:href="#glyph1-8" x="538.073199" y="170.5"/> +</g> +<path style="fill:none;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 391.9375 355.5 L 538.601562 355.5 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 546.601562 355.5 L 538.601562 352.5 L 538.601562 358.5 Z M 546.601562 355.5 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(100%,57.647705%,0%);stroke-opacity:1;stroke-dasharray:4,4;stroke-miterlimit:10;" d="M 211.824219 335.25 L 282.183594 335.25 L 282.183594 375.75 L 211.824219 375.75 Z M 211.824219 335.25 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-11" x="159.634959" y="156.5"/> + <use xlink:href="#glyph1-4" x="169.630959" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-10" x="176.305359" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-7" x="179.638959" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-5" x="186.313359" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-1" x="189.646959" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-2" x="198.313359" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-3" x="204.987759" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-4" x="211.662159" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-5" x="218.336559" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-6" x="175.645699" y="170.5"/> + <use xlink:href="#glyph1-4" x="184.979299" y="170.5"/> + <use xlink:href="#glyph1-7" x="191.648899" y="170.5"/> + <use xlink:href="#glyph1-8" x="198.318499" y="170.5"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(100%,57.647705%,0%);stroke-opacity:1;stroke-dasharray:4,4;stroke-miterlimit:10;" d="M 423.839844 335.25 L 493.035156 335.25 L 493.035156 375.75 L 423.839844 375.75 Z M 423.839844 335.25 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-11" x="371.069059" y="156.5"/> + <use xlink:href="#glyph1-4" x="381.065059" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-10" x="387.739459" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-7" x="391.073059" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-5" x="397.747459" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-1" x="401.081059" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-2" x="409.747459" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-3" x="416.421859" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-4" x="423.096259" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-5" x="429.770659" y="156.5"/> +</g> +<g style="fill:rgb(76.078796%,34.509277%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-6" x="387.079799" y="170.5"/> + <use xlink:href="#glyph1-4" x="396.413399" y="170.5"/> + <use xlink:href="#glyph1-7" x="403.082999" y="170.5"/> + <use xlink:href="#glyph1-8" x="409.752599" y="170.5"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 316.421875 207 L 391.9375 207 L 391.9375 252 L 316.421875 252 Z M 316.421875 207 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-1" x="266.810659" y="37.5"/> + <use xlink:href="#glyph1-2" x="275.477059" y="37.5"/> + <use xlink:href="#glyph1-3" x="282.151459" y="37.5"/> + <use xlink:href="#glyph1-4" x="288.825859" y="37.5"/> + <use xlink:href="#glyph1-5" x="295.500259" y="37.5"/> + <use xlink:href="#glyph1-6" x="298.838659" y="37.5"/> + <use xlink:href="#glyph1-4" x="308.177059" y="37.5"/> + <use xlink:href="#glyph1-7" x="314.851459" y="37.5"/> + <use xlink:href="#glyph1-8" x="321.525859" y="37.5"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 159.941406 213.589844 C 174.6875 222.375 174.6875 236.625 159.941406 245.410156 C 145.195312 254.195312 121.289062 254.195312 106.542969 245.410156 C 91.796875 236.625 91.796875 222.375 106.542969 213.589844 C 121.289062 204.804688 145.195312 204.804688 159.941406 213.589844 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-9" x="62.547809" y="30.5"/> + <use xlink:href="#glyph1-7" x="71.214209" y="30.5"/> + <use xlink:href="#glyph1-10" x="77.888609" y="30.5"/> + <use xlink:href="#glyph1-7" x="81.227009" y="30.5"/> + <use xlink:href="#glyph1-5" x="87.901409" y="30.5"/> +</g> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-6" x="61.882769" y="44.5"/> + <use xlink:href="#glyph1-4" x="71.216369" y="44.5"/> + <use xlink:href="#glyph1-7" x="77.885969" y="44.5"/> + <use xlink:href="#glyph1-8" x="84.555569" y="44.5"/> +</g> +<path style="fill:none;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 171.5 229.5 L 306.519531 229.5 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 314.519531 229.5 L 306.519531 226.5 L 306.519531 232.5 Z M 314.519531 229.5 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 613.457031 213.589844 C 628.203125 222.375 628.203125 236.625 613.457031 245.410156 C 598.710937 254.195312 574.804687 254.195312 560.058594 245.410156 C 545.3125 236.625 545.3125 222.375 560.058594 213.589844 C 574.804687 204.804688 598.710937 204.804688 613.457031 213.589844 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-9" x="516.065439" y="30.5"/> + <use xlink:href="#glyph1-7" x="524.731839" y="30.5"/> + <use xlink:href="#glyph1-10" x="531.406239" y="30.5"/> + <use xlink:href="#glyph1-7" x="534.744639" y="30.5"/> + <use xlink:href="#glyph1-5" x="541.419039" y="30.5"/> +</g> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-6" x="515.400399" y="44.5"/> + <use xlink:href="#glyph1-4" x="524.733999" y="44.5"/> + <use xlink:href="#glyph1-7" x="531.403599" y="44.5"/> + <use xlink:href="#glyph1-8" x="538.073199" y="44.5"/> +</g> +<path style="fill:none;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 391.9375 229.5 L 538.601562 229.5 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 546.601562 229.5 L 538.601562 226.5 L 538.601562 232.5 Z M 546.601562 229.5 " transform="matrix(1,0,0,1,-58.019531,-196)"/> +</g> +</svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/pic/cgdg.svg Sun Jan 13 23:42:16 2019 +0900 @@ -0,0 +1,201 @@ +<?xml version="1.0" encoding="UTF-8"?> +<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="535pt" height="427pt" viewBox="0 0 535 427" version="1.1"> +<defs> +<g> +<symbol overflow="visible" id="glyph0-0"> +<path style="stroke:none;" d="M 0.390625 0 L 0.390625 -8.609375 L 7.21875 -8.609375 L 7.21875 0 Z M 6.140625 -1.078125 L 6.140625 -7.53125 L 1.46875 -7.53125 L 1.46875 -1.078125 Z M 6.140625 -1.078125 "/> +</symbol> +<symbol overflow="visible" id="glyph0-1"> +<path style="stroke:none;" d="M 4.546875 -8.84375 C 5.628906 -8.84375 6.472656 -8.554688 7.078125 -7.984375 C 7.679688 -7.410156 8.015625 -6.757812 8.078125 -6.03125 L 6.9375 -6.03125 C 6.8125 -6.582031 6.554688 -7.019531 6.171875 -7.34375 C 5.785156 -7.664062 5.242188 -7.828125 4.546875 -7.828125 C 3.703125 -7.828125 3.019531 -7.53125 2.5 -6.9375 C 1.976562 -6.34375 1.71875 -5.429688 1.71875 -4.203125 C 1.71875 -3.191406 1.953125 -2.367188 2.421875 -1.734375 C 2.890625 -1.109375 3.59375 -0.796875 4.53125 -0.796875 C 5.382812 -0.796875 6.039062 -1.128906 6.5 -1.796875 C 6.726562 -2.140625 6.90625 -2.597656 7.03125 -3.171875 L 8.15625 -3.171875 C 8.0625 -2.265625 7.726562 -1.503906 7.15625 -0.890625 C 6.46875 -0.148438 5.546875 0.21875 4.390625 0.21875 C 3.390625 0.21875 2.550781 -0.0820312 1.875 -0.6875 C 0.976562 -1.488281 0.53125 -2.722656 0.53125 -4.390625 C 0.53125 -5.660156 0.863281 -6.703125 1.53125 -7.515625 C 2.257812 -8.398438 3.265625 -8.84375 4.546875 -8.84375 Z M 4.3125 -8.84375 Z M 4.3125 -8.84375 "/> +</symbol> +<symbol overflow="visible" id="glyph0-2"> +<path style="stroke:none;" d="M 3.265625 -0.6875 C 3.960938 -0.6875 4.441406 -0.945312 4.703125 -1.46875 C 4.960938 -2 5.09375 -2.585938 5.09375 -3.234375 C 5.09375 -3.828125 5 -4.304688 4.8125 -4.671875 C 4.507812 -5.242188 4 -5.53125 3.28125 -5.53125 C 2.632812 -5.53125 2.164062 -5.285156 1.875 -4.796875 C 1.582031 -4.304688 1.4375 -3.710938 1.4375 -3.015625 C 1.4375 -2.347656 1.582031 -1.789062 1.875 -1.34375 C 2.164062 -0.90625 2.628906 -0.6875 3.265625 -0.6875 Z M 3.3125 -6.453125 C 4.113281 -6.453125 4.789062 -6.179688 5.34375 -5.640625 C 5.90625 -5.109375 6.1875 -4.316406 6.1875 -3.265625 C 6.1875 -2.253906 5.941406 -1.414062 5.453125 -0.75 C 4.960938 -0.09375 4.203125 0.234375 3.171875 0.234375 C 2.304688 0.234375 1.617188 -0.0546875 1.109375 -0.640625 C 0.597656 -1.234375 0.34375 -2.019531 0.34375 -3 C 0.34375 -4.050781 0.609375 -4.890625 1.140625 -5.515625 C 1.679688 -6.140625 2.40625 -6.453125 3.3125 -6.453125 Z M 3.265625 -6.421875 Z M 3.265625 -6.421875 "/> +</symbol> +<symbol overflow="visible" id="glyph0-3"> +<path style="stroke:none;" d="M 1.4375 -3.0625 C 1.4375 -2.394531 1.578125 -1.832031 1.859375 -1.375 C 2.148438 -0.925781 2.609375 -0.703125 3.234375 -0.703125 C 3.722656 -0.703125 4.125 -0.910156 4.4375 -1.328125 C 4.757812 -1.742188 4.921875 -2.347656 4.921875 -3.140625 C 4.921875 -3.929688 4.753906 -4.515625 4.421875 -4.890625 C 4.097656 -5.273438 3.703125 -5.46875 3.234375 -5.46875 C 2.703125 -5.46875 2.269531 -5.265625 1.9375 -4.859375 C 1.601562 -4.453125 1.4375 -3.851562 1.4375 -3.0625 Z M 3.03125 -6.390625 C 3.507812 -6.390625 3.910156 -6.285156 4.234375 -6.078125 C 4.421875 -5.960938 4.632812 -5.757812 4.875 -5.46875 L 4.875 -8.640625 L 5.890625 -8.640625 L 5.890625 0 L 4.9375 0 L 4.9375 -0.875 C 4.695312 -0.488281 4.40625 -0.207031 4.0625 -0.03125 C 3.726562 0.132812 3.34375 0.21875 2.90625 0.21875 C 2.207031 0.21875 1.601562 -0.0703125 1.09375 -0.65625 C 0.582031 -1.25 0.328125 -2.03125 0.328125 -3 C 0.328125 -3.914062 0.5625 -4.707031 1.03125 -5.375 C 1.5 -6.050781 2.164062 -6.390625 3.03125 -6.390625 Z M 3.03125 -6.390625 "/> +</symbol> +<symbol overflow="visible" id="glyph0-4"> +<path style="stroke:none;" d="M 3.390625 -6.421875 C 3.835938 -6.421875 4.269531 -6.316406 4.6875 -6.109375 C 5.101562 -5.898438 5.421875 -5.628906 5.640625 -5.296875 C 5.847656 -4.972656 5.988281 -4.601562 6.0625 -4.1875 C 6.125 -3.894531 6.15625 -3.429688 6.15625 -2.796875 L 1.546875 -2.796875 C 1.566406 -2.160156 1.71875 -1.648438 2 -1.265625 C 2.28125 -0.878906 2.71875 -0.6875 3.3125 -0.6875 C 3.863281 -0.6875 4.300781 -0.867188 4.625 -1.234375 C 4.8125 -1.441406 4.945312 -1.6875 5.03125 -1.96875 L 6.0625 -1.96875 C 6.039062 -1.738281 5.953125 -1.484375 5.796875 -1.203125 C 5.640625 -0.921875 5.46875 -0.6875 5.28125 -0.5 C 4.957031 -0.1875 4.554688 0.0195312 4.078125 0.125 C 3.828125 0.1875 3.539062 0.21875 3.21875 0.21875 C 2.4375 0.21875 1.773438 -0.0625 1.234375 -0.625 C 0.691406 -1.195312 0.421875 -1.992188 0.421875 -3.015625 C 0.421875 -4.023438 0.691406 -4.84375 1.234375 -5.46875 C 1.785156 -6.101562 2.503906 -6.421875 3.390625 -6.421875 Z M 5.0625 -3.640625 C 5.019531 -4.097656 4.921875 -4.460938 4.765625 -4.734375 C 4.484375 -5.242188 4.003906 -5.5 3.328125 -5.5 C 2.835938 -5.5 2.425781 -5.320312 2.09375 -4.96875 C 1.769531 -4.625 1.597656 -4.179688 1.578125 -3.640625 Z M 3.28125 -6.421875 Z M 3.28125 -6.421875 "/> +</symbol> +<symbol overflow="visible" id="glyph0-5"> +<path style="stroke:none;" d=""/> +</symbol> +<symbol overflow="visible" id="glyph0-6"> +<path style="stroke:none;" d="M 4.640625 -8.828125 C 5.441406 -8.828125 6.140625 -8.671875 6.734375 -8.359375 C 7.585938 -7.910156 8.109375 -7.125 8.296875 -6 L 7.15625 -6 C 7.007812 -6.625 6.710938 -7.082031 6.265625 -7.375 C 5.828125 -7.664062 5.273438 -7.8125 4.609375 -7.8125 C 3.804688 -7.8125 3.132812 -7.507812 2.59375 -6.90625 C 2.050781 -6.3125 1.78125 -5.421875 1.78125 -4.234375 C 1.78125 -3.210938 2.003906 -2.378906 2.453125 -1.734375 C 2.898438 -1.097656 3.628906 -0.78125 4.640625 -0.78125 C 5.421875 -0.78125 6.066406 -1.003906 6.578125 -1.453125 C 7.085938 -1.898438 7.347656 -2.628906 7.359375 -3.640625 L 4.671875 -3.640625 L 4.671875 -4.609375 L 8.4375 -4.609375 L 8.4375 0 L 7.6875 0 L 7.40625 -1.109375 C 7.019531 -0.671875 6.671875 -0.367188 6.359375 -0.203125 C 5.847656 0.0859375 5.195312 0.234375 4.40625 0.234375 C 3.394531 0.234375 2.519531 -0.0976562 1.78125 -0.765625 C 0.976562 -1.585938 0.578125 -2.722656 0.578125 -4.171875 C 0.578125 -5.609375 0.96875 -6.753906 1.75 -7.609375 C 2.488281 -8.421875 3.453125 -8.828125 4.640625 -8.828125 Z M 4.4375 -8.84375 Z M 4.4375 -8.84375 "/> +</symbol> +<symbol overflow="visible" id="glyph0-7"> +<path style="stroke:none;" d="M 1.578125 -1.671875 C 1.578125 -1.367188 1.6875 -1.128906 1.90625 -0.953125 C 2.132812 -0.773438 2.398438 -0.6875 2.703125 -0.6875 C 3.078125 -0.6875 3.4375 -0.769531 3.78125 -0.9375 C 4.375 -1.226562 4.671875 -1.695312 4.671875 -2.34375 L 4.671875 -3.1875 C 4.535156 -3.113281 4.363281 -3.046875 4.15625 -2.984375 C 3.957031 -2.929688 3.757812 -2.894531 3.5625 -2.875 L 2.9375 -2.796875 C 2.550781 -2.742188 2.257812 -2.660156 2.0625 -2.546875 C 1.738281 -2.367188 1.578125 -2.078125 1.578125 -1.671875 Z M 4.140625 -3.796875 C 4.378906 -3.828125 4.539062 -3.929688 4.625 -4.109375 C 4.664062 -4.203125 4.6875 -4.335938 4.6875 -4.515625 C 4.6875 -4.867188 4.554688 -5.125 4.296875 -5.28125 C 4.046875 -5.445312 3.6875 -5.53125 3.21875 -5.53125 C 2.664062 -5.53125 2.273438 -5.382812 2.046875 -5.09375 C 1.910156 -4.925781 1.820312 -4.679688 1.78125 -4.359375 L 0.796875 -4.359375 C 0.816406 -5.128906 1.066406 -5.664062 1.546875 -5.96875 C 2.035156 -6.269531 2.597656 -6.421875 3.234375 -6.421875 C 3.972656 -6.421875 4.570312 -6.28125 5.03125 -6 C 5.488281 -5.71875 5.71875 -5.28125 5.71875 -4.6875 L 5.71875 -1.078125 C 5.71875 -0.972656 5.738281 -0.882812 5.78125 -0.8125 C 5.832031 -0.75 5.929688 -0.71875 6.078125 -0.71875 C 6.117188 -0.71875 6.164062 -0.71875 6.21875 -0.71875 C 6.28125 -0.726562 6.347656 -0.738281 6.421875 -0.75 L 6.421875 0.03125 C 6.253906 0.0703125 6.125 0.0976562 6.03125 0.109375 C 5.945312 0.128906 5.832031 0.140625 5.6875 0.140625 C 5.320312 0.140625 5.0625 0.0078125 4.90625 -0.25 C 4.8125 -0.382812 4.75 -0.578125 4.71875 -0.828125 C 4.5 -0.546875 4.1875 -0.300781 3.78125 -0.09375 C 3.382812 0.113281 2.945312 0.21875 2.46875 0.21875 C 1.882812 0.21875 1.40625 0.0390625 1.03125 -0.3125 C 0.664062 -0.664062 0.484375 -1.109375 0.484375 -1.640625 C 0.484375 -2.222656 0.664062 -2.675781 1.03125 -3 C 1.394531 -3.320312 1.867188 -3.519531 2.453125 -3.59375 Z M 3.265625 -6.421875 Z M 3.265625 -6.421875 "/> +</symbol> +<symbol overflow="visible" id="glyph0-8"> +<path style="stroke:none;" d="M 0.796875 -6.28125 L 1.8125 -6.28125 L 1.8125 -5.1875 C 1.882812 -5.40625 2.082031 -5.664062 2.40625 -5.96875 C 2.726562 -6.269531 3.097656 -6.421875 3.515625 -6.421875 C 3.535156 -6.421875 3.566406 -6.414062 3.609375 -6.40625 C 3.660156 -6.40625 3.742188 -6.398438 3.859375 -6.390625 L 3.859375 -5.28125 C 3.796875 -5.289062 3.738281 -5.296875 3.6875 -5.296875 C 3.632812 -5.296875 3.578125 -5.296875 3.515625 -5.296875 C 2.984375 -5.296875 2.570312 -5.125 2.28125 -4.78125 C 2 -4.445312 1.859375 -4.054688 1.859375 -3.609375 L 1.859375 0 L 0.796875 0 Z M 0.796875 -6.28125 "/> +</symbol> +<symbol overflow="visible" id="glyph0-9"> +<path style="stroke:none;" d="M 4.21875 -1 C 4.613281 -1 4.9375 -1.039062 5.1875 -1.125 C 5.644531 -1.269531 6.019531 -1.5625 6.3125 -2 C 6.539062 -2.34375 6.703125 -2.785156 6.796875 -3.328125 C 6.859375 -3.660156 6.890625 -3.960938 6.890625 -4.234375 C 6.890625 -5.304688 6.675781 -6.132812 6.25 -6.71875 C 5.832031 -7.3125 5.148438 -7.609375 4.203125 -7.609375 L 2.140625 -7.609375 L 2.140625 -1 Z M 0.96875 -8.609375 L 4.453125 -8.609375 C 5.640625 -8.609375 6.554688 -8.1875 7.203125 -7.34375 C 7.785156 -6.59375 8.078125 -5.625 8.078125 -4.4375 C 8.078125 -3.519531 7.90625 -2.691406 7.5625 -1.953125 C 6.957031 -0.648438 5.914062 0 4.4375 0 L 0.96875 0 Z M 0.96875 -8.609375 "/> +</symbol> +<symbol overflow="visible" id="glyph0-10"> +<path style="stroke:none;" d="M 0.984375 -8.03125 L 2.046875 -8.03125 L 2.046875 -6.28125 L 3.046875 -6.28125 L 3.046875 -5.421875 L 2.046875 -5.421875 L 2.046875 -1.3125 C 2.046875 -1.09375 2.125 -0.945312 2.28125 -0.875 C 2.351562 -0.832031 2.488281 -0.8125 2.6875 -0.8125 C 2.738281 -0.8125 2.789062 -0.8125 2.84375 -0.8125 C 2.90625 -0.820312 2.972656 -0.828125 3.046875 -0.828125 L 3.046875 0 C 2.929688 0.03125 2.804688 0.0507812 2.671875 0.0625 C 2.546875 0.0820312 2.40625 0.09375 2.25 0.09375 C 1.757812 0.09375 1.425781 -0.03125 1.25 -0.28125 C 1.070312 -0.53125 0.984375 -0.859375 0.984375 -1.265625 L 0.984375 -5.421875 L 0.140625 -5.421875 L 0.140625 -6.28125 L 0.984375 -6.28125 Z M 0.984375 -8.03125 "/> +</symbol> +<symbol overflow="visible" id="glyph1-0"> +<path style="stroke:none;" d="M 6.546875 -10.65625 L 1.625 -10.65625 L 1.625 -0.75 L 6.546875 -0.75 Z M 7.359375 -11.390625 L 7.359375 -0.015625 L 0.8125 -0.015625 L 0.8125 -11.390625 Z M 7.359375 -11.390625 "/> +</symbol> +<symbol overflow="visible" id="glyph1-1"> +<path style="stroke:none;" d="M 1.3125 -11.421875 L 1.3125 0 L 2.828125 0 L 2.828125 -11.421875 Z M 1.3125 -11.421875 "/> +</symbol> +<symbol overflow="visible" id="glyph1-2"> +<path style="stroke:none;" d="M 1.03125 -8.265625 L 1.03125 0 L 2.390625 0 L 2.390625 -4.671875 C 2.390625 -5.046875 2.4375 -5.390625 2.53125 -5.703125 C 2.632812 -6.015625 2.785156 -6.285156 2.984375 -6.515625 C 3.191406 -6.753906 3.445312 -6.9375 3.75 -7.0625 C 4.050781 -7.195312 4.410156 -7.265625 4.828125 -7.265625 C 5.347656 -7.265625 5.757812 -7.113281 6.0625 -6.8125 C 6.363281 -6.519531 6.515625 -6.113281 6.515625 -5.59375 L 6.515625 0 L 7.875 0 L 7.875 -5.4375 C 7.875 -5.882812 7.828125 -6.289062 7.734375 -6.65625 C 7.640625 -7.03125 7.476562 -7.347656 7.25 -7.609375 C 7.03125 -7.878906 6.738281 -8.085938 6.375 -8.234375 C 6.019531 -8.390625 5.570312 -8.46875 5.03125 -8.46875 C 3.800781 -8.46875 2.90625 -7.960938 2.34375 -6.953125 L 2.296875 -6.953125 L 2.296875 -8.265625 Z M 1.03125 -8.265625 "/> +</symbol> +<symbol overflow="visible" id="glyph1-3"> +<path style="stroke:none;" d="M 1.078125 -8.265625 L 1.078125 3.15625 L 2.4375 3.15625 L 2.4375 -1.109375 L 2.46875 -1.109375 C 2.613281 -0.859375 2.796875 -0.648438 3.015625 -0.484375 C 3.234375 -0.316406 3.460938 -0.1875 3.703125 -0.09375 C 3.953125 0 4.203125 0.0664062 4.453125 0.109375 C 4.703125 0.148438 4.929688 0.171875 5.140625 0.171875 C 5.765625 0.171875 6.3125 0.0625 6.78125 -0.15625 C 7.257812 -0.382812 7.65625 -0.691406 7.96875 -1.078125 C 8.289062 -1.460938 8.523438 -1.914062 8.671875 -2.4375 C 8.828125 -2.96875 8.90625 -3.523438 8.90625 -4.109375 C 8.90625 -4.691406 8.828125 -5.242188 8.671875 -5.765625 C 8.515625 -6.296875 8.273438 -6.757812 7.953125 -7.15625 C 7.640625 -7.5625 7.242188 -7.878906 6.765625 -8.109375 C 6.296875 -8.347656 5.742188 -8.46875 5.109375 -8.46875 C 4.523438 -8.46875 3.992188 -8.363281 3.515625 -8.15625 C 3.035156 -7.945312 2.6875 -7.613281 2.46875 -7.15625 L 2.4375 -7.15625 L 2.4375 -8.265625 Z M 7.46875 -4.203125 C 7.46875 -3.796875 7.425781 -3.398438 7.34375 -3.015625 C 7.257812 -2.640625 7.117188 -2.300781 6.921875 -2 C 6.734375 -1.695312 6.484375 -1.457031 6.171875 -1.28125 C 5.859375 -1.101562 5.460938 -1.015625 4.984375 -1.015625 C 4.515625 -1.015625 4.113281 -1.097656 3.78125 -1.265625 C 3.457031 -1.441406 3.191406 -1.675781 2.984375 -1.96875 C 2.773438 -2.257812 2.625 -2.59375 2.53125 -2.96875 C 2.4375 -3.34375 2.390625 -3.734375 2.390625 -4.140625 C 2.390625 -4.523438 2.429688 -4.90625 2.515625 -5.28125 C 2.609375 -5.65625 2.753906 -5.988281 2.953125 -6.28125 C 3.160156 -6.570312 3.421875 -6.804688 3.734375 -6.984375 C 4.054688 -7.171875 4.445312 -7.265625 4.90625 -7.265625 C 5.34375 -7.265625 5.722656 -7.175781 6.046875 -7 C 6.378906 -6.832031 6.648438 -6.601562 6.859375 -6.3125 C 7.066406 -6.03125 7.21875 -5.703125 7.3125 -5.328125 C 7.414062 -4.960938 7.46875 -4.585938 7.46875 -4.203125 Z M 7.46875 -4.203125 "/> +</symbol> +<symbol overflow="visible" id="glyph1-4"> +<path style="stroke:none;" d="M 7.875 0 L 7.875 -8.265625 L 6.515625 -8.265625 L 6.515625 -3.59375 C 6.515625 -3.226562 6.460938 -2.882812 6.359375 -2.5625 C 6.253906 -2.25 6.097656 -1.972656 5.890625 -1.734375 C 5.691406 -1.503906 5.441406 -1.328125 5.140625 -1.203125 C 4.835938 -1.078125 4.476562 -1.015625 4.0625 -1.015625 C 3.539062 -1.015625 3.128906 -1.160156 2.828125 -1.453125 C 2.535156 -1.753906 2.390625 -2.160156 2.390625 -2.671875 L 2.390625 -8.265625 L 1.03125 -8.265625 L 1.03125 -2.828125 C 1.03125 -2.378906 1.070312 -1.972656 1.15625 -1.609375 C 1.25 -1.242188 1.40625 -0.925781 1.625 -0.65625 C 1.851562 -0.382812 2.148438 -0.175781 2.515625 -0.03125 C 2.878906 0.101562 3.332031 0.171875 3.875 0.171875 C 4.476562 0.171875 5.003906 0.0507812 5.453125 -0.1875 C 5.898438 -0.425781 6.269531 -0.800781 6.5625 -1.3125 L 6.59375 -1.3125 L 6.59375 0 Z M 7.875 0 "/> +</symbol> +<symbol overflow="visible" id="glyph1-5"> +<path style="stroke:none;" d="M 2.90625 -8.265625 L 2.90625 -10.75 L 1.546875 -10.75 L 1.546875 -8.265625 L 0.140625 -8.265625 L 0.140625 -7.078125 L 1.546875 -7.078125 L 1.546875 -1.8125 C 1.546875 -1.425781 1.582031 -1.113281 1.65625 -0.875 C 1.738281 -0.644531 1.851562 -0.460938 2 -0.328125 C 2.15625 -0.203125 2.359375 -0.113281 2.609375 -0.0625 C 2.859375 -0.0195312 3.160156 0 3.515625 0 L 4.5625 0 L 4.5625 -1.203125 L 3.9375 -1.203125 C 3.71875 -1.203125 3.539062 -1.207031 3.40625 -1.21875 C 3.28125 -1.238281 3.175781 -1.273438 3.09375 -1.328125 C 3.019531 -1.378906 2.96875 -1.453125 2.9375 -1.546875 C 2.914062 -1.648438 2.90625 -1.78125 2.90625 -1.9375 L 2.90625 -7.078125 L 4.5625 -7.078125 L 4.5625 -8.265625 Z M 2.90625 -8.265625 "/> +</symbol> +<symbol overflow="visible" id="glyph1-6"> +<path style="stroke:none;" d=""/> +</symbol> +<symbol overflow="visible" id="glyph1-7"> +<path style="stroke:none;" d="M 2.765625 -1.28125 L 2.765625 -10.140625 L 5.328125 -10.140625 C 6.035156 -10.140625 6.628906 -10.039062 7.109375 -9.84375 C 7.585938 -9.644531 7.976562 -9.359375 8.28125 -8.984375 C 8.582031 -8.609375 8.800781 -8.148438 8.9375 -7.609375 C 9.070312 -7.066406 9.140625 -6.457031 9.140625 -5.78125 C 9.140625 -5.070312 9.066406 -4.46875 8.921875 -3.96875 C 8.773438 -3.476562 8.585938 -3.066406 8.359375 -2.734375 C 8.140625 -2.398438 7.890625 -2.132812 7.609375 -1.9375 C 7.328125 -1.75 7.039062 -1.601562 6.75 -1.5 C 6.457031 -1.40625 6.179688 -1.34375 5.921875 -1.3125 C 5.671875 -1.289062 5.460938 -1.28125 5.296875 -1.28125 Z M 1.25 -11.421875 L 1.25 0 L 5.171875 0 C 6.117188 0 6.9375 -0.128906 7.625 -0.390625 C 8.320312 -0.660156 8.894531 -1.046875 9.34375 -1.546875 C 9.789062 -2.054688 10.117188 -2.679688 10.328125 -3.421875 C 10.546875 -4.171875 10.65625 -5.023438 10.65625 -5.984375 C 10.65625 -7.816406 10.179688 -9.179688 9.234375 -10.078125 C 8.285156 -10.972656 6.929688 -11.421875 5.171875 -11.421875 Z M 1.25 -11.421875 "/> +</symbol> +<symbol overflow="visible" id="glyph1-8"> +<path style="stroke:none;" d="M 8.359375 -0.03125 C 8.117188 0.101562 7.789062 0.171875 7.375 0.171875 C 7.019531 0.171875 6.738281 0.0703125 6.53125 -0.125 C 6.320312 -0.320312 6.21875 -0.644531 6.21875 -1.09375 C 5.84375 -0.644531 5.40625 -0.320312 4.90625 -0.125 C 4.414062 0.0703125 3.882812 0.171875 3.3125 0.171875 C 2.9375 0.171875 2.582031 0.128906 2.25 0.046875 C 1.914062 -0.0351562 1.625 -0.164062 1.375 -0.34375 C 1.132812 -0.53125 0.941406 -0.769531 0.796875 -1.0625 C 0.648438 -1.351562 0.578125 -1.707031 0.578125 -2.125 C 0.578125 -2.59375 0.65625 -2.976562 0.8125 -3.28125 C 0.976562 -3.582031 1.191406 -3.820312 1.453125 -4 C 1.710938 -4.1875 2.007812 -4.328125 2.34375 -4.421875 C 2.675781 -4.523438 3.019531 -4.609375 3.375 -4.671875 C 3.75 -4.742188 4.101562 -4.796875 4.4375 -4.828125 C 4.769531 -4.867188 5.066406 -4.925781 5.328125 -5 C 5.585938 -5.070312 5.789062 -5.171875 5.9375 -5.296875 C 6.082031 -5.429688 6.15625 -5.628906 6.15625 -5.890625 C 6.15625 -6.191406 6.097656 -6.429688 5.984375 -6.609375 C 5.878906 -6.785156 5.738281 -6.921875 5.5625 -7.015625 C 5.382812 -7.117188 5.1875 -7.1875 4.96875 -7.21875 C 4.75 -7.25 4.53125 -7.265625 4.3125 -7.265625 C 3.738281 -7.265625 3.257812 -7.15625 2.875 -6.9375 C 2.488281 -6.71875 2.28125 -6.304688 2.25 -5.703125 L 0.890625 -5.703125 C 0.910156 -6.210938 1.015625 -6.640625 1.203125 -6.984375 C 1.398438 -7.335938 1.660156 -7.625 1.984375 -7.84375 C 2.304688 -8.0625 2.671875 -8.21875 3.078125 -8.3125 C 3.492188 -8.414062 3.9375 -8.46875 4.40625 -8.46875 C 4.769531 -8.46875 5.132812 -8.4375 5.5 -8.375 C 5.875 -8.320312 6.207031 -8.210938 6.5 -8.046875 C 6.800781 -7.890625 7.039062 -7.660156 7.21875 -7.359375 C 7.40625 -7.054688 7.5 -6.664062 7.5 -6.1875 L 7.5 -1.9375 C 7.5 -1.613281 7.515625 -1.378906 7.546875 -1.234375 C 7.585938 -1.085938 7.71875 -1.015625 7.9375 -1.015625 C 8.050781 -1.015625 8.191406 -1.039062 8.359375 -1.09375 Z M 6.140625 -4.265625 C 5.972656 -4.140625 5.75 -4.046875 5.46875 -3.984375 C 5.195312 -3.929688 4.90625 -3.882812 4.59375 -3.84375 C 4.289062 -3.8125 3.984375 -3.769531 3.671875 -3.71875 C 3.367188 -3.664062 3.09375 -3.585938 2.84375 -3.484375 C 2.601562 -3.378906 2.40625 -3.226562 2.25 -3.03125 C 2.09375 -2.832031 2.015625 -2.5625 2.015625 -2.21875 C 2.015625 -2 2.054688 -1.8125 2.140625 -1.65625 C 2.234375 -1.5 2.351562 -1.375 2.5 -1.28125 C 2.644531 -1.1875 2.8125 -1.117188 3 -1.078125 C 3.195312 -1.035156 3.398438 -1.015625 3.609375 -1.015625 C 4.054688 -1.015625 4.441406 -1.070312 4.765625 -1.1875 C 5.085938 -1.3125 5.347656 -1.46875 5.546875 -1.65625 C 5.753906 -1.84375 5.90625 -2.046875 6 -2.265625 C 6.09375 -2.484375 6.140625 -2.6875 6.140625 -2.875 Z M 6.140625 -4.265625 "/> +</symbol> +<symbol overflow="visible" id="glyph1-9"> +<path style="stroke:none;" d="M 9.796875 -1.421875 L 10.1875 0 L 11.15625 0 L 11.15625 -6.015625 L 6.140625 -6.015625 L 6.140625 -4.734375 L 9.796875 -4.734375 C 9.816406 -4.210938 9.742188 -3.722656 9.578125 -3.265625 C 9.421875 -2.816406 9.1875 -2.421875 8.875 -2.078125 C 8.5625 -1.742188 8.175781 -1.484375 7.71875 -1.296875 C 7.257812 -1.109375 6.726562 -1.015625 6.125 -1.015625 C 5.488281 -1.015625 4.925781 -1.140625 4.4375 -1.390625 C 3.957031 -1.640625 3.550781 -1.972656 3.21875 -2.390625 C 2.882812 -2.816406 2.628906 -3.300781 2.453125 -3.84375 C 2.285156 -4.394531 2.203125 -4.96875 2.203125 -5.5625 C 2.203125 -6.175781 2.273438 -6.769531 2.421875 -7.34375 C 2.578125 -7.925781 2.8125 -8.441406 3.125 -8.890625 C 3.4375 -9.347656 3.84375 -9.71875 4.34375 -10 C 4.84375 -10.28125 5.4375 -10.421875 6.125 -10.421875 C 6.550781 -10.421875 6.953125 -10.367188 7.328125 -10.265625 C 7.710938 -10.160156 8.050781 -10.003906 8.34375 -9.796875 C 8.644531 -9.597656 8.894531 -9.34375 9.09375 -9.03125 C 9.300781 -8.71875 9.441406 -8.34375 9.515625 -7.90625 L 11.046875 -7.90625 C 10.929688 -8.570312 10.726562 -9.144531 10.4375 -9.625 C 10.144531 -10.101562 9.78125 -10.492188 9.34375 -10.796875 C 8.914062 -11.109375 8.425781 -11.335938 7.875 -11.484375 C 7.332031 -11.628906 6.75 -11.703125 6.125 -11.703125 C 5.21875 -11.703125 4.425781 -11.53125 3.75 -11.1875 C 3.070312 -10.851562 2.503906 -10.398438 2.046875 -9.828125 C 1.597656 -9.265625 1.257812 -8.609375 1.03125 -7.859375 C 0.800781 -7.109375 0.6875 -6.316406 0.6875 -5.484375 C 0.6875 -4.742188 0.804688 -4.023438 1.046875 -3.328125 C 1.296875 -2.628906 1.65625 -2.015625 2.125 -1.484375 C 2.59375 -0.953125 3.160156 -0.53125 3.828125 -0.21875 C 4.503906 0.09375 5.269531 0.25 6.125 0.25 C 6.800781 0.25 7.46875 0.117188 8.125 -0.140625 C 8.789062 -0.398438 9.347656 -0.828125 9.796875 -1.421875 Z M 9.796875 -1.421875 "/> +</symbol> +<symbol overflow="visible" id="glyph1-10"> +<path style="stroke:none;" d="M 6.765625 -4.921875 L 2.015625 -4.921875 C 2.035156 -5.242188 2.101562 -5.546875 2.21875 -5.828125 C 2.34375 -6.109375 2.503906 -6.351562 2.703125 -6.5625 C 2.910156 -6.78125 3.15625 -6.953125 3.4375 -7.078125 C 3.71875 -7.203125 4.035156 -7.265625 4.390625 -7.265625 C 4.722656 -7.265625 5.03125 -7.203125 5.3125 -7.078125 C 5.601562 -6.953125 5.851562 -6.785156 6.0625 -6.578125 C 6.269531 -6.367188 6.429688 -6.117188 6.546875 -5.828125 C 6.671875 -5.546875 6.742188 -5.242188 6.765625 -4.921875 Z M 8.078125 -2.625 L 6.734375 -2.625 C 6.617188 -2.082031 6.375 -1.675781 6 -1.40625 C 5.632812 -1.144531 5.164062 -1.015625 4.59375 -1.015625 C 4.144531 -1.015625 3.753906 -1.085938 3.421875 -1.234375 C 3.085938 -1.378906 2.8125 -1.578125 2.59375 -1.828125 C 2.382812 -2.078125 2.234375 -2.363281 2.140625 -2.6875 C 2.046875 -3.019531 2.003906 -3.367188 2.015625 -3.734375 L 8.203125 -3.734375 C 8.222656 -4.234375 8.175781 -4.757812 8.0625 -5.3125 C 7.957031 -5.863281 7.757812 -6.375 7.46875 -6.84375 C 7.175781 -7.3125 6.785156 -7.695312 6.296875 -8 C 5.804688 -8.3125 5.195312 -8.46875 4.46875 -8.46875 C 3.894531 -8.46875 3.367188 -8.359375 2.890625 -8.140625 C 2.421875 -7.929688 2.015625 -7.632812 1.671875 -7.25 C 1.328125 -6.863281 1.054688 -6.410156 0.859375 -5.890625 C 0.671875 -5.367188 0.578125 -4.789062 0.578125 -4.15625 C 0.597656 -3.53125 0.691406 -2.945312 0.859375 -2.40625 C 1.023438 -1.875 1.269531 -1.414062 1.59375 -1.03125 C 1.925781 -0.65625 2.332031 -0.359375 2.8125 -0.140625 C 3.300781 0.0664062 3.878906 0.171875 4.546875 0.171875 C 5.484375 0.171875 6.257812 -0.0625 6.875 -0.53125 C 7.5 -1 7.898438 -1.695312 8.078125 -2.625 Z M 8.078125 -2.625 "/> +</symbol> +<symbol overflow="visible" id="glyph1-11"> +<path style="stroke:none;" d="M 0.96875 -8.265625 L 0.96875 0 L 2.34375 0 L 2.34375 -3.6875 C 2.34375 -4.21875 2.394531 -4.6875 2.5 -5.09375 C 2.601562 -5.507812 2.769531 -5.859375 3 -6.140625 C 3.238281 -6.429688 3.550781 -6.648438 3.9375 -6.796875 C 4.320312 -6.953125 4.785156 -7.03125 5.328125 -7.03125 L 5.328125 -8.46875 C 4.585938 -8.488281 3.976562 -8.335938 3.5 -8.015625 C 3.019531 -7.691406 2.613281 -7.195312 2.28125 -6.53125 L 2.25 -6.53125 L 2.25 -8.265625 Z M 0.96875 -8.265625 "/> +</symbol> +<symbol overflow="visible" id="glyph1-12"> +<path style="stroke:none;" d="M 2.125 -5.71875 C 2.125 -6.289062 2.195312 -6.851562 2.34375 -7.40625 C 2.5 -7.96875 2.734375 -8.472656 3.046875 -8.921875 C 3.367188 -9.367188 3.78125 -9.726562 4.28125 -10 C 4.789062 -10.28125 5.390625 -10.421875 6.078125 -10.421875 C 6.773438 -10.421875 7.375 -10.28125 7.875 -10 C 8.375 -9.726562 8.78125 -9.367188 9.09375 -8.921875 C 9.414062 -8.472656 9.648438 -7.96875 9.796875 -7.40625 C 9.953125 -6.851562 10.03125 -6.289062 10.03125 -5.71875 C 10.03125 -5.132812 9.953125 -4.5625 9.796875 -4 C 9.648438 -3.445312 9.414062 -2.945312 9.09375 -2.5 C 8.78125 -2.050781 8.375 -1.691406 7.875 -1.421875 C 7.375 -1.148438 6.773438 -1.015625 6.078125 -1.015625 C 5.390625 -1.015625 4.789062 -1.148438 4.28125 -1.421875 C 3.78125 -1.691406 3.367188 -2.050781 3.046875 -2.5 C 2.734375 -2.945312 2.5 -3.445312 2.34375 -4 C 2.195312 -4.5625 2.125 -5.132812 2.125 -5.71875 Z M 0.609375 -5.71875 C 0.609375 -4.9375 0.722656 -4.1875 0.953125 -3.46875 C 1.179688 -2.75 1.523438 -2.109375 1.984375 -1.546875 C 2.441406 -0.992188 3.007812 -0.554688 3.6875 -0.234375 C 4.375 0.0859375 5.171875 0.25 6.078125 0.25 C 6.984375 0.25 7.773438 0.0859375 8.453125 -0.234375 C 9.140625 -0.554688 9.710938 -0.992188 10.171875 -1.546875 C 10.628906 -2.109375 10.972656 -2.75 11.203125 -3.46875 C 11.429688 -4.1875 11.546875 -4.9375 11.546875 -5.71875 C 11.546875 -6.488281 11.429688 -7.234375 11.203125 -7.953125 C 10.972656 -8.679688 10.628906 -9.320312 10.171875 -9.875 C 9.710938 -10.425781 9.140625 -10.867188 8.453125 -11.203125 C 7.773438 -11.535156 6.984375 -11.703125 6.078125 -11.703125 C 5.171875 -11.703125 4.375 -11.535156 3.6875 -11.203125 C 3.007812 -10.867188 2.441406 -10.425781 1.984375 -9.875 C 1.523438 -9.320312 1.179688 -8.679688 0.953125 -7.953125 C 0.722656 -7.234375 0.609375 -6.488281 0.609375 -5.71875 Z M 0.609375 -5.71875 "/> +</symbol> +</g> +</defs> +<g id="surface1"> +<rect x="0" y="0" width="535" height="427" style="fill:rgb(100%,100%,100%);fill-opacity:1;stroke:none;"/> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 486 333 L 585 333 L 585 387 L 486 387 Z M 486 333 " transform="matrix(1,0,0,1,-268,-133)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph0-1" x="238.15039" y="231"/> + <use xlink:href="#glyph0-2" x="246.81679" y="231"/> + <use xlink:href="#glyph0-3" x="253.49119" y="231"/> + <use xlink:href="#glyph0-4" x="260.16559" y="231"/> + <use xlink:href="#glyph0-5" x="266.83999" y="231"/> + <use xlink:href="#glyph0-6" x="270.17839" y="231"/> + <use xlink:href="#glyph0-4" x="279.51679" y="231"/> + <use xlink:href="#glyph0-7" x="286.19119" y="231"/> + <use xlink:href="#glyph0-8" x="292.86559" y="231"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 279 144 L 459 144 L 459 549 L 279 549 Z M 279 144 " transform="matrix(1,0,0,1,-268,-133)"/> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 399.5 240.589844 C 418.832031 249.375 418.832031 263.625 399.5 272.410156 C 380.171875 281.195312 348.828125 281.195312 329.5 272.410156 C 310.167969 263.625 310.167969 249.375 329.5 240.589844 C 348.828125 231.804688 380.171875 231.804688 399.5 240.589844 " transform="matrix(1,0,0,1,-268,-133)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph0-9" x="68.82031" y="127.5"/> + <use xlink:href="#glyph0-7" x="77.48671" y="127.5"/> + <use xlink:href="#glyph0-10" x="84.16111" y="127.5"/> + <use xlink:href="#glyph0-7" x="87.49951" y="127.5"/> + <use xlink:href="#glyph0-5" x="94.17391" y="127.5"/> + <use xlink:href="#glyph0-6" x="97.51231" y="127.5"/> + <use xlink:href="#glyph0-4" x="106.85071" y="127.5"/> + <use xlink:href="#glyph0-7" x="113.52511" y="127.5"/> + <use xlink:href="#glyph0-8" x="120.19951" y="127.5"/> +</g> +<path style="fill:none;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 393.902344 275.011719 L 477.203125 327.453125 " transform="matrix(1,0,0,1,-268,-133)"/> +<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 483.972656 331.714844 L 478.800781 324.914062 L 475.605469 329.992188 Z M 483.972656 331.714844 " transform="matrix(1,0,0,1,-268,-133)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-1" x="44.248" y="58.776001"/> + <use xlink:href="#glyph1-2" x="48.392" y="58.776001"/> + <use xlink:href="#glyph1-3" x="57.288" y="58.776001"/> + <use xlink:href="#glyph1-4" x="66.776" y="58.776001"/> + <use xlink:href="#glyph1-5" x="75.672" y="58.776001"/> + <use xlink:href="#glyph1-6" x="80.712" y="58.776001"/> + <use xlink:href="#glyph1-7" x="85.16" y="58.776001"/> + <use xlink:href="#glyph1-8" x="96.424" y="58.776001"/> + <use xlink:href="#glyph1-5" x="105.016" y="58.776001"/> + <use xlink:href="#glyph1-8" x="110.056" y="58.776001"/> + <use xlink:href="#glyph1-6" x="118.648" y="58.776001"/> + <use xlink:href="#glyph1-9" x="123.096" y="58.776001"/> + <use xlink:href="#glyph1-10" x="135.24" y="58.776001"/> + <use xlink:href="#glyph1-8" x="143.832" y="58.776001"/> + <use xlink:href="#glyph1-11" x="152.424" y="58.776001"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 399.5 339.589844 C 418.832031 348.375 418.832031 362.625 399.5 371.410156 C 380.171875 380.195312 348.828125 380.195312 329.5 371.410156 C 310.167969 362.625 310.167969 348.375 329.5 339.589844 C 348.828125 330.804688 380.171875 330.804688 399.5 339.589844 " transform="matrix(1,0,0,1,-268,-133)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph0-9" x="68.82031" y="226.5"/> + <use xlink:href="#glyph0-7" x="77.48671" y="226.5"/> + <use xlink:href="#glyph0-10" x="84.16111" y="226.5"/> + <use xlink:href="#glyph0-7" x="87.49951" y="226.5"/> + <use xlink:href="#glyph0-5" x="94.17391" y="226.5"/> + <use xlink:href="#glyph0-6" x="97.51231" y="226.5"/> + <use xlink:href="#glyph0-4" x="106.85071" y="226.5"/> + <use xlink:href="#glyph0-7" x="113.52511" y="226.5"/> + <use xlink:href="#glyph0-8" x="120.19951" y="226.5"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 399.5 438.589844 C 418.832031 447.375 418.832031 461.625 399.5 470.410156 C 380.171875 479.195312 348.828125 479.195312 329.5 470.410156 C 310.167969 461.625 310.167969 447.375 329.5 438.589844 C 348.828125 429.804688 380.171875 429.804688 399.5 438.589844 " transform="matrix(1,0,0,1,-268,-133)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph0-9" x="68.82031" y="325.5"/> + <use xlink:href="#glyph0-7" x="77.48671" y="325.5"/> + <use xlink:href="#glyph0-10" x="84.16111" y="325.5"/> + <use xlink:href="#glyph0-7" x="87.49951" y="325.5"/> + <use xlink:href="#glyph0-5" x="94.17391" y="325.5"/> + <use xlink:href="#glyph0-6" x="97.51231" y="325.5"/> + <use xlink:href="#glyph0-4" x="106.85071" y="325.5"/> + <use xlink:href="#glyph0-7" x="113.52511" y="325.5"/> + <use xlink:href="#glyph0-8" x="120.19951" y="325.5"/> +</g> +<path style="fill:none;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 414.339844 357.335938 L 475.609375 359.589844 " transform="matrix(1,0,0,1,-268,-133)"/> +<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 483.601562 359.886719 L 475.71875 356.59375 L 475.5 362.589844 Z M 483.601562 359.886719 " transform="matrix(1,0,0,1,-268,-133)"/> +<path style="fill:none;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 396.285156 436.84375 L 477.347656 391.808594 " transform="matrix(1,0,0,1,-268,-133)"/> +<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 484.339844 387.921875 L 475.890625 389.183594 L 478.804688 394.429688 Z M 484.339844 387.921875 " transform="matrix(1,0,0,1,-268,-133)"/> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 612 216 L 792 216 L 792 477 L 612 477 Z M 612 216 " transform="matrix(1,0,0,1,-268,-133)"/> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 732.5 303.589844 C 751.832031 312.375 751.832031 326.625 732.5 335.410156 C 713.171875 344.195312 681.828125 344.195312 662.5 335.410156 C 643.167969 326.625 643.167969 312.375 662.5 303.589844 C 681.828125 294.804688 713.171875 294.804688 732.5 303.589844 " transform="matrix(1,0,0,1,-268,-133)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph0-9" x="401.82031" y="190.5"/> + <use xlink:href="#glyph0-7" x="410.48671" y="190.5"/> + <use xlink:href="#glyph0-10" x="417.16111" y="190.5"/> + <use xlink:href="#glyph0-7" x="420.49951" y="190.5"/> + <use xlink:href="#glyph0-5" x="427.17391" y="190.5"/> + <use xlink:href="#glyph0-6" x="430.51231" y="190.5"/> + <use xlink:href="#glyph0-4" x="439.85071" y="190.5"/> + <use xlink:href="#glyph0-7" x="446.52511" y="190.5"/> + <use xlink:href="#glyph0-8" x="453.19951" y="190.5"/> +</g> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph1-12" x="370.72" y="130.776001"/> + <use xlink:href="#glyph1-4" x="382.88" y="130.776001"/> + <use xlink:href="#glyph1-5" x="391.776" y="130.776001"/> + <use xlink:href="#glyph1-3" x="396.816" y="130.776001"/> + <use xlink:href="#glyph1-4" x="406.304" y="130.776001"/> + <use xlink:href="#glyph1-5" x="415.2" y="130.776001"/> + <use xlink:href="#glyph1-6" x="420.24" y="130.776001"/> + <use xlink:href="#glyph1-7" x="424.688" y="130.776001"/> + <use xlink:href="#glyph1-8" x="435.952" y="130.776001"/> + <use xlink:href="#glyph1-5" x="444.544" y="130.776001"/> + <use xlink:href="#glyph1-8" x="449.584" y="130.776001"/> + <use xlink:href="#glyph1-6" x="458.176" y="130.776001"/> + <use xlink:href="#glyph1-9" x="462.624" y="130.776001"/> + <use xlink:href="#glyph1-10" x="474.768" y="130.776001"/> + <use xlink:href="#glyph1-8" x="483.36" y="130.776001"/> + <use xlink:href="#glyph1-11" x="491.952" y="130.776001"/> +</g> +<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 732.5 384.589844 C 751.832031 393.375 751.832031 407.625 732.5 416.410156 C 713.171875 425.195312 681.828125 425.195312 662.5 416.410156 C 643.167969 407.625 643.167969 393.375 662.5 384.589844 C 681.828125 375.804688 713.171875 375.804688 732.5 384.589844 " transform="matrix(1,0,0,1,-268,-133)"/> +<g style="fill:rgb(0%,0%,0%);fill-opacity:1;"> + <use xlink:href="#glyph0-9" x="401.82031" y="271.5"/> + <use xlink:href="#glyph0-7" x="410.48671" y="271.5"/> + <use xlink:href="#glyph0-10" x="417.16111" y="271.5"/> + <use xlink:href="#glyph0-7" x="420.49951" y="271.5"/> + <use xlink:href="#glyph0-5" x="427.17391" y="271.5"/> + <use xlink:href="#glyph0-6" x="430.51231" y="271.5"/> + <use xlink:href="#glyph0-4" x="439.85071" y="271.5"/> + <use xlink:href="#glyph0-7" x="446.52511" y="271.5"/> + <use xlink:href="#glyph0-8" x="453.19951" y="271.5"/> +</g> +<path style="fill:none;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 585 348.378906 L 644.3125 333.152344 " transform="matrix(1,0,0,1,-268,-133)"/> +<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 652.0625 331.164062 L 643.566406 330.246094 L 645.058594 336.058594 Z M 652.0625 331.164062 " transform="matrix(1,0,0,1,-268,-133)"/> +<path style="fill:none;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 585 378 L 641.980469 389.394531 " transform="matrix(1,0,0,1,-268,-133)"/> +<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 649.828125 390.964844 L 642.570312 386.453125 L 641.394531 392.339844 Z M 649.828125 390.964844 " transform="matrix(1,0,0,1,-268,-133)"/> +</g> +</svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/pic/codeGear_dataGear.xbb Sun Jan 13 23:42:16 2019 +0900 @@ -0,0 +1,8 @@ +%%Title: ./codeGear_dataGear.pdf +%%Creator: extractbb 20180217 +%%BoundingBox: 0 0 535 427 +%%HiResBoundingBox: 0.000000 0.000000 535.000000 427.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Sun Jan 13 21:55:46 2019 +
--- a/slide/s6/themes/blank.css Sun Jan 13 03:51:48 2019 +0900 +++ b/slide/s6/themes/blank.css Sun Jan 13 23:42:16 2019 +0900 @@ -100,7 +100,7 @@ padding: 2px; } .smaller_code { - font-size: 180%; + font-size: 80%; padding: 2px; } code {
--- a/slide/slide.html Sun Jan 13 03:51:48 2019 +0900 +++ b/slide/slide.html Sun Jan 13 23:42:16 2019 +0900 @@ -93,46 +93,37 @@ <!-- _S9SLIDE_ --> -<h2 id="研究目的">研究目的</h2> -<!-- 後回しだ！！！！！ --> +<h2 id="研究背景">研究背景</h2> <ul> - <li>OS やアプリケーションなどの信頼性は重要な課題である。</li> - <li>プログラムの信頼性を上げるためには仕様を検証する必要がある。</li> - <li>使用の検証手法として Floyd-Hoare Logic (以下 HoareLogic) があり。 + <li>OS やアプリケーションなどの信頼性は重要な課題</li> + <li>信頼性を上げるために仕様を検証する必要</li> + <li>仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある <ul> - <li>これはプログラムを Pre、Post Condition(事前、事後条件)、Command (関数)</li> - </ul> - </li> - <li>当研究室では信頼性の高い OS として GearsOS を開発している。</li> - <li>GearsOS では CodeGear、 DataGear という単位を用いてプログラムを記述する手法を提案している。</li> - <li>OS やアプリケーションなど、ソフトウェアの信頼性を高めることは重要である。</li> - <li>そのために当研究室では CodeGear 、 DataGear という単位を用いてプログラムを記述する手法を提案している。 - <ul> - <li>CodeGear は処理の単位で、処理が終わると次の CodeGear へと継続を行う。</li> - <li>このとき、 CodeGear は通常の関数呼び出しとは異なり、呼び出し前の環境を持たずに継続をする。</li> - <li>DataGear はデータの単位で、 CodeGear の入力、出力変数となる。</li> + <li>事前条件(PreCondition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(PostCondition)を満たす</li> </ul> </li> - <li>また、当研究室では Gears の単位を用いて作られる OS である、 GearsOS を開発している。</li> - <li> - <p>本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた検証手法を提案する。</p> - </li> - <li>当研究室では検証しやすい単位として <strong>CodeGear</strong>、<strong>DataGear</strong> という単位を用いてプログラムを記述する手法を提案している + <li>既存の言語ではあまり利用されていない(python の pyrefine ってコードチェッカーくらい…?)</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="背景">背景</h2> +<ul> + <li>当研究室では 処理の単位を <strong>CodeGear</strong>、データの単位を <strong>DataGear</strong> としてプログラムを記述する手法を提案</li> + <li>CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む</li> + <li>Gear 間の接続処理はメタ計算として定義 <ul> - <li><strong>CodeGear</strong> とはプログラムを記述する際の処理の単位</li> - <li><strong>DataGear</strong> は CodeGear で扱うデータの単位</li> + <li>メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証</li> </ul> </li> - <li>これは関数型プログラミングに近い形になる</li> - <li>本研究では関数型言語であり、 <strong>証明支援系</strong> 言語でもある <strong>Agda</strong> を用いて仕様を検証することにしている</li> + <li>本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する</li> </ul> -<!-- * 動作するプログラムは高い信頼性を持っていてほしい --> -<!-- * そのために当研究室では CodeGear 、 DataGear を用いて記述する手法を提案している --> -<!-- * 処理の単位である CodeGear を継続しプログラムを記述していく --> -<!-- * メタ計算部分を切り替えることで CodeGear の処理を変更すること無くプログラムの検証をすることができる --> -<!-- * 継続に関数を呼び出すときの前提条件(pre-condition)を追加することができ、Hoare Logic を用いた証明を Agda で記述できると考えている --> -<!-- * 本研究では CodeGear, DataGear という単位を用いてプログラムを記述する手法の継続部分で Hoare Logic をベースにした証明手法を検討する --> +<p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt="" width="75%" height="75%" /></p> @@ -154,6 +145,9 @@ </li> </ul> +<!-- {} --> +<p style="text-align:center;"><img src="./pic/cgdg.svg" alt="" width="30%" height="30%" /></p> + </div> @@ -165,7 +159,7 @@ <li>Gears の単位でプログラミングできる言語として CbC (Continuation based C) が存在</li> <li>現在の CbC では assert での検証ができる</li> <li>将来的には証明も扱えるようにしたいが現段階では未実装</li> - <li>そのため Gears の単位を定理証明支援系の言語である <strong>Agda</strong> で記述できるようにし、 Agda 上で証明を行う</li> + <li>そのため Gears の単位を定理証明支援系の言語である <strong>Agda</strong> で記述し、 Agda 上で証明</li> </ul> @@ -193,12 +187,10 @@ <li>データ型は代数的なデータ構造</li> <li><strong>data</strong> キーワードの後に、<strong>名前 : 型</strong>、 where 句</li> <li>次の行以降は<strong>コンストラクタ名 : 型</strong></li> - <li>型は<strong>-></strong>または<strong>→</strong>で繋げる事ができる</li> - <li><strong>PrimComm -> Comm</strong>は<strong>PrimComm</strong> を受け取り、 <strong>Comm</strong>を返す型</li> - <li>再帰的な定義も可能</li> -</ul> - -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <li>型は<strong>-></strong>または<strong>→</strong>で繋げる</li> + <li>例えば、型<strong>PrimComm -> Comm</strong>は<strong>PrimComm</strong> を受け取り<strong>Comm</strong>を返す型</li> + <li>再帰的な定義も可能 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data Comm : Set where <span class="line-numbers"><a href="#n2" name="n2">2</a></span> Skip : Comm <span class="line-numbers"><a href="#n3" name="n3">3</a></span> Abort : Comm @@ -208,7 +200,9 @@ <span class="line-numbers"><a href="#n7" name="n7">7</a></span> While : Cond -> Comm -> Comm </pre></div> </div> -</div> + </div> + </li> +</ul> <!-- - where は宣言した部分に束縛する --> @@ -221,20 +215,24 @@ <h2 id="agda-のレコード型">Agda のレコード型</h2> <ul> <li>C 言語での構造体に近い</li> - <li>複数のデータ型をまとめる</li> + <li>複数のデータをまとめる</li> <li>関数内で構築できる</li> <li>構築時は<strong>レコード名 {フィールド名 = 値}</strong></li> - <li>複数ある場合は <strong>{フィールド1 = 1 ; フィールド2 = 2}</strong>のように <strong>;</strong> を使って列挙</li> -</ul> - -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record Env : Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> field -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> varn : ℕ -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> vari : ℕ + <li>複数ある場合は <strong>{フィールド1 = 1 ; フィールド2 = 2}</strong>のように <strong>;</strong> を使って列挙 + <ul> + <li>(varn,vari の型 <strong>ℕ</strong> は Agda 上の 自然数、 データ型で zero : ℕ と succ : ℕ -> ℕ で定義されてる) + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>record Env : Set where +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> field +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> varn : ℕ +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> vari : ℕ </pre></div> </div> -</div> + </div> + </li> + </ul> + </li> +</ul> @@ -247,17 +245,17 @@ <li>関数にも型が必要</li> <li>関数は <strong>関数名 = 値</strong></li> <li>関数ではパターンマッチがかける</li> - <li><strong>_</strong> は任意の引数</li> -</ul> - -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> _-_ : ℕ → ℕ → ℕ -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> x - zero = x -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> zero - _ = zero -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> (suc x) - (suc y) = x - y + <li><strong>_</strong> は任意の引数 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> _-_ : ℕ → ℕ → ℕ +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> x - zero = x +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> zero - _ = zero +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> (suc x) - (suc y) = x - y </pre></div> </div> -</div> + </div> + </li> +</ul> @@ -271,16 +269,16 @@ <li>関数自体にそれを満たす導出</li> <li>完成した関数は証明</li> <li><strong>{}</strong> は暗黙的(推論される)</li> - <li>下のコードは自然数に 0 を足したとき値が変わらないことの証明</li> -</ul> - -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>+zero : {y : ℕ} → y + zero ≡ y -<span class="line-numbers"><a href="#n2" name="n2">2</a></span>+zero {zero} = refl -<span class="line-numbers"><a href="#n3" name="n3">3</a></span>+zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) + <li>下のコードは自然数に 0 を足したとき値が変わらないことの証明 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> +zero : { y : ℕ } → y + zero ≡ y +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> +zero {zero} = refl +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) </pre></div> </div> -</div> + </div> + </li> +</ul> @@ -303,10 +301,8 @@ <!-- _S9SLIDE_ --> <h2 id="agda-での-hoarelogic-の理解">Agda での HoareLogic の理解</h2> <ul> - <li>HoareLogic を用いて次のようなプログラム(while Program)を検証した。</li> -</ul> - -<div class="language-C highlighter-coderay"><div class="CodeRay"> + <li>HoareLogic を用いて次のようなプログラム(while Program)を検証した。 + <div class="language-C highlighter-coderay"><div class="CodeRay"> <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>; <span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>; <span class="line-numbers"><a href="#n3" name="n3">3</a></span> @@ -317,8 +313,8 @@ <span class="line-numbers"><a href="#n8" name="n8">8</a></span> } </pre></div> </div> -</div> -<ul> + </div> + </li> <li>このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす</li> <li>n==0のとき停止するため、終了時の変数の結果はi==10、n==0 になるはずである。</li> </ul> @@ -347,10 +343,8 @@ <ul> <li>Env は while Program の変数である var n, i</li> <li><strong>PrimComm</strong> は代入時に使用される</li> - <li><strong>Cond</strong> は Condition で Env を受け取って Boolean の値を返す</li> -</ul> - -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <li><strong>Cond</strong> は Condition で Env を受け取って Boolean の値を返す + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span> record Env : Set where <span class="line-numbers"> <a href="#n2" name="n2">2</a></span> field <span class="line-numbers"> <a href="#n3" name="n3">3</a></span> varn : ℕ @@ -363,7 +357,9 @@ <span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> Cond = (Env → Bool) </pre></div> </div> -</div> + </div> + </li> +</ul> @@ -377,25 +373,25 @@ <ul> <li><strong>Skip</strong> は何も変更しない</li> <li><strong>PComm</strong> は変数を代入する</li> - <li><strong>Seq</strong> は Command を次の Command に移す</li> + <li><strong>Seq</strong> は Command を実行して次の Command に移す</li> <li><strong>If</strong> は Cond と2つの Comm を受け取り Cond の状態により実行する Comm を変える</li> - <li><strong>while</strong> は Cond と Comm を受け取り Cond の中身が真である間 Comm を繰り返す</li> + <li><strong>while</strong> は Cond と Comm を受け取り Cond の中身が真である間 Comm を繰り返す + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>data Comm : Set where +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> Skip : Comm +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Abort : Comm +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> PComm : PrimComm -> Comm +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> Seq : Comm -> Comm -> Comm +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> If : Cond -> Comm -> Comm -> Comm +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> While : Cond -> Comm -> Comm +</pre></div> +</div> + </div> + </li> </ul> </li> </ul> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data Comm : Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> Skip : Comm -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Abort : Comm -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> PComm : PrimComm -> Comm -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> Seq : Comm -> Comm -> Comm -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> If : Cond -> Comm -> Comm -> Comm -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> While : Cond -> Comm -> Comm -</pre></div> -</div> -</div> - </div> @@ -404,10 +400,14 @@ <!-- _S9SLIDE_ --> <h2 id="agda-上での-hoarelogic実際のプログラムの記述">Agda 上での HoareLogic(実際のプログラムの記述)</h2> <ul> - <li>先程の Comm を使ってwhile Program を記述した。</li> -</ul> - -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <li>Command を使って while Program を記述した。</li> + <li><strong>$</strong> は <strong>()</strong> の糖衣で行頭から行末までを ( ) で囲う + <ul> + <li>見やすさのため改行しているため 3~7 行はまとまっている</li> + </ul> + </li> + <li>Seq は Comm を2つ取って次の Comm に移行する + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> program : Comm <span class="line-numbers"><a href="#n2" name="n2">2</a></span> program = <span class="line-numbers"><a href="#n3" name="n3">3</a></span> Seq ( PComm (λ env → record env {varn = 10})) @@ -417,7 +417,9 @@ <span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ PComm (λ env → record env {varn = ((varn env) - 1)} )) </pre></div> </div> -</div> + </div> + </li> +</ul> @@ -427,22 +429,35 @@ <!-- _S9SLIDE_ --> <h2 id="agda-上での-hoarelogicの理解">Agda 上での HoareLogicの理解</h2> <ul> - <li>証明規則は HTProof にまとめられてる</li> - <li><strong>PrimRule</strong> は代入を</li> -</ul> - -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <li>規則は HTProof にまとめられてる</li> + <li><strong>PrimRule</strong> は <strong>PComm</strong> で行う代入を保証する</li> + <li>3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述 + <ul> + <li><strong><em>⇒</em></strong> は pre, post の Condition をとって post の Condition が成り立つときに True を返す関数</li> + </ul> + </li> + <li>SkipRule は PreCondition を変更しないことの保証</li> + <li>AbortRule は プログラムが停止するときのルール + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data HTProof : Cond -> Comm -> Cond -> Set where <span class="line-numbers"><a href="#n2" name="n2">2</a></span> PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} -> -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> (pr : Axiom bPre pcm bPost) -> -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> HTProof bPre (PComm pcm) bPost +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> (pr : Axiom bPre pcm bPost) -> +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> HTProof bPre (PComm pcm) bPost <span class="line-numbers"><a href="#n5" name="n5">5</a></span> SkipRule : (b : Cond) -> HTProof b Skip b <span class="line-numbers"><a href="#n6" name="n6">6</a></span> AbortRule : (bPre : Cond) -> (bPost : Cond) -> -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> HTProof bPre Abort bPost +<span class="line-numbers"><a href="#n7" name="n7">7</a></span> HTProof bPre Abort bPost <span class="line-numbers"><a href="#n8" name="n8">8</a></span>-- 次のスライドに続く </pre></div> </div> + </div> + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> Axiom : Cond -> PrimComm -> Cond -> Set +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true +</pre></div> </div> + </div> + </li> +</ul> @@ -452,10 +467,39 @@ <!-- _S9SLIDE_ --> <h2 id="agda-上での-hoarelogicの理解-1">Agda 上での HoareLogicの理解</h2> <ul> - <li></li> + <li><strong>SeqRule</strong> は Command を推移させる Seq の保証</li> + <li><strong>IfRule</strong> は If の Command が正しく動くことを保証 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>-- HTProof の続き +<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} -> +<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> {cm2 : Comm} -> {bPost : Cond} -> +<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> HTProof bPre cm1 bMid -> +<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> HTProof bMid cm2 bPost -> +<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> HTProof bPre (Seq cm1 cm2) bPost +<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> IfRule : {cmThen : Comm} -> {cmElse : Comm} -> +<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> {bPre : Cond} -> {bPost : Cond} -> +<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> {b : Cond} -> +<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> HTProof (bPre /\ b) cmThen bPost -> +<span class="line-numbers"><a href="#n11" name="n11">11</a></span> HTProof (bPre /\ neg b) cmElse bPost -> +<span class="line-numbers"><a href="#n12" name="n12">12</a></span> HTProof bPre (If b cmThen cmElse) bPost +</pre></div> +</div> + </div> + </li> </ul> -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="agda-上での-hoarelogicの理解-2">Agda 上での HoareLogicの理解</h2> +<ul> + <li><strong>WeakeningRule</strong> は通常の Condition からループ不変条件(Loop Invaliant)に変換</li> + <li>Tautology は Condition と不変条件が等しく成り立つ</li> + <li><strong>WhileRule</strong> はループ不変条件が成り立つ間 Comm を繰り返す + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>-- HTProof の続き <span class="line-numbers"> <a href="#n2" name="n2">2</a></span> WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} -> <span class="line-numbers"> <a href="#n3" name="n3">3</a></span> {bPost' : Cond} -> {bPost : Cond} -> @@ -463,23 +507,20 @@ <span class="line-numbers"> <a href="#n5" name="n5">5</a></span> HTProof bPre' cm bPost' -> <span class="line-numbers"> <a href="#n6" name="n6">6</a></span> Tautology bPost' bPost -> <span class="line-numbers"> <a href="#n7" name="n7">7</a></span> HTProof bPre cm bPost -<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} -> -<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> {cm2 : Comm} -> {bPost : Cond} -> -<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> HTProof bPre cm1 bMid -> -<span class="line-numbers"><a href="#n11" name="n11">11</a></span> HTProof bMid cm2 bPost -> -<span class="line-numbers"><a href="#n12" name="n12">12</a></span> HTProof bPre (Seq cm1 cm2) bPost -<span class="line-numbers"><a href="#n13" name="n13">13</a></span> IfRule : {cmThen : Comm} -> {cmElse : Comm} -> -<span class="line-numbers"><a href="#n14" name="n14">14</a></span> {bPre : Cond} -> {bPost : Cond} -> -<span class="line-numbers"><a href="#n15" name="n15">15</a></span> {b : Cond} -> -<span class="line-numbers"><a href="#n16" name="n16">16</a></span> HTProof (bPre /\ b) cmThen bPost -> -<span class="line-numbers"><a href="#n17" name="n17">17</a></span> HTProof (bPre /\ neg b) cmElse bPost -> -<span class="line-numbers"><a href="#n18" name="n18">18</a></span> HTProof bPre (If b cmThen cmElse) bPost -<span class="line-numbers"><a href="#n19" name="n19">19</a></span> WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> -<span class="line-numbers"><strong><a href="#n20" name="n20">20</a></strong></span> HTProof (bInv /\ b) cm bInv -> -<span class="line-numbers"><a href="#n21" name="n21">21</a></span> HTProof bInv (While b cm) (bInv /\ neg b) +<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> +<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> HTProof (bInv /\ b) cm bInv -> +<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> HTProof bInv (While b cm) (bInv /\ neg b) </pre></div> </div> + </div> + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> Tautology : Cond -> Cond -> Set +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true +</pre></div> </div> + </div> + </li> +</ul> @@ -488,20 +529,75 @@ <div class='slide'> <!-- _S9SLIDE_ --> <h2 id="agda-上での-hoarelogic証明">Agda 上での HoareLogic(証明)</h2> - -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proof1 : HTProof initCond program termCond -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proof1 = -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> SeqRule {λ e → true} ( PrimRule empty-case ) -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 ) -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 ( -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) -<span class="line-numbers"><a href="#n8" name="n8">8</a></span> $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 +<ul> + <li><strong>proof1</strong> は while Program の証明</li> + <li>HTProof に 初期状態とコマンドで書かれた <strong>program</strong> と終了状態を渡す</li> + <li>lemma1~5は rule それぞれの証明</li> + <li> + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>proof1 : HTProof initCond program termCond +<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>proof1 = +<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> SeqRule {λ e → true} ( PrimRule empty-case ) +<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 ) +<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 ( +<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} +<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) +<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 +<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> +<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span>initCond : Cond +<span class="line-numbers"><a href="#n11" name="n11">11</a></span>initCond env = true +<span class="line-numbers"><a href="#n12" name="n12">12</a></span> +<span class="line-numbers"><a href="#n13" name="n13">13</a></span>termCond : {c10 : ℕ} → Cond +<span class="line-numbers"><a href="#n14" name="n14">14</a></span>termCond {c10} env = Equal (vari env) c10 </pre></div> </div> + </div> + </li> +</ul> + +<p><!-- program : Comm --> + <!-- program = --> + <!-- Seq ( PComm (λ env → record env {varn = 10})) --> + <!-- $ Seq ( PComm (λ env → record env {vari = 0})) --> + <!-- $ While (λ env → lt zero (varn env ) ) --> + <!-- (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) --> + <!-- $ PComm (λ env → record env {varn = ((varn env) - 1)} )) --></p> + + + </div> +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="証明の一部">証明の一部</h2> +<ul> + <li>型だけ載せる</li> + <li>基本的な証明方法は Condtition を変化させて次の Condition が成り立つように変形する</li> + <li>impl⇒ + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span> lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) +<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in +<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> begin +<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> (Equal (varn env) c10 ) ∧ true +<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> ≡⟨ ∧true ⟩ +<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> Equal (varn env) c10 +<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> ≡⟨ cond ⟩ +<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> true +<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> ∎ ) +</pre></div> +</div> + </div> + + <p><!-- lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv --></p> + + <p><!-- lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' --></p> + + <p><!-- lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv --></p> + + <p><!-- lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond --></p> + </li> +</ul> + </div> @@ -515,7 +611,16 @@ <li><strong>名前 : 引数 -> (Code : fa -> t) -> t</strong></li> <li><strong>t</strong> は継続</li> <li><strong>(Code : fa -> t)</strong> は次の継続先</li> - <li>DataGear は Agda での CodeGear に使われる引数</li> + <li>DataGear は Agda での CodeGear に使われる引数 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>_g-_ : {t : Set} → ℕ → ℕ → (Code : ℕ → t) → t +<span class="line-numbers"><a href="#n2" name="n2">2</a></span>x g- zero next = next x +<span class="line-numbers"><a href="#n3" name="n3">3</a></span>zero g- _ = next zero +<span class="line-numbers"><a href="#n4" name="n4">4</a></span>(suc x) g- (suc y) = next (x g- y) +</pre></div> +</div> + </div> + </li> </ul> @@ -527,21 +632,19 @@ <h2 id="gears-をベースにした-hoarelogic">Gears をベースにした HoareLogic</h2> <ul> <li>次に Gears をベースにした while Program をみる。</li> - <li>このプログラムは c10</li> -</ul> - -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTest : {l : Level} {t : Set l} -> {c10 : ℕ } → (Code : (env : Env) -> -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileTest {_} {_} {c10} next = next env proof2 -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> where -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> env : Env -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> env = record {vari = 0 ; varn = c10} -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -<span class="line-numbers"><a href="#n8" name="n8">8</a></span> proof2 = record {pi1 = refl ; pi2 = refl} + <li>このプログラムは自然数と継続先を受け取って t を返す + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> {-# TERMINATING #-} +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileLoop : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) -> t +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileLoop env next with lt 0 (varn env) +<span class="line-numbers"><a href="#n4" name="n4">4</a></span> whileLoop env next | false = next env +<span class="line-numbers"><a href="#n5" name="n5">5</a></span> whileLoop env next | true = +<span class="line-numbers"><a href="#n6" name="n6">6</a></span> whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next </pre></div> </div> -</div> + </div> + </li> +</ul> @@ -551,15 +654,16 @@ <!-- _S9SLIDE_ --> <h2 id="gears-と-hoarelogic-をベースにした証明">Gears と HoareLogic をベースにした証明</h2> <ul> - <li>ここでは</li> -</ul> - -<div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proofGears : {c10 : ℕ } → Set -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proofGears {c10} = whileTest {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) + <li>ここでは + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proofGears : {c10 : ℕ } → Set +<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 +<span class="line-numbers"><a href="#n3" name="n3">3</a></span> (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) </pre></div> </div> -</div> + </div> + </li> +</ul> <p><–! [論文目次]
--- a/slide/slide.md Sun Jan 13 03:51:48 2019 +0900 +++ b/slide/slide.md Sun Jan 13 23:42:16 2019 +0900 @@ -5,36 +5,21 @@ <!-- 発表20分、質疑応答5分 --> -## 研究目的 -<!-- 後回しだ！！！！！ --> -- OS やアプリケーションなどの信頼性は重要な課題である。 -- プログラムの信頼性を上げるためには仕様を検証する必要がある。 -- 使用の検証手法として Floyd-Hoare Logic (以下 HoareLogic) があり。 - - これはプログラムを Pre、Post Condition(事前、事後条件)、Command (関数) -- 当研究室では信頼性の高い OS として GearsOS を開発している。 -- GearsOS では CodeGear、 DataGear という単位を用いてプログラムを記述する手法を提案している。 -- OS やアプリケーションなど、ソフトウェアの信頼性を高めることは重要である。 -- そのために当研究室では CodeGear 、 DataGear という単位を用いてプログラムを記述する手法を提案している。 - - CodeGear は処理の単位で、処理が終わると次の CodeGear へと継続を行う。 - - このとき、 CodeGear は通常の関数呼び出しとは異なり、呼び出し前の環境を持たずに継続をする。 - - DataGear はデータの単位で、 CodeGear の入力、出力変数となる。 -- また、当研究室では Gears の単位を用いて作られる OS である、 GearsOS を開発している。 -- 本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた検証手法を提案する。 +## 研究背景 +- OS やアプリケーションなどの信頼性は重要な課題 +- 信頼性を上げるために仕様を検証する必要 +- 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある + - 事前条件(PreCondition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(PostCondition)を満たす +- 既存の言語ではあまり利用されていない(python の pyrefine ってコードチェッカーくらい...?) -* 当研究室では検証しやすい単位として **CodeGear**、**DataGear** という単位を用いてプログラムを記述する手法を提案している - * **CodeGear** とはプログラムを記述する際の処理の単位 - * **DataGear** は CodeGear で扱うデータの単位 -* これは関数型プログラミングに近い形になる -* 本研究では関数型言語であり、 **証明支援系** 言語でもある **Agda** を用いて仕様を検証することにしている +## 背景 +- 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案 +- CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む +- Gear 間の接続処理はメタ計算として定義 + - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証 +- 本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する -<!-- * 動作するプログラムは高い信頼性を持っていてほしい --> -<!-- * そのために当研究室では CodeGear 、 DataGear を用いて記述する手法を提案している --> -<!-- * 処理の単位である CodeGear を継続しプログラムを記述していく --> -<!-- * メタ計算部分を切り替えることで CodeGear の処理を変更すること無くプログラムの検証をすることができる --> -<!-- * 継続に関数を呼び出すときの前提条件(pre-condition)を追加することができ、Hoare Logic を用いた証明を Agda で記述できると考えている --> -<!-- * 本研究では CodeGear, DataGear という単位を用いてプログラムを記述する手法の継続部分で Hoare Logic をベースにした証明手法を検討する --> - - +<p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt="" width="75%" height="75%"/></p> ## Gears について - **Gears** は当研究室で提案しているプログラム記述手法 @@ -45,11 +30,16 @@ - CodeGear の接続処理は通常の計算とは異なるメタ計算として定義 - メタ計算で信頼性の検証を行う +<!-- {} --> +<p style="text-align:center;"><img src="./pic/cgdg.svg" alt="" width="30%" height="30%"/></p> + ## CbC について -- Gears の単位でプログラミングできる言語として CbC (Continuation based C) が存在 -- 現在の CbC では assert での検証ができる +- Gears の単位でプログラミングできる言語として当研究室で開発している **CbC** (Continuation based C) が存在 + - これは C からループ制御構造と関数呼び出しを取り除き継続を導入したもの + - 環境を継続に含めない +- 現在の CbC ではメタ計算での検証 - 将来的には証明も扱えるようにしたいが現段階では未実装 -- そのため Gears の単位を定理証明支援系の言語である **Agda** で記述できるようにし、 Agda 上で証明を行う +- そのため Gears の単位を定理証明支援系の言語である **Agda** で記述し、 Agda で証明している ## Agda - Agda は定理証明支援系の言語 @@ -61,34 +51,33 @@ - データ型は代数的なデータ構造 - **data** キーワードの後に、**名前 : 型**、 where 句 - 次の行以降は**コンストラクタ名 : 型** -- 型は**->**または**→**で繋げる事ができる -- **PrimComm −> Comm**は**PrimComm** を受け取り、 **Comm**を返す型 +- 型は**->**または**→**で繋げる +- 例えば、型**PrimComm −> Comm**は**PrimComm** を受け取り**Comm**を返す型 - 再帰的な定義も可能 - ```AGDA - data Comm : Set where - Skip : Comm - Abort : Comm - PComm : PrimComm −> Comm - Seq : Comm −> Comm −> Comm - If : Cond −> Comm −> Comm −> Comm - While : Cond −> Comm −> Comm + data Comm : Set where + Skip : Comm + Abort : Comm + PComm : PrimComm −> Comm + Seq : Comm −> Comm −> Comm + If : Cond −> Comm −> Comm −> Comm + While : Cond −> Comm −> Comm ``` <!-- - where は宣言した部分に束縛する --> ## Agda のレコード型 - C 言語での構造体に近い -- 複数のデータ型をまとめる +- 複数のデータをまとめる - 関数内で構築できる - 構築時は**レコード名 {フィールド名 = 値}** - 複数ある場合は **{フィールド1 = 1 ; フィールド2 = 2}**のように **;** を使って列挙 - + - (varn,vari の型 **ℕ** は Agda 上の 自然数、 データ型で zero : ℕ と succ : ℕ -> ℕ で定義されてる) ```AGDA - record Env : Set where - field - varn : ℕ - vari : ℕ + record Env : Set where + field + varn : ℕ + vari : ℕ ``` ## Agda の関数 @@ -96,12 +85,11 @@ - 関数は **関数名 = 値** - 関数ではパターンマッチがかける - **_** は任意の引数 - ```AGDA - _−_ : ℕ → ℕ → ℕ - x − zero = x - zero − _ = zero - (suc x) − (suc y) = x − y + _-_ : ℕ → ℕ → ℕ + x - zero = x + zero - _ = zero + (suc x) - (suc y) = x - y ``` ## Agda での証明 @@ -110,11 +98,10 @@ - 完成した関数は証明 - **{}** は暗黙的(推論される) - 下のコードは自然数に 0 を足したとき値が変わらないことの証明 - ```AGDA -+zero : {y : ℕ} → y + zero ≡ y -+zero {zero} = refl -+zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) + +zero : { y : ℕ } → y + zero ≡ y + +zero {zero} = refl + +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) ``` ## Agda 上での HoareLogic @@ -125,16 +112,15 @@ ## Agda での HoareLogic の理解 * HoareLogic を用いて次のようなプログラム(while Program)を検証した。 - ```C - n = 10; - i = 0; + n = 10; + i = 0; - while (n>0) - { - i++; - n--; - } + while (n>0) + { + i++; + n--; + } ``` * このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす * n==0のとき停止するため、終了時の変数の結果はi==10、n==0 になるはずである。 @@ -150,109 +136,166 @@ * Env は while Program の変数である var n, i * **PrimComm** は代入時に使用される * **Cond** は Condition で Env を受け取って Boolean の値を返す +```AGDA + record Env : Set where + field + varn : ℕ + vari : ℕ -```AGDA - record Env : Set where - field - varn : ℕ - vari : ℕ + PrimComm : Set + PrimComm = Env → Env - PrimComm : Set - PrimComm = Env → Env - - Cond : Set - Cond = (Env → Bool) + Cond : Set + Cond = (Env → Bool) ``` ## Agda 上での HoareLogic(コマンド定義) * **Comm** は Agda のデータ型で定義した HoareLogic の Command * **Skip** は何も変更しない * **PComm** は変数を代入する - * **Seq** は Command を次の Command に移す + * **Seq** は Command を実行して次の Command に移す * **If** は Cond と2つの Comm を受け取り Cond の状態により実行する Comm を変える * **while** は Cond と Comm を受け取り Cond の中身が真である間 Comm を繰り返す - ```AGDA - data Comm : Set where - Skip : Comm - Abort : Comm - PComm : PrimComm -> Comm - Seq : Comm -> Comm -> Comm - If : Cond -> Comm -> Comm -> Comm - While : Cond -> Comm -> Comm + data Comm : Set where + Skip : Comm + Abort : Comm + PComm : PrimComm -> Comm + Seq : Comm -> Comm -> Comm + If : Cond -> Comm -> Comm -> Comm + While : Cond -> Comm -> Comm ``` ## Agda 上での HoareLogic(実際のプログラムの記述) -* 先程の Comm を使ってwhile Program を記述した。 - +* Command を使って while Program を記述した。 +* **$** は **()** の糖衣で行頭から行末までを ( ) で囲う + * 見やすさのため改行しているため 3~7 行はまとまっている +* Seq は Comm を2つ取って次の Comm に移行する ```AGDA - program : Comm - program = - Seq ( PComm (λ env → record env {varn = 10})) - $ Seq ( PComm (λ env → record env {vari = 0})) - $ While (λ env → lt zero (varn env ) ) - (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) - $ PComm (λ env → record env {varn = ((varn env) - 1)} )) + program : Comm + program = + Seq ( PComm (λ env → record env {varn = 10})) + $ Seq ( PComm (λ env → record env {vari = 0})) + $ While (λ env → lt zero (varn env ) ) + (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) + $ PComm (λ env → record env {varn = ((varn env) - 1)} )) ``` ## Agda 上での HoareLogicの理解 -* 証明規則は HTProof にまとめられてる -* **PrimRule** は代入を +* 規則は HTProof にまとめられてる +* **PrimRule** は **PComm** で行う代入を保証する +* 3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述 + * **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す関数 +* SkipRule は PreCondition を変更しないことの保証 +* AbortRule は プログラムが停止するときのルール +```AGDA + data HTProof : Cond -> Comm -> Cond -> Set where + PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} -> + (pr : Axiom bPre pcm bPost) -> + HTProof bPre (PComm pcm) bPost + SkipRule : (b : Cond) -> HTProof b Skip b + AbortRule : (bPre : Cond) -> (bPost : Cond) -> + HTProof bPre Abort bPost +-- 次のスライドに続く +``` +```AGDA + Axiom : Cond -> PrimComm -> Cond -> Set + Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true +``` +## Agda 上での HoareLogicの理解 +* **SeqRule** は Command を推移させる Seq の保証 +* **IfRule** は If の Command が正しく動くことを保証 +```AGDA +-- HTProof の続き + SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} -> + {cm2 : Comm} -> {bPost : Cond} -> + HTProof bPre cm1 bMid -> + HTProof bMid cm2 bPost -> + HTProof bPre (Seq cm1 cm2) bPost + IfRule : {cmThen : Comm} -> {cmElse : Comm} -> + {bPre : Cond} -> {bPost : Cond} -> + {b : Cond} -> + HTProof (bPre /\ b) cmThen bPost -> + HTProof (bPre /\ neg b) cmElse bPost -> + HTProof bPre (If b cmThen cmElse) bPost +``` +## Agda 上での HoareLogicの理解 +* **WeakeningRule** は通常の Condition からループ不変条件(Loop Invaliant)に変換 +* Tautology は Condition と不変条件が等しく成り立つ +* **WhileRule** はループ不変条件が成り立つ間 Comm を繰り返す ```AGDA - data HTProof : Cond -> Comm -> Cond -> Set where - PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} -> - (pr : Axiom bPre pcm bPost) -> - HTProof bPre (PComm pcm) bPost - SkipRule : (b : Cond) -> HTProof b Skip b - AbortRule : (bPre : Cond) -> (bPost : Cond) -> - HTProof bPre Abort bPost --- 次のスライドに続く +-- HTProof の続き + WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} -> + {bPost' : Cond} -> {bPost : Cond} -> + Tautology bPre bPre' -> + HTProof bPre' cm bPost' -> + Tautology bPost' bPost -> + HTProof bPre cm bPost + WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> + HTProof (bInv /\ b) cm bInv -> + HTProof bInv (While b cm) (bInv /\ neg b) +``` +```AGDA + Tautology : Cond -> Cond -> Set + Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true +``` + +## Agda 上での HoareLogic(証明) +* **proof1** は while Program の証明 +* HTProof に 初期状態とコマンドで書かれた **program** と終了状態を渡す +* lemma1~5は rule それぞれの証明 +* +```AGDA + proof1 : HTProof initCond program termCond + proof1 = + SeqRule {λ e → true} ( PrimRule empty-case ) + $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 + + initCond : Cond + initCond env = true + + termCond : {c10 : ℕ} → Cond + termCond {c10} env = Equal (vari env) c10 +``` + + <!-- program : Comm --> + <!-- program = --> + <!-- Seq ( PComm (λ env → record env {varn = 10})) --> + <!-- $ Seq ( PComm (λ env → record env {vari = 0})) --> + <!-- $ While (λ env → lt zero (varn env ) ) --> + <!-- (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) --> + <!-- $ PComm (λ env → record env {varn = ((varn env) - 1)} )) --> + +## 証明の一部 +- 基本的な証明方法は Condtition を変化させて次の Condition が成り立つように変形する +- impl⇒ +```AGDA + lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) + lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + (Equal (varn env) c10 ) ∧ true + ≡⟨ ∧true ⟩ + Equal (varn env) c10 + ≡⟨ cond ⟩ + true + ∎ ) ``` -## Agda 上での HoareLogicの理解 -* - -```AGDA --- HTProof の続き - WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} -> - {bPost' : Cond} -> {bPost : Cond} -> - Tautology bPre bPre' -> - HTProof bPre' cm bPost' -> - Tautology bPost' bPost -> - HTProof bPre cm bPost - SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} -> - {cm2 : Comm} -> {bPost : Cond} -> - HTProof bPre cm1 bMid -> - HTProof bMid cm2 bPost -> - HTProof bPre (Seq cm1 cm2) bPost - IfRule : {cmThen : Comm} -> {cmElse : Comm} -> - {bPre : Cond} -> {bPost : Cond} -> - {b : Cond} -> - HTProof (bPre /\ b) cmThen bPost -> - HTProof (bPre /\ neg b) cmElse bPost -> - HTProof bPre (If b cmThen cmElse) bPost - WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> - HTProof (bInv /\ b) cm bInv -> - HTProof bInv (While b cm) (bInv /\ neg b) -``` - -## Agda 上での HoareLogic(証明) - -```AGDA - proof1 : HTProof initCond program termCond - proof1 = - SeqRule {λ e → true} ( PrimRule empty-case ) - $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 ) - $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 ( - WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} - $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) - $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 -``` - + <!-- lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv --> + + <!-- lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' --> + + <!-- lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv --> + + <!-- lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond --> ## Agda での Gears - Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数 @@ -261,49 +304,37 @@ - **t** は継続 - **(Code : fa -> t)** は次の継続先 - DataGear は Agda での CodeGear に使われる引数 +```AGDA +_g-_ : {t : Set} → ℕ → ℕ → (Code : ℕ → t) → t +x g- zero next = next x +zero g- _ = next zero +(suc x) g- (suc y) = next (x g- y) +``` ## Gears をベースにした HoareLogic * 次に Gears をベースにした while Program をみる。 -* このプログラムは c10 - +* このプログラムは自然数と継続先を受け取って t を返す ```AGDA - whileTest : {l : Level} {t : Set l} -> {c10 : ℕ } → (Code : (env : Env) -> - ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t - whileTest {_} {_} {c10} next = next env proof2 - where - env : Env - env = record {vari = 0 ; varn = c10} - proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) - proof2 = record {pi1 = refl ; pi2 = refl} + {-# TERMINATING #-} + whileLoop : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) -> t + whileLoop env next with lt 0 (varn env) + whileLoop env next | false = next env + whileLoop env next | true = + whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next ``` ## Gears と HoareLogic をベースにした証明 * ここでは - ```AGDA - proofGears : {c10 : ℕ } → Set - proofGears {c10} = whileTest {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) + proofGears : {c10 : ℕ } → Set + proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 + (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) ``` -<--! -[論文目次] -まえがき - -現状 - -Agda - -GearsOS - -CodeGear DataGear - -Gears と Agda - -Agda での HoareLogic - -Gears ベースの HoareLogic - -まとめと課題 - ---> +## まとめと今後の課題 +- HoareLogic の while を使った例題を作成、証明を行った +- Gears を用いた HoareLogic ベースの検証方法を導入した + - 証明が引数として渡される記述のため証明とプログラムを一体化できた +- 今後の課題 + - RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)