Mercurial > hg > Papers > 2023 > moririn-sigos
changeset 0:170b950774a3
add files
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 15 Apr 2023 11:39:08 +0900 |
| parents | |
| children | 25fe88d3fb88 |
| files | fig/meta_cg_dg.graffle fig/meta_cg_dg.pdf fig/meta_cg_dg.svg fig/meta_cg_dg.xbb fig/meta_gear.svg fig/model_checking.svg gearsAgda.html gearsAgda.ind gearsAgda.md rbtree-gearsagda.mm rbtree.ind |
| diffstat | 11 files changed, 2260 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/meta_cg_dg.svg Sat Apr 15 11:39:08 2023 +0900 @@ -0,0 +1,130 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" viewBox="17.5 287.5 585.3511 421.08984" width="585.3511" height="421.08984"> + <defs> + <font-face font-family="Helvetica" font-size="9" units-per-em="1000" underline-position="-75.68359" underline-thickness="49.316406" slope="0" x-height="522.9492" cap-height="717.28516" ascent="770.0195" descent="-229.98047" font-weight="400"> + <font-face-src> + <font-face-name name="Helvetica"/> + </font-face-src> + </font-face> + <font-face font-family="Helvetica Neue" font-size="12" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400"> + <font-face-src> + <font-face-name name="HelveticaNeue"/> + </font-face-src> + </font-face> + <font-face font-family="Helvetica" font-size="12" units-per-em="1000" underline-position="-75.68359" underline-thickness="49.316406" slope="0" x-height="522.9492" cap-height="717.28516" ascent="770.0195" descent="-229.98047" font-weight="400"> + <font-face-src> + <font-face-name name="Helvetica"/> + </font-face-src> + </font-face> + <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"> + <g> + <path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> + </g> + </marker> + </defs> + <metadata> Produced by OmniGraffle 7.19.2\n2022-01-06 02:09:09 +0000</metadata> + <g id="Canvas_1" stroke-opacity="1" stroke="none" stroke-dasharray="none" fill="none" fill-opacity="1"> + <title>Canvas 1</title> + <g id="Canvas_1_Layer_1"> + <title>Layer 1</title> + <g id="Graphic_3"> + <text transform="translate(507.9492 692.58984)" fill="#945200"> + <tspan font-family="Helvetica" font-size="9" font-weight="400" fill="#945200" x="0" y="9"> </tspan> + </text> + </g> + <g id="Group_94"> + <g id="Graphic_96"> + <rect x="18" y="378" width="130.17553" height="90" fill="white"/> + <path d="M 18 378 L 148.17553 378 L 148.17553 468 L 18 468 Z" stroke="#ff9300" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/> + </g> + <g id="Graphic_95"> + <text transform="translate(38.798856 392)" fill="#c25800"> + <tspan font-family="Helvetica Neue" font-size="12" font-weight="400" fill="#c25800" x=".6286934" y="11">Meta Data Gear</tspan> + </text> + </g> + </g> + <g id="Group_91"> + <g id="Graphic_93"> + <rect x="472.17553" y="378" width="130.17553" height="90" fill="white"/> + <path d="M 472.17553 378 L 602.3511 378 L 602.3511 468 L 472.17553 468 Z" stroke="#ff9300" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/> + </g> + <g id="Graphic_92"> + <text transform="translate(492.9744 392)" fill="#c25800"> + <tspan font-family="Helvetica Neue" font-size="12" font-weight="400" fill="#c25800" x=".6286934" y="11">Meta Data Gear</tspan> + </text> + </g> + </g> + <g id="Graphic_121"> + <ellipse cx="310.17553" cy="436.5" rx="45.8794865380515" ry="22.5000359527927" fill="white"/> + <ellipse cx="310.17553" cy="436.5" rx="45.8794865380515" ry="22.5000359527927" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(278.472 429.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="2.353922" y="11">Code Gear</tspan> + </text> + </g> + <g id="Graphic_83"> + <rect x="45.65788" y="414" width="75.51765" height="45" fill="white"/> + <rect x="45.65788" y="414" width="75.51765" height="45" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(50.65788 429.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="5.07914" y="11">Data Gear</tspan> + </text> + </g> + <g id="Line_118"> + <line x1="121.67553" y1="436.5" x2="254.3961" y2="436.5" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="butt" stroke-linejoin="miter" stroke-width="1"/> + </g> + <g id="Graphic_120"> + <rect x="499.17553" y="414" width="75.51765" height="45" fill="white"/> + <rect x="499.17553" y="414" width="75.51765" height="45" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(504.17553 429.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="5.07914" y="11">Data Gear</tspan> + </text> + </g> + <g id="Line_116"> + <line x1="356.05497" y1="436.5" x2="488.77553" y2="436.5" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="butt" stroke-linejoin="miter" stroke-width="1"/> + </g> + <g id="Graphic_117"> + <ellipse cx="418.437" cy="436.5" rx="45.4435686903338" ry="22.5000359527927" fill="white"/> + <path d="M 450.57035 420.5901 C 468.3172 429.3769 468.3172 443.6231 450.57035 452.4099 C 432.82357 461.1967 404.0504 461.1967 386.3036 452.4099 C 368.55674 443.6231 368.55674 429.3769 386.3036 420.5901 C 404.0504 411.8033 432.82357 411.8033 450.57035 420.5901" stroke="#ff9300" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/> + <text transform="translate(387.0822 422.5)" fill="#c25800"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="#c25800" x="18.01593" y="11">Meta </tspan> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="#c25800" x="2.005188" y="25">Code Gear</tspan> + </text> + </g> + <g id="Graphic_103"> + <ellipse cx="310.17553" cy="310.5" rx="44.2896033411883" ry="22.5000359527927" fill="white"/> + <ellipse cx="310.17553" cy="310.5" rx="44.2896033411883" ry="22.5000359527927" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(279.7439 303.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="1.082016" y="11">Code Gear</tspan> + </text> + </g> + <g id="Graphic_104"> + <rect x="45.65788" y="288" width="75.51765" height="45" fill="white"/> + <rect x="45.65788" y="288" width="75.51765" height="45" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(50.65788 303.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="5.07914" y="11">Data Gear</tspan> + </text> + </g> + <g id="Line_105"> + <line x1="121.67553" y1="310.5" x2="255.98598" y2="310.5" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="butt" stroke-linejoin="miter" stroke-width="1"/> + </g> + <g id="Graphic_106"> + <rect x="499.17553" y="288" width="75.51765" height="45" fill="white"/> + <rect x="499.17553" y="288" width="75.51765" height="45" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + <text transform="translate(504.17553 303.5)" fill="black"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="black" x="5.07914" y="11">Data Gear</tspan> + </text> + </g> + <g id="Line_107"> + <line x1="354.4651" y1="310.5" x2="488.77553" y2="310.5" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="butt" stroke-linejoin="miter" stroke-width="1"/> + </g> + <g id="Graphic_122"> + <ellipse cx="200.39427" cy="436.5" rx="45.4435686903337" ry="22.5000359527927" fill="white"/> + <path d="M 232.52763 420.5901 C 250.2745 429.3769 250.2745 443.6231 232.52763 452.4099 C 214.78086 461.1967 186.00767 461.1967 168.2609 452.4099 C 150.51403 443.6231 150.51403 429.3769 168.2609 420.5901 C 186.00767 411.8033 214.78086 411.8033 232.52763 420.5901" stroke="#ff9300" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/> + <text transform="translate(169.03947 422.5)" fill="#c25800"> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="#c25800" x="18.01593" y="11">Meta </tspan> + <tspan font-family="Helvetica" font-size="12" font-weight="400" fill="#c25800" x="2.005188" y="25">Code Gear</tspan> + </text> + </g> + </g> + </g> +</svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/meta_cg_dg.xbb Sat Apr 15 11:39:08 2023 +0900 @@ -0,0 +1,8 @@ +%%Title: fig/meta_cg_dg.pdf +%%Creator: extractbb 20190225 +%%BoundingBox: 0 0 608 202 +%%HiResBoundingBox: 0.000000 0.000000 608.000000 202.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Wed Feb 5 17:52:45 2020 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/meta_gear.svg Sat Apr 15 11:39:08 2023 +0900 @@ -0,0 +1,376 @@ +<?xml version="1.0" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 20010904//EN" + "http://www.w3.org/TR/2001/REC-SVG-20010904/DTD/svg10.dtd"> +<svg version="1.0" xmlns="http://www.w3.org/2000/svg" + width="792.000000pt" height="532.000000pt" viewBox="0 0 792.000000 532.000000" + preserveAspectRatio="xMidYMid meet"> +<metadata> +Created by potrace 1.16, written by Peter Selinger 2001-2019 +</metadata> +<g transform="translate(0.000000,532.000000) scale(0.100000,-0.100000)" +fill="#000000" stroke="none"> +<path d="M3030 5090 c0 -126 -2 -230 -4 -230 -2 0 -48 9 -101 20 -53 11 -99 +20 -101 20 -2 0 -4 -13 -4 -30 0 -16 -5 -30 -11 -30 -14 0 -1281 -198 -1321 +-206 l-28 -6 0 106 0 106 -730 0 -730 0 0 -355 0 -355 730 0 730 0 0 110 0 +110 28 -1 c15 0 320 -44 677 -97 l650 -98 3 -27 c4 -31 8 -32 99 -12 37 9 78 +18 91 20 l22 5 0 -230 0 -230 733 2 732 3 3 212 c2 211 3 213 25 218 12 3 380 +52 817 110 437 58 810 108 828 112 31 5 32 4 32 -27 l0 -32 95 51 c53 28 98 +51 100 51 3 0 5 -56 5 -125 l0 -125 730 0 730 0 0 355 0 355 -730 0 -729 0 -3 +-119 -3 -118 -85 48 c-47 26 -91 48 -97 48 -7 1 -13 -10 -13 -24 0 -17 -5 -25 +-17 -25 -10 1 -391 54 -848 118 l-830 118 -3 217 -2 217 -735 0 -735 0 0 -230z +m1450 1 c0 -130 -4 -212 -10 -216 -7 -4 -7 -12 0 -25 5 -10 10 -64 10 -119 l0 +-101 -715 0 -715 0 0 335 0 335 715 0 715 0 0 -209z m-715 -481 l735 0 0 110 +c0 98 2 110 18 110 9 0 384 -52 832 -115 448 -63 821 -115 828 -115 10 0 12 +-8 7 -30 -4 -16 -3 -30 2 -30 4 0 54 11 111 24 l102 23 0 -93 c0 -52 -2 -94 +-4 -94 -6 0 -177 40 -200 47 -16 4 -17 1 -11 -25 6 -29 4 -30 -32 -36 -93 -15 +-1613 -216 -1632 -216 -20 0 -21 5 -21 110 l0 110 -735 0 -734 0 -3 -115 -3 +-114 -89 49 c-49 28 -90 50 -91 50 -2 0 -6 -13 -10 -28 l-6 -28 -682 102 +c-375 56 -683 103 -684 103 -5 2 -3 171 1 171 3 0 307 47 676 105 368 58 675 +105 680 105 5 0 12 -11 16 -25 3 -14 9 -25 13 -25 3 0 44 22 91 49 l85 49 3 +-114 3 -114 734 0z m-2326 -120 l0 -340 -715 0 -714 0 0 340 0 340 714 0 715 +0 0 -340z m6401 0 l0 -340 -715 0 -715 0 0 340 0 340 715 0 715 0 0 -340z +m-3360 -216 c0 -58 -5 -114 -10 -124 -7 -13 -7 -21 0 -25 6 -4 10 -86 10 -216 +l0 -209 -715 0 -715 0 0 340 0 340 715 0 715 0 0 -106z"/> +<path d="M3420 4970 c0 -60 0 -60 29 -60 37 0 61 23 61 60 0 37 -24 60 -61 60 +-29 0 -29 0 -29 -60z m69 34 c10 -10 3 -67 -10 -75 -36 -22 -49 -11 -49 42 0 +51 0 51 27 44 16 -4 30 -9 32 -11z"/> +<path d="M3630 5018 c0 -9 -6 -19 -12 -21 -10 -4 -10 -6 0 -6 7 -1 12 -16 12 +-41 0 -22 3 -40 8 -40 8 0 6 109 -2 118 -3 3 -6 -2 -6 -10z"/> +<path d="M3806 5014 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M3527 4994 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3667 4994 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3921 4986 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M4007 4994 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -30 0 -17 6 -20 45 -19 41 0 45 3 45 26 0 14 7 33 16 +43 15 17 15 18 -5 16 -17 -1 -21 -8 -22 -37 l-2 -35 -6 35 c-5 28 -11 36 -31 +38 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M366 4534 c-19 -18 -21 -75 -4 -92 17 -17 54 -15 73 4 22 22 10 31 +-13 10 -22 -19 -49 -12 -57 15 -15 46 24 82 56 53 17 -15 19 -15 19 -2 0 29 +-49 37 -74 12z"/> +<path d="M620 4532 c0 -13 -8 -18 -27 -17 -26 0 -28 -3 -28 -40 0 -38 1 -40 +33 -41 l32 -1 0 59 c0 32 -2 58 -5 58 -3 0 -5 -8 -5 -18z m-11 -74 c-6 -11 +-16 -17 -22 -15 -17 5 -21 36 -6 53 12 14 14 14 26 -1 9 -13 9 -23 2 -37z"/> +<path d="M796 4534 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M470 4506 c-28 -35 11 -93 48 -70 35 22 22 84 -18 84 -10 0 -23 -7 +-30 -14z m54 -21 c2 -7 -1 -21 -9 -31 -11 -15 -15 -16 -29 -5 -19 16 -20 33 +-5 48 13 13 35 7 43 -12z"/> +<path d="M661 4506 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 15 +5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 -16 +16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 14 +15 15 15 1 0 8 -7 15 -15z"/> +<path d="M911 4506 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 15 +5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 -16 +16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 14 +15 15 15 1 0 8 -7 15 -15z"/> +<path d="M997 4514 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -30 0 -17 6 -20 45 -19 41 0 45 3 45 26 0 14 7 33 16 +43 15 17 15 18 -5 16 -17 -1 -21 -8 -22 -37 l-2 -35 -6 35 c-5 28 -11 36 -31 +38 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M6766 4534 c-19 -18 -21 -75 -4 -92 17 -17 54 -15 73 4 22 22 10 31 +-13 10 -22 -19 -49 -12 -57 15 -15 46 24 82 56 53 17 -15 19 -15 19 -2 0 29 +-49 37 -74 12z"/> +<path d="M7020 4532 c0 -13 -8 -18 -27 -17 -26 0 -28 -3 -28 -40 0 -38 1 -40 +33 -41 l32 -1 0 59 c0 32 -2 58 -5 58 -3 0 -5 -8 -5 -18z m-11 -74 c-6 -11 +-16 -17 -22 -15 -17 5 -21 36 -6 53 12 14 14 14 26 -1 9 -13 9 -23 2 -37z"/> +<path d="M7196 4534 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M6870 4506 c-28 -35 11 -93 48 -70 35 22 22 84 -18 84 -10 0 -23 -7 +-30 -14z m54 -21 c2 -7 -1 -21 -9 -31 -11 -15 -15 -16 -29 -5 -19 16 -20 33 +-5 48 13 13 35 7 43 -12z"/> +<path d="M7061 4506 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M7311 4506 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M7397 4514 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -30 0 -17 6 -20 45 -19 41 0 45 3 45 26 0 14 7 33 16 +43 15 17 15 18 -5 16 -17 -1 -21 -8 -22 -37 l-2 -35 -6 35 c-5 28 -11 36 -31 +38 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3420 4040 c0 -60 0 -60 29 -60 37 0 61 23 61 60 0 37 -24 60 -61 60 +-29 0 -29 0 -29 -60z m69 34 c10 -10 3 -67 -10 -75 -36 -22 -49 -11 -49 42 0 +51 0 51 27 44 16 -4 30 -9 32 -11z"/> +<path d="M3630 4088 c0 -9 -6 -19 -12 -21 -10 -4 -10 -6 0 -6 7 -1 12 -16 12 +-41 0 -22 3 -40 8 -40 8 0 6 109 -2 118 -3 3 -6 -2 -6 -10z"/> +<path d="M3806 4084 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M3527 4064 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3667 4064 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3921 4056 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M4007 4064 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -30 0 -17 6 -20 45 -19 41 0 45 3 45 26 0 14 7 33 16 +43 15 17 15 18 -5 16 -17 -1 -21 -8 -22 -37 l-2 -35 -6 35 c-5 28 -11 36 -31 +38 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3090 2795 l0 -175 361 0 c340 0 361 -1 354 -17 -17 -43 -65 -175 +-65 -179 0 -2 14 -4 30 -4 28 0 30 -3 30 -35 l0 -35 -355 0 -355 0 0 -282 0 +-281 -110 7 c-60 3 -110 4 -110 2 0 -3 4 -16 9 -29 9 -23 7 -25 -52 -42 -34 +-9 -70 -20 -79 -22 -16 -5 -18 4 -18 86 l0 91 -475 0 -475 0 0 -174 0 -174 +-102 39 c-57 21 -104 39 -105 39 -2 0 -3 -13 -3 -30 0 -25 -4 -30 -25 -30 +l-25 0 0 165 0 165 -730 0 -730 0 0 -355 0 -355 730 0 730 0 0 165 0 165 25 0 +c21 0 25 -5 25 -30 0 -16 1 -30 3 -30 1 0 48 18 105 39 l102 39 0 -174 0 -174 +475 0 475 0 0 96 c0 73 3 95 13 92 6 -3 42 -13 79 -23 64 -17 66 -18 57 -42 +-5 -13 -9 -27 -9 -30 0 -5 128 4 188 13 l32 5 0 -281 0 -280 355 0 355 0 0 +-40 c0 -38 -1 -40 -31 -40 -26 0 -30 -3 -24 -17 17 -43 65 -175 65 -179 0 -2 +-162 -4 -360 -4 l-360 0 0 -175 0 -175 733 2 732 3 3 172 2 173 -363 2 -364 3 +33 85 c40 104 40 110 9 110 -22 0 -25 4 -25 40 l0 40 355 0 355 0 0 255 0 254 +38 10 c79 21 366 91 374 91 4 0 8 -6 8 -12 0 -7 4 -19 9 -27 7 -11 26 -2 90 +42 44 32 83 57 86 57 3 0 5 -49 5 -110 l0 -110 480 0 480 0 0 165 0 165 60 0 +60 0 0 -30 c0 -16 1 -30 3 -30 1 0 48 18 105 39 l102 39 0 -174 0 -174 730 0 +730 0 0 355 0 355 -730 0 -730 0 0 -174 0 -174 -102 39 c-57 21 -104 39 -105 +39 -2 0 -3 -13 -3 -30 l0 -30 -60 0 -60 0 0 165 0 165 -480 0 -480 0 0 -110 0 +-110 -84 60 c-90 64 -96 67 -96 48 -1 -42 -12 -42 -224 13 l-206 54 0 257 0 +258 -355 0 -355 0 0 35 c0 31 3 35 25 35 32 0 31 9 -5 103 -16 43 -30 82 -30 +88 0 5 147 10 358 11 l357 3 3 173 2 172 -735 0 -735 0 0 -175z m1450 0 l0 +-155 -715 0 -715 0 0 155 0 155 715 0 715 0 0 -155z m-730 -465 c13 -7 21 -7 +25 0 4 6 133 10 356 10 l349 0 0 -254 c0 -160 -4 -257 -10 -261 -7 -4 -7 -12 +0 -25 5 -10 10 -46 10 -79 l0 -61 -715 0 -715 0 0 340 0 340 341 0 c208 0 348 +-4 359 -10z m-2311 -805 l0 -335 -714 0 -715 0 0 335 0 335 715 0 714 0 0 +-335z m1210 0 l0 -335 -460 0 -459 0 0 335 0 335 459 0 460 0 0 -335z m3401 +176 c0 -96 -4 -162 -10 -166 -7 -4 -7 -12 0 -25 5 -10 10 -86 10 -169 l0 -151 +-460 0 -460 0 0 335 0 335 460 0 460 0 0 -159z m1790 -176 l0 -335 -715 0 +-715 0 0 335 0 335 715 0 715 0 0 -335z m-3109 196 c164 -43 176 -47 168 -66 +-14 -35 -10 -37 46 -31 30 3 80 9 110 12 l55 6 0 -112 0 -113 -72 7 c-40 4 +-90 10 -111 13 -37 6 -37 5 -31 -24 l6 -30 -201 -50 -201 -51 0 74 0 74 -735 +0 -734 0 -3 -66 -3 -65 -80 60 c-44 33 -83 61 -87 61 -5 0 -8 -9 -8 -19 0 -32 +-14 -33 -100 -9 l-81 23 3 114 3 114 75 24 c41 12 78 23 83 23 4 0 12 -12 17 +-26 l10 -26 38 28 c20 15 56 42 79 61 23 18 44 33 47 33 3 0 6 -27 6 -60 l0 +-60 733 2 732 3 3 68 3 67 27 -7 c15 -3 106 -27 203 -52z m-251 -380 c0 -39 +-5 -73 -10 -76 -7 -4 -7 -12 0 -25 6 -11 10 -118 10 -259 l0 -241 -715 0 -715 +0 0 335 0 335 715 0 715 0 0 -69z m0 -1076 l0 -155 -715 0 -715 0 0 155 0 155 +715 0 715 0 0 -155z"/> +<path d="M3472 2798 c2 -62 2 -62 6 -13 l4 50 17 -45 c9 -25 21 -44 26 -42 6 +1 17 21 25 45 l15 42 6 -50 6 -50 1 63 c1 34 -2 62 -7 62 -5 0 -17 -20 -27 +-45 -19 -50 -26 -49 -44 8 -18 56 -30 45 -28 -25z"/> +<path d="M3700 2848 c0 -9 -6 -19 -12 -21 -10 -4 -10 -6 0 -6 7 -1 12 -16 12 +-41 0 -22 3 -40 8 -40 8 0 6 109 -2 118 -3 3 -6 -2 -6 -10z"/> +<path d="M3876 2844 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M3611 2816 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M3737 2824 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3991 2816 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M4077 2824 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M4161 2780 c2 -34 3 -37 6 -15 3 17 12 38 20 47 14 15 13 17 -6 15 +-18 -1 -21 -7 -20 -47z"/> +<path d="M3480 2000 c0 -60 0 -60 29 -60 37 0 61 23 61 60 0 37 -24 60 -61 60 +-29 0 -29 0 -29 -60z m69 34 c10 -10 3 -67 -10 -75 -36 -22 -49 -11 -49 42 0 +51 0 51 27 44 16 -4 30 -9 32 -11z"/> +<path d="M3690 2048 c0 -9 -6 -19 -12 -21 -10 -4 -10 -6 0 -6 7 -1 12 -16 12 +-41 0 -22 3 -40 8 -40 8 0 6 109 -2 118 -3 3 -6 -2 -6 -10z"/> +<path d="M3866 2044 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M3587 2024 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3727 2024 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3981 2016 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M4067 2024 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -30 0 -17 6 -20 45 -19 41 0 45 3 45 26 0 14 7 33 16 +43 15 17 15 18 -5 16 -17 -1 -21 -8 -22 -37 l-2 -35 -6 35 c-5 28 -11 36 -31 +38 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M426 1574 c-19 -18 -21 -75 -4 -92 17 -17 54 -15 73 4 22 22 10 31 +-13 10 -22 -19 -49 -12 -57 15 -15 46 24 82 56 53 17 -15 19 -15 19 -2 0 29 +-49 37 -74 12z"/> +<path d="M680 1572 c0 -13 -8 -18 -27 -17 -26 0 -28 -3 -28 -40 0 -38 1 -40 +33 -41 l32 -1 0 59 c0 32 -2 58 -5 58 -3 0 -5 -8 -5 -18z m-11 -74 c-6 -11 +-16 -17 -22 -15 -17 5 -21 36 -6 53 12 14 14 14 26 -1 9 -13 9 -23 2 -37z"/> +<path d="M856 1574 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M530 1546 c-28 -35 11 -93 48 -70 35 22 22 84 -18 84 -10 0 -23 -7 +-30 -14z m54 -21 c2 -7 -1 -21 -9 -31 -11 -15 -15 -16 -29 -5 -19 16 -20 33 +-5 48 13 13 35 7 43 -12z"/> +<path d="M721 1546 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 15 +5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 -16 +16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 14 +15 15 15 1 0 8 -7 15 -15z"/> +<path d="M971 1546 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 15 +5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 -16 +16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 14 +15 15 15 1 0 8 -7 15 -15z"/> +<path d="M1057 1554 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -30 0 -17 6 -20 45 -19 41 0 45 3 45 26 0 14 7 33 16 +43 15 17 15 18 -5 16 -17 -1 -21 -8 -22 -37 l-2 -35 -6 35 c-5 28 -11 36 -31 +38 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M1902 1528 c2 -62 2 -62 6 -13 l4 50 17 -45 c9 -25 21 -44 26 -42 6 +1 17 21 25 45 l15 42 6 -50 6 -50 1 63 c1 34 -2 62 -7 62 -5 0 -17 -20 -27 +-45 -19 -50 -26 -49 -44 8 -18 56 -30 45 -28 -25z"/> +<path d="M2130 1578 c0 -9 -6 -19 -12 -21 -10 -4 -10 -6 0 -6 7 -1 12 -16 12 +-41 0 -22 3 -40 8 -40 8 0 6 109 -2 118 -3 3 -6 -2 -6 -10z"/> +<path d="M2306 1574 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M2041 1546 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M2167 1554 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M2421 1546 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M2507 1554 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M2591 1510 c2 -34 3 -37 6 -15 3 17 12 38 20 47 14 15 13 17 -6 15 +-18 -1 -21 -7 -20 -47z"/> +<path d="M5292 1528 c2 -62 2 -62 6 -13 l4 50 17 -45 c9 -25 21 -44 26 -42 6 +1 17 21 25 45 l15 42 6 -50 6 -50 1 63 c1 34 -2 62 -7 62 -5 0 -17 -20 -27 +-45 -19 -50 -26 -49 -44 8 -18 56 -30 45 -28 -25z"/> +<path d="M5530 1578 c0 -9 -6 -19 -12 -21 -10 -4 -10 -6 0 -6 7 -1 12 -16 12 +-41 0 -22 3 -40 8 -40 8 0 6 109 -2 118 -3 3 -6 -2 -6 -10z"/> +<path d="M5706 1574 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M5431 1546 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M5567 1554 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M5821 1546 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M5897 1554 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M5981 1510 c2 -34 3 -37 6 -15 3 17 12 38 20 47 14 15 13 17 -6 15 +-18 -1 -21 -7 -20 -47z"/> +<path d="M6826 1574 c-19 -18 -21 -75 -4 -92 17 -17 54 -15 73 4 22 22 10 31 +-13 10 -22 -19 -49 -12 -57 15 -15 46 24 82 56 53 17 -15 19 -15 19 -2 0 29 +-49 37 -74 12z"/> +<path d="M7080 1572 c0 -13 -8 -18 -27 -17 -26 0 -28 -3 -28 -40 0 -38 1 -40 +33 -41 l32 -1 0 59 c0 32 -2 58 -5 58 -3 0 -5 -8 -5 -18z m-11 -74 c-6 -11 +-16 -17 -22 -15 -17 5 -21 36 -6 53 12 14 14 14 26 -1 9 -13 9 -23 2 -37z"/> +<path d="M7256 1574 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M6930 1546 c-28 -35 11 -93 48 -70 35 22 22 84 -18 84 -10 0 -23 -7 +-30 -14z m54 -21 c2 -7 -1 -21 -9 -31 -11 -15 -15 -16 -29 -5 -19 16 -20 33 +-5 48 13 13 35 7 43 -12z"/> +<path d="M7121 1546 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M7371 1546 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M7457 1554 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -30 0 -17 6 -20 45 -19 41 0 45 3 45 26 0 14 7 33 16 +43 15 17 15 18 -5 16 -17 -1 -21 -8 -22 -37 l-2 -35 -6 35 c-5 28 -11 36 -31 +38 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3480 1080 c0 -60 0 -60 29 -60 37 0 61 23 61 60 0 37 -24 60 -61 60 +-29 0 -29 0 -29 -60z m69 34 c10 -10 3 -67 -10 -75 -36 -22 -49 -11 -49 42 0 +51 0 51 27 44 16 -4 30 -9 32 -11z"/> +<path d="M3690 1128 c0 -9 -6 -19 -12 -21 -10 -4 -10 -6 0 -6 7 -1 12 -16 12 +-41 0 -22 3 -40 8 -40 8 0 6 109 -2 118 -3 3 -6 -2 -6 -10z"/> +<path d="M3866 1124 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M3587 1104 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3727 1104 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3981 1096 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 +15 5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 +-16 16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 +14 15 15 15 1 0 8 -7 15 -15z"/> +<path d="M4067 1104 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -30 0 -17 6 -20 45 -19 41 0 45 3 45 26 0 14 7 33 16 +43 15 17 15 18 -5 16 -17 -1 -21 -8 -22 -37 l-2 -35 -6 35 c-5 28 -11 36 -31 +38 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3472 268 c2 -62 2 -62 6 -13 l4 50 17 -45 c9 -25 21 -44 26 -42 6 1 +17 21 25 45 l15 42 6 -50 6 -50 1 63 c1 34 -2 62 -7 62 -5 0 -17 -20 -27 -45 +-19 -50 -26 -49 -44 8 -18 56 -30 45 -28 -25z"/> +<path d="M3700 318 c0 -9 -6 -19 -12 -21 -10 -4 -10 -6 0 -6 7 -1 12 -16 12 +-41 0 -22 3 -40 8 -40 8 0 6 109 -2 118 -3 3 -6 -2 -6 -10z"/> +<path d="M3876 314 c-9 -8 -16 -31 -16 -49 0 -40 22 -57 70 -53 27 2 30 6 30 +35 0 30 -3 33 -27 32 -17 -1 -21 -3 -10 -6 21 -5 23 -39 2 -47 -34 -13 -63 23 +-50 63 8 27 34 34 61 16 25 -16 33 -8 12 13 -17 17 -54 15 -72 -4z"/> +<path d="M3611 286 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 15 +5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 -16 +16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 14 +15 15 15 1 0 8 -7 15 -15z"/> +<path d="M3737 294 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M3991 286 c-7 -8 -11 -27 -9 -43 2 -24 8 -28 32 -28 17 0 31 6 34 15 +5 13 3 13 -11 1 -18 -14 -47 -9 -47 9 0 5 14 10 30 10 31 0 39 17 18 38 -16 +16 -33 15 -47 -2z m39 -11 c11 -13 8 -15 -15 -15 -23 0 -26 2 -15 15 7 8 14 +15 15 15 1 0 8 -7 15 -15z"/> +<path d="M4077 294 c-14 -14 -7 -26 8 -14 12 10 19 10 27 2 8 -8 4 -14 -15 +-21 -17 -7 -27 -18 -27 -31 0 -17 6 -20 38 -18 l38 1 -6 41 c-4 35 -9 41 -30 +44 -14 2 -29 0 -33 -4z m41 -60 c-9 -9 -21 -13 -27 -9 -16 10 -3 25 22 25 20 +0 20 -1 5 -16z"/> +<path d="M4161 250 c2 -34 3 -37 6 -15 3 17 12 38 20 47 14 15 13 17 -6 15 +-18 -1 -21 -7 -20 -47z"/> +</g> +</svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/model_checking.svg Sat Apr 15 11:39:08 2023 +0900 @@ -0,0 +1,421 @@ +<?xml version="1.0" encoding="UTF-8"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg version="1.2" width="210mm" height="297mm" viewBox="0 0 21000 29700" preserveAspectRatio="xMidYMid" fill-rule="evenodd" stroke-width="28.222" stroke-linejoin="round" xmlns="http://www.w3.org/2000/svg" xmlns:ooo="http://xml.openoffice.org/svg/export" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:presentation="http://sun.com/xmlns/staroffice/presentation" xmlns:smil="http://www.w3.org/2001/SMIL20/" xmlns:anim="urn:oasis:names:tc:opendocument:xmlns:animation:1.0" xml:space="preserve"> + <defs class="ClipPathGroup"> + <clipPath id="presentation_clip_path" clipPathUnits="userSpaceOnUse"> + <rect x="0" y="0" width="21000" height="29700"/> + </clipPath> + <clipPath id="presentation_clip_path_shrink" clipPathUnits="userSpaceOnUse"> + <rect x="21" y="29" width="20958" height="29641"/> + </clipPath> + </defs> + <defs> + <font id="EmbeddedFont_1" horiz-adv-x="2048"> + <font-face font-family="Liberation Sans embedded" units-per-em="2048" font-weight="normal" font-style="normal" ascent="1870" descent="439"/> + <missing-glyph horiz-adv-x="2048" d="M 0,0 L 2047,0 2047,2047 0,2047 0,0 Z"/> + <glyph unicode="●" horiz-adv-x="901" d="M 618,1018 C 691,1018 764,999 837,960 909,921 964,866 1002,793 1040,720 1059,649 1059,578 1059,456 1016,352 930,266 844,180 740,137 618,137 497,137 393,180 307,267 221,353 178,457 178,578 178,650 197,722 234,793 271,864 325,919 397,959 468,998 542,1018 618,1018 Z"/> + <glyph unicode="z" horiz-adv-x="856" d="M 83,0 L 83,137 688,943 117,943 117,1082 901,1082 901,945 295,139 922,139 922,0 Z"/> + <glyph unicode="y" horiz-adv-x="1040" d="M 191,-425 C 142,-425 100,-421 67,-414 L 67,-279 C 92,-283 120,-285 151,-285 263,-285 352,-203 417,-38 L 434,5 5,1082 197,1082 425,484 C 428,475 432,464 437,451 442,438 457,394 482,320 507,246 521,205 523,196 L 593,393 830,1082 1020,1082 604,0 C 559,-115 518,-201 479,-258 440,-314 398,-356 351,-384 304,-411 250,-425 191,-425 Z"/> + <glyph unicode="u" horiz-adv-x="902" d="M 314,1082 L 314,396 C 314,325 321,269 335,230 349,191 371,162 402,145 433,128 478,119 537,119 624,119 692,149 742,208 792,267 817,350 817,455 L 817,1082 997,1082 997,231 C 997,105 999,28 1003,0 L 833,0 C 832,3 832,12 831,27 830,42 830,59 829,78 828,97 826,132 825,185 L 822,185 C 781,110 733,58 679,27 624,-5 557,-20 476,-20 357,-20 271,10 216,69 161,128 133,225 133,361 L 133,1082 Z"/> + <glyph unicode="t" horiz-adv-x="532" d="M 554,8 C 495,-8 434,-16 372,-16 228,-16 156,66 156,229 L 156,951 31,951 31,1082 163,1082 216,1324 336,1324 336,1082 536,1082 536,951 336,951 336,268 C 336,216 345,180 362,159 379,138 408,127 450,127 474,127 509,132 554,141 Z"/> + <glyph unicode="s" horiz-adv-x="925" d="M 950,299 C 950,197 912,118 835,63 758,8 650,-20 511,-20 376,-20 273,2 200,47 127,91 79,160 57,254 L 216,285 C 231,227 263,185 311,158 359,131 426,117 511,117 602,117 669,131 712,159 754,187 775,229 775,285 775,328 760,362 731,389 702,416 654,438 589,455 L 460,489 C 357,516 283,542 240,568 196,593 162,624 137,661 112,698 100,743 100,796 100,895 135,970 206,1022 276,1073 378,1099 513,1099 632,1099 727,1078 798,1036 868,994 912,927 931,834 L 769,814 C 759,862 732,899 689,925 645,950 586,963 513,963 432,963 372,951 333,926 294,901 275,864 275,814 275,783 283,758 299,738 315,718 339,701 370,687 401,673 467,654 568,629 663,605 732,583 774,563 816,542 849,520 874,495 898,470 917,442 930,410 943,377 950,340 950,299 Z"/> + <glyph unicode="r" horiz-adv-x="556" d="M 142,0 L 142,830 C 142,906 140,990 136,1082 L 306,1082 C 311,959 314,886 314,861 L 318,861 C 347,954 380,1017 417,1051 454,1085 507,1102 575,1102 599,1102 623,1099 648,1092 L 648,927 C 624,934 592,937 552,937 477,937 420,905 381,841 342,776 322,684 322,564 L 322,0 Z"/> + <glyph unicode="p" horiz-adv-x="948" d="M 1053,546 C 1053,169 920,-20 655,-20 488,-20 376,43 319,168 L 314,168 C 317,163 318,106 318,-2 L 318,-425 138,-425 138,861 C 138,972 136,1046 132,1082 L 306,1082 C 307,1079 308,1070 309,1054 310,1037 312,1012 314,978 315,944 316,921 316,908 L 320,908 C 352,975 394,1024 447,1055 500,1086 569,1101 655,1101 788,1101 888,1056 954,967 1020,878 1053,737 1053,546 Z M 864,542 C 864,693 844,800 803,865 762,930 698,962 609,962 538,962 482,947 442,917 401,887 371,840 350,777 329,713 318,630 318,528 318,386 341,281 386,214 431,147 505,113 607,113 696,113 762,146 803,212 844,277 864,387 864,542 Z"/> + <glyph unicode="o" horiz-adv-x="994" d="M 1053,542 C 1053,353 1011,212 928,119 845,26 724,-20 565,-20 407,-20 288,28 207,125 126,221 86,360 86,542 86,915 248,1102 571,1102 736,1102 858,1057 936,966 1014,875 1053,733 1053,542 Z M 864,542 C 864,691 842,800 798,868 753,935 679,969 574,969 469,969 393,935 346,866 299,797 275,689 275,542 275,399 298,292 345,221 391,149 464,113 563,113 671,113 748,148 795,217 841,286 864,395 864,542 Z"/> + <glyph unicode="n" horiz-adv-x="902" d="M 825,0 L 825,686 C 825,757 818,813 804,852 790,891 768,920 737,937 706,954 661,963 602,963 515,963 447,933 397,874 347,815 322,732 322,627 L 322,0 142,0 142,851 C 142,977 140,1054 136,1082 L 306,1082 C 307,1079 307,1070 308,1055 309,1040 310,1024 311,1005 312,986 313,950 314,897 L 317,897 C 358,972 406,1025 461,1056 515,1087 582,1102 663,1102 782,1102 869,1073 924,1014 979,955 1006,857 1006,721 L 1006,0 Z"/> + <glyph unicode="m" horiz-adv-x="1479" d="M 768,0 L 768,686 C 768,791 754,863 725,903 696,943 645,963 570,963 493,963 433,934 388,875 343,816 321,734 321,627 L 321,0 142,0 142,851 C 142,977 140,1054 136,1082 L 306,1082 C 307,1079 307,1070 308,1055 309,1040 310,1024 311,1005 312,986 313,950 314,897 L 317,897 C 356,974 400,1027 450,1057 500,1087 561,1102 633,1102 715,1102 780,1086 828,1053 875,1020 908,968 927,897 L 930,897 C 967,970 1013,1022 1066,1054 1119,1086 1183,1102 1258,1102 1367,1102 1447,1072 1497,1013 1546,954 1571,856 1571,721 L 1571,0 1393,0 1393,686 C 1393,791 1379,863 1350,903 1321,943 1270,963 1195,963 1116,963 1055,934 1012,876 968,817 946,734 946,627 L 946,0 Z"/> + <glyph unicode="l" horiz-adv-x="209" d="M 138,0 L 138,1484 318,1484 318,0 Z"/> + <glyph unicode="k" horiz-adv-x="925" d="M 816,0 L 450,494 318,385 318,0 138,0 138,1484 318,1484 318,557 793,1082 1004,1082 565,617 1027,0 Z"/> + <glyph unicode="i" horiz-adv-x="209" d="M 137,1312 L 137,1484 317,1484 317,1312 Z M 137,0 L 137,1082 317,1082 317,0 Z"/> + <glyph unicode="h" horiz-adv-x="878" d="M 317,897 C 356,968 402,1020 457,1053 511,1086 580,1102 663,1102 780,1102 867,1073 923,1015 978,956 1006,858 1006,721 L 1006,0 825,0 825,686 C 825,762 818,819 804,856 790,893 767,920 735,937 703,954 659,963 602,963 517,963 450,934 399,875 348,816 322,737 322,638 L 322,0 142,0 142,1484 322,1484 322,1098 C 322,1057 321,1015 319,972 316,929 315,904 314,897 Z"/> + <glyph unicode="g" horiz-adv-x="948" d="M 548,-425 C 430,-425 336,-402 266,-356 196,-309 151,-243 131,-158 L 312,-132 C 324,-182 351,-221 392,-248 433,-275 486,-288 553,-288 732,-288 822,-183 822,27 L 822,201 820,201 C 786,132 739,80 680,45 621,10 551,-8 472,-8 339,-8 242,36 180,124 117,212 86,350 86,539 86,730 120,872 187,963 254,1054 355,1099 492,1099 569,1099 635,1082 692,1047 748,1012 791,962 822,897 L 824,897 C 824,917 825,952 828,1001 831,1050 833,1077 836,1082 L 1007,1082 C 1003,1046 1001,971 1001,858 L 1001,31 C 1001,-273 850,-425 548,-425 Z M 822,541 C 822,629 810,705 786,769 762,832 728,881 685,915 641,948 591,965 536,965 444,965 377,932 335,865 293,798 272,690 272,541 272,393 292,287 331,222 370,157 438,125 533,125 590,125 640,142 684,175 728,208 762,256 786,319 810,381 822,455 822,541 Z"/> + <glyph unicode="f" horiz-adv-x="555" d="M 361,951 L 361,0 181,0 181,951 29,951 29,1082 181,1082 181,1204 C 181,1303 203,1374 246,1417 289,1460 356,1482 445,1482 495,1482 537,1478 572,1470 L 572,1333 C 542,1338 515,1341 492,1341 446,1341 413,1329 392,1306 371,1283 361,1240 361,1179 L 361,1082 572,1082 572,951 Z"/> + <glyph unicode="e" horiz-adv-x="994" d="M 276,503 C 276,379 302,283 353,216 404,149 479,115 578,115 656,115 719,131 766,162 813,193 844,233 861,281 L 1019,236 C 954,65 807,-20 578,-20 418,-20 296,28 213,123 129,218 87,360 87,548 87,727 129,864 213,959 296,1054 416,1102 571,1102 889,1102 1048,910 1048,527 L 1048,503 Z M 862,641 C 852,755 823,838 775,891 727,943 658,969 568,969 481,969 412,940 361,882 310,823 282,743 278,641 Z"/> + <glyph unicode="d" horiz-adv-x="948" d="M 821,174 C 788,105 744,55 689,25 634,-5 565,-20 484,-20 347,-20 247,26 183,118 118,210 86,349 86,536 86,913 219,1102 484,1102 566,1102 634,1087 689,1057 744,1027 788,979 821,914 L 823,914 821,1035 821,1484 1001,1484 1001,223 C 1001,110 1003,36 1007,0 L 835,0 C 833,11 831,35 829,74 826,113 825,146 825,174 Z M 275,542 C 275,391 295,282 335,217 375,152 440,119 530,119 632,119 706,154 752,225 798,296 821,405 821,554 821,697 798,802 752,869 706,936 633,969 532,969 441,969 376,936 336,869 295,802 275,693 275,542 Z"/> + <glyph unicode="c" horiz-adv-x="925" d="M 275,546 C 275,402 298,295 343,226 388,157 457,122 548,122 612,122 666,139 709,174 752,209 778,262 788,334 L 970,322 C 956,218 912,135 837,73 762,11 668,-20 553,-20 402,-20 286,28 207,124 127,219 87,359 87,542 87,724 127,863 207,959 287,1054 402,1102 551,1102 662,1102 754,1073 827,1016 900,959 945,880 964,779 L 779,765 C 770,825 746,873 708,908 670,943 616,961 546,961 451,961 382,929 339,866 296,803 275,696 275,546 Z"/> + <glyph unicode="a" horiz-adv-x="1087" d="M 414,-20 C 305,-20 224,9 169,66 114,123 87,202 87,302 87,414 124,500 198,560 271,620 390,652 554,656 L 797,660 797,719 C 797,807 778,870 741,908 704,946 645,965 565,965 484,965 426,951 389,924 352,897 330,853 323,793 L 135,810 C 166,1005 310,1102 569,1102 705,1102 807,1071 876,1009 945,946 979,856 979,738 L 979,272 C 979,219 986,179 1000,152 1014,125 1041,111 1080,111 1097,111 1117,113 1139,118 L 1139,6 C 1094,-5 1047,-10 1000,-10 933,-10 885,8 855,43 824,78 807,132 803,207 L 797,207 C 751,124 698,66 637,32 576,-3 501,-20 414,-20 Z M 455,115 C 521,115 580,130 631,160 682,190 723,231 753,284 782,336 797,390 797,445 L 797,534 600,530 C 515,529 451,520 408,504 364,488 330,463 307,430 284,397 272,353 272,299 272,240 288,195 320,163 351,131 396,115 455,115 Z"/> + <glyph unicode="T" horiz-adv-x="1202" d="M 720,1253 L 720,0 530,0 530,1253 46,1253 46,1409 1204,1409 1204,1253 Z"/> + <glyph unicode="S" horiz-adv-x="1202" d="M 1272,389 C 1272,259 1221,158 1120,87 1018,16 875,-20 690,-20 347,-20 148,99 93,338 L 278,375 C 299,290 345,228 414,189 483,149 578,129 697,129 820,129 916,150 983,193 1050,235 1083,297 1083,379 1083,425 1073,462 1052,491 1031,520 1001,543 963,562 925,581 880,596 827,609 774,622 716,635 652,650 541,675 456,699 399,724 341,749 295,776 262,807 229,837 203,872 186,913 168,954 159,1000 159,1053 159,1174 205,1267 298,1332 390,1397 522,1430 694,1430 854,1430 976,1406 1061,1357 1146,1308 1205,1224 1239,1106 L 1051,1073 C 1030,1148 991,1202 933,1236 875,1269 795,1286 692,1286 579,1286 493,1267 434,1230 375,1193 345,1137 345,1063 345,1020 357,984 380,956 403,927 436,903 479,884 522,864 609,840 738,811 781,801 825,791 868,781 911,770 952,758 991,744 1030,729 1067,712 1102,693 1136,674 1166,650 1191,622 1216,594 1236,561 1251,523 1265,485 1272,440 1272,389 Z"/> + <glyph unicode="R" horiz-adv-x="1224" d="M 1164,0 L 798,585 359,585 359,0 168,0 168,1409 831,1409 C 990,1409 1112,1374 1199,1303 1285,1232 1328,1133 1328,1006 1328,901 1298,813 1237,742 1176,671 1091,626 984,607 L 1384,0 Z M 1136,1004 C 1136,1086 1108,1149 1053,1192 997,1235 917,1256 812,1256 L 359,1256 359,736 820,736 C 921,736 999,760 1054,807 1109,854 1136,919 1136,1004 Z"/> + <glyph unicode="Q" horiz-adv-x="1410" d="M 1495,711 C 1495,512 1445,349 1345,221 1245,93 1106,17 928,-6 955,-90 991,-151 1036,-188 1080,-225 1136,-244 1204,-244 1241,-244 1279,-240 1319,-231 L 1319,-365 C 1257,-380 1198,-387 1141,-387 1040,-387 958,-359 893,-302 828,-245 774,-149 733,-16 601,-9 487,24 392,85 296,145 223,229 173,337 122,444 97,569 97,711 97,936 159,1113 282,1240 405,1367 577,1430 797,1430 940,1430 1065,1402 1170,1345 1275,1288 1356,1205 1412,1096 1467,987 1495,859 1495,711 Z M 1300,711 C 1300,886 1256,1024 1169,1124 1081,1224 957,1274 797,1274 636,1274 511,1225 423,1126 335,1027 291,889 291,711 291,534 336,394 425,291 514,187 637,135 795,135 958,135 1083,185 1170,286 1257,386 1300,528 1300,711 Z"/> + <glyph unicode="P" horiz-adv-x="1109" d="M 1258,985 C 1258,852 1215,746 1128,667 1041,588 922,549 773,549 L 359,549 359,0 168,0 168,1409 761,1409 C 919,1409 1041,1372 1128,1298 1215,1224 1258,1120 1258,985 Z M 1066,983 C 1066,1165 957,1256 738,1256 L 359,1256 359,700 746,700 C 959,700 1066,794 1066,983 Z"/> + <glyph unicode="M" horiz-adv-x="1386" d="M 1366,0 L 1366,940 C 1366,1044 1369,1144 1375,1240 1342,1121 1313,1027 1287,960 L 923,0 789,0 420,960 364,1130 331,1240 334,1129 338,940 338,0 168,0 168,1409 419,1409 794,432 C 807,393 820,351 833,306 845,261 853,228 857,208 862,235 874,275 891,330 908,384 919,418 925,432 L 1293,1409 1538,1409 1538,0 Z"/> + <glyph unicode="L" horiz-adv-x="924" d="M 168,0 L 168,1409 359,1409 359,156 1071,156 1071,0 Z"/> + <glyph unicode="G" horiz-adv-x="1364" d="M 103,711 C 103,940 164,1117 287,1242 410,1367 582,1430 804,1430 960,1430 1087,1404 1184,1351 1281,1298 1356,1214 1409,1098 L 1227,1044 C 1187,1124 1132,1182 1062,1219 991,1256 904,1274 799,1274 636,1274 512,1225 426,1127 340,1028 297,890 297,711 297,533 343,393 434,290 525,187 652,135 813,135 905,135 991,149 1071,177 1150,205 1215,243 1264,291 L 1264,545 843,545 843,705 1440,705 1440,219 C 1365,143 1274,84 1166,43 1057,1 940,-20 813,-20 666,-20 539,9 432,68 325,127 244,211 188,322 131,432 103,562 103,711 Z"/> + <glyph unicode="E" horiz-adv-x="1132" d="M 168,0 L 168,1409 1237,1409 1237,1253 359,1253 359,801 1177,801 1177,647 359,647 359,156 1278,156 1278,0 Z"/> + <glyph unicode="D" horiz-adv-x="1224" d="M 1381,719 C 1381,574 1353,447 1296,338 1239,229 1159,145 1055,87 951,29 831,0 695,0 L 168,0 168,1409 634,1409 C 873,1409 1057,1349 1187,1230 1316,1110 1381,940 1381,719 Z M 1189,719 C 1189,894 1141,1027 1046,1119 950,1210 811,1256 630,1256 L 359,1256 359,153 673,153 C 776,153 867,176 946,221 1024,266 1084,332 1126,417 1168,502 1189,603 1189,719 Z"/> + <glyph unicode="C" horiz-adv-x="1318" d="M 792,1274 C 636,1274 515,1224 428,1124 341,1023 298,886 298,711 298,538 343,400 434,295 524,190 646,137 800,137 997,137 1146,235 1245,430 L 1401,352 C 1343,231 1262,138 1157,75 1052,12 930,-20 791,-20 649,-20 526,10 423,69 319,128 240,212 186,322 131,431 104,561 104,711 104,936 165,1112 286,1239 407,1366 575,1430 790,1430 940,1430 1065,1401 1166,1342 1267,1283 1341,1196 1388,1081 L 1207,1021 C 1174,1103 1122,1166 1050,1209 977,1252 891,1274 792,1274 Z"/> + <glyph unicode="B" horiz-adv-x="1109" d="M 1258,397 C 1258,272 1212,174 1121,105 1030,35 903,0 740,0 L 168,0 168,1409 680,1409 C 1011,1409 1176,1295 1176,1067 1176,984 1153,914 1106,857 1059,800 993,762 908,743 1020,730 1106,692 1167,631 1228,569 1258,491 1258,397 Z M 984,1044 C 984,1120 958,1174 906,1207 854,1240 779,1256 680,1256 L 359,1256 359,810 680,810 C 782,810 858,829 909,868 959,906 984,965 984,1044 Z M 1065,412 C 1065,578 948,661 715,661 L 359,661 359,153 730,153 C 847,153 932,175 985,218 1038,261 1065,326 1065,412 Z"/> + <glyph unicode="5" horiz-adv-x="994" d="M 1053,459 C 1053,310 1009,193 921,108 832,23 710,-20 553,-20 422,-20 316,9 235,66 154,123 103,206 82,315 L 264,336 C 302,197 400,127 557,127 654,127 729,156 784,215 839,273 866,353 866,455 866,544 839,615 784,670 729,725 654,752 561,752 512,752 467,744 425,729 383,714 341,688 299,651 L 123,651 170,1409 971,1409 971,1256 334,1256 307,809 C 385,869 482,899 598,899 737,899 847,858 930,777 1012,696 1053,590 1053,459 Z"/> + <glyph unicode="4" horiz-adv-x="1040" d="M 881,319 L 881,0 711,0 711,319 47,319 47,459 692,1409 881,1409 881,461 1079,461 1079,319 Z M 711,1206 C 710,1202 700,1184 683,1153 666,1122 653,1100 644,1087 L 283,555 229,481 213,461 711,461 Z"/> + <glyph unicode="3" horiz-adv-x="994" d="M 1049,389 C 1049,259 1008,158 925,87 842,16 724,-20 571,-20 428,-20 315,12 230,77 145,141 94,236 78,362 L 264,379 C 288,212 390,129 571,129 662,129 733,151 785,196 836,241 862,307 862,395 862,472 833,532 774,575 715,618 629,639 518,639 L 416,639 416,795 514,795 C 613,795 689,817 744,860 798,903 825,962 825,1038 825,1113 803,1173 759,1217 714,1260 648,1282 561,1282 482,1282 418,1262 369,1221 320,1180 291,1123 283,1049 L 102,1063 C 115,1178 163,1268 246,1333 328,1398 434,1430 563,1430 704,1430 814,1397 893,1332 971,1266 1010,1174 1010,1057 1010,967 985,894 935,838 884,781 811,743 715,723 L 715,719 C 820,708 902,672 961,613 1020,554 1049,479 1049,389 Z"/> + <glyph unicode="2" horiz-adv-x="948" d="M 103,0 L 103,127 C 137,205 179,274 228,334 277,393 328,447 382,496 436,544 490,589 543,630 596,671 643,713 686,754 729,795 763,839 790,884 816,929 829,981 829,1038 829,1115 806,1175 761,1218 716,1261 653,1282 572,1282 495,1282 432,1261 383,1220 333,1178 304,1119 295,1044 L 111,1061 C 124,1174 172,1263 255,1330 337,1397 443,1430 572,1430 714,1430 823,1397 900,1330 976,1263 1014,1167 1014,1044 1014,989 1002,935 977,881 952,827 914,773 865,719 816,665 721,581 582,468 505,405 444,349 399,299 354,248 321,200 301,153 L 1036,153 1036,0 Z"/> + <glyph unicode="." horiz-adv-x="209" d="M 187,0 L 187,219 382,219 382,0 Z"/> + <glyph unicode=" " horiz-adv-x="577"/> + </font> + </defs> + <defs> + <font id="EmbeddedFont_2" horiz-adv-x="2048"> + <font-face font-family="ＭＳ Ｐゴシック embedded" units-per-em="2048" font-weight="normal" font-style="normal" ascent="1755" descent="300"/> + <missing-glyph horiz-adv-x="2048" d="M 0,0 L 2047,0 2047,2047 0,2047 0,0 Z"/> + <glyph unicode="１" horiz-adv-x="601" d="M 872,1408 L 872,24 688,24 688,1088 288,1088 288,1216 C 523,1211 675,1275 744,1408 Z"/> + <glyph unicode=" " horiz-adv-x="1"/> + </font> + </defs> + <defs class="TextShapeIndex"> + <g ooo:slide="id1" ooo:id-list="id3 id4 id5 id6 id7 id8 id9 id10 id11 id12 id13 id14 id15 id16 id17 id18 id19 id20 id21 id22 id23 id24 id25 id26 id27 id28 id29 id30 id31 id32 id33 id34 id35 id36 id37 id38 id39 id40 id41 id42 id43 id44 id45 id46 id47"/> + </defs> + <defs class="EmbeddedBulletChars"> + <g id="bullet-char-template-57356" transform="scale(0.00048828125,-0.00048828125)"> + <path d="M 580,1141 L 1163,571 580,0 -4,571 580,1141 Z"/> + </g> + <g id="bullet-char-template-57354" transform="scale(0.00048828125,-0.00048828125)"> + <path d="M 8,1128 L 1137,1128 1137,0 8,0 8,1128 Z"/> + </g> + <g id="bullet-char-template-10146" transform="scale(0.00048828125,-0.00048828125)"> + <path d="M 174,0 L 602,739 174,1481 1456,739 174,0 Z M 1358,739 L 309,1346 659,739 1358,739 Z"/> + </g> + <g id="bullet-char-template-10132" transform="scale(0.00048828125,-0.00048828125)"> + <path d="M 2015,739 L 1276,0 717,0 1260,543 174,543 174,936 1260,936 717,1481 1274,1481 2015,739 Z"/> + </g> + <g id="bullet-char-template-10007" transform="scale(0.00048828125,-0.00048828125)"> + <path d="M 0,-2 C -7,14 -16,27 -25,37 L 356,567 C 262,823 215,952 215,954 215,979 228,992 255,992 264,992 276,990 289,987 310,991 331,999 354,1012 L 381,999 492,748 772,1049 836,1024 860,1049 C 881,1039 901,1025 922,1006 886,937 835,863 770,784 769,783 710,716 594,584 L 774,223 C 774,196 753,168 711,139 L 727,119 C 717,90 699,76 672,76 641,76 570,178 457,381 L 164,-76 C 142,-110 111,-127 72,-127 30,-127 9,-110 8,-76 1,-67 -2,-52 -2,-32 -2,-23 -1,-13 0,-2 Z"/> + </g> + <g id="bullet-char-template-10004" transform="scale(0.00048828125,-0.00048828125)"> + <path d="M 285,-33 C 182,-33 111,30 74,156 52,228 41,333 41,471 41,549 55,616 82,672 116,743 169,778 240,778 293,778 328,747 346,684 L 369,508 C 377,444 397,411 428,410 L 1163,1116 C 1174,1127 1196,1133 1229,1133 1271,1133 1292,1118 1292,1087 L 1292,965 C 1292,929 1282,901 1262,881 L 442,47 C 390,-6 338,-33 285,-33 Z"/> + </g> + <g id="bullet-char-template-9679" transform="scale(0.00048828125,-0.00048828125)"> + <path d="M 813,0 C 632,0 489,54 383,161 276,268 223,411 223,592 223,773 276,916 383,1023 489,1130 632,1184 813,1184 992,1184 1136,1130 1245,1023 1353,916 1407,772 1407,592 1407,412 1353,268 1245,161 1136,54 992,0 813,0 Z"/> + </g> + <g id="bullet-char-template-8226" transform="scale(0.00048828125,-0.00048828125)"> + <path d="M 346,457 C 273,457 209,483 155,535 101,586 74,649 74,723 74,796 101,859 155,911 209,963 273,989 346,989 419,989 480,963 531,910 582,859 608,796 608,723 608,648 583,586 532,535 482,483 420,457 346,457 Z"/> + </g> + <g id="bullet-char-template-8211" transform="scale(0.00048828125,-0.00048828125)"> + <path d="M -4,459 L 1135,459 1135,606 -4,606 -4,459 Z"/> + </g> + <g id="bullet-char-template-61548" transform="scale(0.00048828125,-0.00048828125)"> + <path d="M 173,740 C 173,903 231,1043 346,1159 462,1274 601,1332 765,1332 928,1332 1067,1274 1183,1159 1299,1043 1357,903 1357,740 1357,577 1299,437 1183,322 1067,206 928,148 765,148 601,148 462,206 346,322 231,437 173,577 173,740 Z"/> + </g> + </defs> + <g> + <g id="id2" class="Master_Slide"> + <g id="bg-id2" class="Background"/> + <g id="bo-id2" class="BackgroundObjects"/> + </g> + </g> + <g class="SlideGroup"> + <g> + <g id="container-id1"> + <g id="id1" class="Slide" clip-path="url(#presentation_clip_path)"> + <g class="Page"> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id3"> + <rect class="BoundingBox" stroke="none" fill="none" x="12999" y="1999" width="6003" height="1003"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 16000,3000 L 13000,3000 13000,2000 19000,2000 19000,3000 16000,3000 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 16000,3000 L 13000,3000 13000,2000 19000,2000 19000,3000 16000,3000 Z"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="14576" y="2721"><tspan fill="rgb(0,0,0)" stroke="none">Scheduler</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id4"> + <rect class="BoundingBox" stroke="none" fill="none" x="13099" y="3999" width="6003" height="1003"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 16100,5000 L 13100,5000 13100,4000 19100,4000 19100,5000 16100,5000 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 16100,5000 L 13100,5000 13100,4000 19100,4000 19100,5000 16100,5000 Z"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="14938" y="4721"><tspan fill="rgb(0,0,0)" stroke="none">par goto</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id5"> + <rect class="BoundingBox" stroke="none" fill="none" x="15950" y="2999" width="301" height="1002"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 16000,3000 L 16000,3500 16100,3500 16100,3570"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 16100,4000 L 16250,3550 15950,3550 16100,4000 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id6"> + <rect class="BoundingBox" stroke="none" fill="none" x="11599" y="7030" width="8003" height="9803"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 15600,16831 L 11600,16831 11600,7031 19600,7031 19600,16831 15600,16831 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 15600,16831 L 11600,16831 11600,7031 19600,7031 19600,16831 15600,16831 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id7"> + <rect class="BoundingBox" stroke="none" fill="none" x="10999" y="7999" width="8003" height="9703"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 15000,17700 L 11000,17700 11000,8000 19000,8000 19000,17700 15000,17700 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 15000,17700 L 11000,17700 11000,8000 19000,8000 19000,17700 15000,17700 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id8"> + <rect class="BoundingBox" stroke="none" fill="none" x="10499" y="8999" width="8003" height="9903"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 14500,18900 L 10500,18900 10500,9000 18500,9000 18500,18900 14500,18900 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 14500,18900 L 10500,18900 10500,9000 18500,9000 18500,18900 14500,18900 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id9"> + <rect class="BoundingBox" stroke="none" fill="none" x="9899" y="9999" width="8003" height="10003"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 13900,20000 L 9900,20000 9900,10000 17900,10000 17900,20000 13900,20000 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 13900,20000 L 9900,20000 9900,10000 17900,10000 17900,20000 13900,20000 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id10"> + <rect class="BoundingBox" stroke="none" fill="none" x="15561" y="4999" width="541" height="2033"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 16100,5000 L 15703,6613"/> + <path fill="rgb(0,0,0)" stroke="none" d="M 15600,7031 L 15853,6630 15562,6558 15600,7031 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id11"> + <rect class="BoundingBox" stroke="none" fill="none" x="15000" y="4999" width="1102" height="3002"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 16100,5000 L 15148,7596"/> + <path fill="rgb(0,0,0)" stroke="none" d="M 15000,8000 L 15296,7629 15014,7526 15000,8000 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id12"> + <rect class="BoundingBox" stroke="none" fill="none" x="14500" y="4999" width="1602" height="4002"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 16100,5000 L 14660,8601"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 14500,9000 L 14806,8638 14528,8526 14500,9000 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id13"> + <rect class="BoundingBox" stroke="none" fill="none" x="13900" y="4999" width="2202" height="5002"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 16100,5000 L 14073,9606"/> + <path fill="rgb(0,0,0)" stroke="none" d="M 13900,10000 L 14219,9649 13944,9528 13900,10000 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id14"> + <rect class="BoundingBox" stroke="none" fill="none" x="9499" y="10999" width="8003" height="10003"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 13500,21000 L 9500,21000 9500,11000 17500,11000 17500,21000 13500,21000 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 13500,21000 L 9500,21000 9500,11000 17500,11000 17500,21000 13500,21000 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id15"> + <rect class="BoundingBox" stroke="none" fill="none" x="13500" y="4999" width="2602" height="6002"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 16100,5000 L 13671,10605"/> + <path fill="rgb(0,0,0)" stroke="none" d="M 13500,11000 L 13817,10647 13541,10527 13500,11000 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id16"> + <rect class="BoundingBox" stroke="none" fill="none" x="17499" y="15999" width="3" height="3"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 17500,16000 L 17500,16000 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id17"> + <rect class="BoundingBox" stroke="none" fill="none" x="17499" y="15999" width="3" height="3"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 17500,16000 L 17500,16000 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id18"> + <rect class="BoundingBox" stroke="none" fill="none" x="11954" y="11977" width="4301" height="1024"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="12204" y="12678"><tspan fill="rgb(0,0,0)" stroke="none">●</tspan><tspan fill="rgb(0,0,0)" stroke="none">Pick Right</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id19"> + <rect class="BoundingBox" stroke="none" fill="none" x="12000" y="14000" width="4301" height="1001"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="12250" y="14701"><tspan fill="rgb(0,0,0)" stroke="none">●</tspan><tspan fill="rgb(0,0,0)" stroke="none">Eat</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id20"> + <rect class="BoundingBox" stroke="none" fill="none" x="12024" y="13015" width="4301" height="1301"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="12274" y="13716"><tspan fill="rgb(0,0,0)" stroke="none">●</tspan><tspan fill="rgb(0,0,0)" stroke="none">Pick Leftt</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id21"> + <rect class="BoundingBox" stroke="none" fill="none" x="11938" y="14938" width="4301" height="1301"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="12188" y="15639"><tspan fill="rgb(0,0,0)" stroke="none">●</tspan><tspan fill="rgb(0,0,0)" stroke="none">Put Right</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id22"> + <rect class="BoundingBox" stroke="none" fill="none" x="12000" y="16000" width="4301" height="1301"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="12250" y="16701"><tspan fill="rgb(0,0,0)" stroke="none">●</tspan><tspan fill="rgb(0,0,0)" stroke="none">Put Left</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id23"> + <rect class="BoundingBox" stroke="none" fill="none" x="12000" y="17000" width="4301" height="1301"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="12250" y="17701"><tspan fill="rgb(0,0,0)" stroke="none">●</tspan><tspan fill="rgb(0,0,0)" stroke="none">Think</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.LineShape"> + <g id="id24"> + <rect class="BoundingBox" stroke="none" fill="none" x="11068" y="11999" width="301" height="2402"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 11218,12000 L 11218,13970"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 11218,14400 L 11368,13950 11068,13950 11218,14400 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id25"> + <rect class="BoundingBox" stroke="none" fill="none" x="14104" y="11540" width="2798" height="7104"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 14150,18300 C 14150,19050 16900,18801 16900,15139 16900,11478 15038,11435 14353,11680"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 14104,11977 L 14515,11740 14291,11541 14104,11977 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id26"> + <rect class="BoundingBox" stroke="none" fill="none" x="7900" y="5900" width="6801" height="1098"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="8150" y="6601"><tspan fill="rgb(0,0,0)" stroke="none">Pherosoher Threads</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id27"> + <rect class="BoundingBox" stroke="none" fill="none" x="10000" y="14300" width="2057" height="1674"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="10250" y="15001"><tspan fill="rgb(0,0,0)" stroke="none">Go to </tspan></tspan><tspan class="TextPosition" x="10250" y="15712"><tspan fill="rgb(0,0,0)" stroke="none">meta</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.LineShape"> + <g id="id28"> + <rect class="BoundingBox" stroke="none" fill="none" x="10950" y="15999" width="301" height="2102"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 11100,16000 L 11100,17670"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 11100,18100 L 11250,17650 10950,17650 11100,18100 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id29"> + <rect class="BoundingBox" stroke="none" fill="none" x="4700" y="6499" width="10852" height="3555"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 15550,6500 L 5109,9916"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 4700,10050 L 5174,10053 5081,9768 4700,10050 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id30"> + <rect class="BoundingBox" stroke="none" fill="none" x="2199" y="4999" width="2503" height="10103"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 3450,15100 L 2200,15100 2200,5000 4700,5000 4700,15100 3450,15100 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 3450,15100 L 2200,15100 2200,5000 4700,5000 4700,15100 3450,15100 Z"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="2703" y="8531"><tspan fill="rgb(0,0,0)" stroke="none">fork</tspan><tspan font-family="ＭＳ Ｐゴシック, sans-serif" fill="rgb(0,0,0)" stroke="none">１</tspan></tspan></tspan><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="2745" y="9242"><tspan fill="rgb(0,0,0)" stroke="none">fork2</tspan></tspan></tspan><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="2745" y="9953"><tspan fill="rgb(0,0,0)" stroke="none">fork3</tspan></tspan></tspan><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="2745" y="10664"><tspan fill="rgb(0,0,0)" stroke="none">fork4</tspan></tspan></tspan><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="2745" y="11375"><tspan fill="rgb(0,0,0)" stroke="none">fork5</tspan></tspan></tspan><tspan class="TextParagraph" font-family="ＭＳ Ｐゴシック, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="3239" y="12056"><tspan fill="rgb(0,0,0)" stroke="none"> </tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id31"> + <rect class="BoundingBox" stroke="none" fill="none" x="884" y="3100" width="6417" height="963"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="1134" y="3801"><tspan fill="rgb(0,0,0)" stroke="none">Syncrhonized Queue</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id32"> + <rect class="BoundingBox" stroke="none" fill="none" x="4700" y="7999" width="10302" height="2112"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 15000,8000 L 5122,9966"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 4700,10050 L 5171,10109 5112,9815 4700,10050 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id33"> + <rect class="BoundingBox" stroke="none" fill="none" x="4700" y="10050" width="7256" height="2440"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 11954,12488 L 5108,10187"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 4700,10050 L 5079,10336 5174,10051 4700,10050 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id34"> + <rect class="BoundingBox" stroke="none" fill="none" x="4700" y="9897" width="9202" height="302"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 13900,10000 L 5130,10048"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 4700,10050 L 5151,10198 5149,9898 4700,10050 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id35"> + <rect class="BoundingBox" stroke="none" fill="none" x="4700" y="8999" width="9802" height="1154"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 14500,9000 L 5128,10004"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 4700,10050 L 5163,10151 5131,9853 4700,10050 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id36"> + <rect class="BoundingBox" stroke="none" fill="none" x="4800" y="7400" width="7401" height="1401"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="5050" y="8101"><tspan fill="rgb(0,0,0)" stroke="none">Cheack and Set</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id37"> + <rect class="BoundingBox" stroke="none" fill="none" x="1599" y="20299" width="6903" height="6803"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 5050,27100 L 1600,27100 1600,20300 8500,20300 8500,27100 5050,27100 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 5050,27100 L 1600,27100 1600,20300 8500,20300 8500,27100 5050,27100 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id38"> + <rect class="BoundingBox" stroke="none" fill="none" x="7078" y="15135" width="2924" height="10266"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 10000,15136 L 7217,24986"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 7100,25400 L 7367,25008 7078,24926 7100,25400 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id39"> + <rect class="BoundingBox" stroke="none" fill="none" x="5049" y="27099" width="3" height="3"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 5050,27100 L 5050,27100 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id40"> + <rect class="BoundingBox" stroke="none" fill="none" x="-10501" y="11699" width="6003" height="2203"/> + <path fill="rgb(114,159,207)" stroke="none" d="M -7500,13900 L -10500,13900 -10500,11700 -4500,11700 -4500,13900 -7500,13900 Z"/> + <path fill="none" stroke="rgb(52,101,164)" d="M -7500,13900 L -10500,13900 -10500,11700 -4500,11700 -4500,13900 -7500,13900 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id41"> + <rect class="BoundingBox" stroke="none" fill="none" x="3699" y="21299" width="4203" height="1603"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 5800,22900 L 3700,22900 3700,21300 7900,21300 7900,22900 5800,22900 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 5800,22900 L 3700,22900 3700,21300 7900,21300 7900,22900 5800,22900 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id42"> + <rect class="BoundingBox" stroke="none" fill="none" x="2999" y="22099" width="4203" height="1603"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 5100,23700 L 3000,23700 3000,22100 7200,22100 7200,23700 5100,23700 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 5100,23700 L 3000,23700 3000,22100 7200,22100 7200,23700 5100,23700 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id43"> + <rect class="BoundingBox" stroke="none" fill="none" x="1799" y="22399" width="4203" height="1603"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 3900,24000 L 1800,24000 1800,22400 6000,22400 6000,24000 3900,24000 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 3900,24000 L 1800,24000 1800,22400 6000,22400 6000,24000 3900,24000 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id44"> + <rect class="BoundingBox" stroke="none" fill="none" x="1799" y="23799" width="4203" height="1603"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 3900,25400 L 1800,25400 1800,23800 6000,23800 6000,25400 3900,25400 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 3900,25400 L 1800,25400 1800,23800 6000,23800 6000,25400 3900,25400 Z"/> + </g> + </g> + <g class="com.sun.star.drawing.CustomShape"> + <g id="id45"> + <rect class="BoundingBox" stroke="none" fill="none" x="2899" y="24599" width="4203" height="1603"/> + <path fill="rgb(255,255,255)" stroke="none" d="M 5000,26200 L 2900,26200 2900,24600 7100,24600 7100,26200 5000,26200 Z"/> + <path fill="none" stroke="rgb(0,0,0)" d="M 5000,26200 L 2900,26200 2900,24600 7100,24600 7100,26200 5000,26200 Z"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="3133" y="25621"><tspan fill="rgb(0,0,0)" stroke="none">Memory Tree</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.TextShape"> + <g id="id46"> + <rect class="BoundingBox" stroke="none" fill="none" x="2700" y="18200" width="4701" height="1674"/> + <text class="TextShape"><tspan class="TextParagraph" font-family="Liberation Sans, sans-serif" font-size="635px" font-weight="400"><tspan class="TextPosition" x="2950" y="18901"><tspan fill="rgb(0,0,0)" stroke="none">State.DB</tspan></tspan></tspan></text> + </g> + </g> + <g class="com.sun.star.drawing.ConnectorShape"> + <g id="id47"> + <rect class="BoundingBox" stroke="none" fill="none" x="7099" y="16000" width="4002" height="9402"/> + <path fill="none" stroke="rgb(52,101,164)" d="M 7100,25400 L 10932,16396"/> + <path fill="rgb(52,101,164)" stroke="none" d="M 11100,16000 L 10786,16355 11062,16473 11100,16000 Z"/> + </g> + </g> + </g> + </g> + </g> + </g> + </g> +</svg> \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/gearsAgda.html Sat Apr 15 11:39:08 2023 +0900 @@ -0,0 +1,319 @@ +<html> +<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=UTF-8"> +<head> +<STYLE type="text/css"> +.main { width:100%; } +.side { top:0px; width:0%; position:fixed; left:80%; display:none} +</STYLE> +<script type="text/javascript"> +function showElement(layer){ + var myLayer = document.getElementById(layer); + var main = document.getElementById('mmm'); + if(myLayer.style.display=="none"){ + myLayer.style.width="20%"; + main.style.width="80%"; + myLayer.style.display="block"; + myLayer.backgroundPosition="top"; + } else { + myLayer.style.width="0%"; + main.style.width="100%"; + myLayer.style.display="none"; + } +} +</script> +<script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script> +<script type="text/javascript" id="MathJax-script" async + src="https://cdn.jsdelivr.net/npm/mathjax/es5/tex-chtml.js"> +</script> +<title>GearsAgda : Meta continuation based Hoare Logic</title> +</head> +<body> +<div class="main" id="mmm"> +<h1>GearsAgda : Meta continuation based Hoare Logic</h1> +<a href="#" left="0px" onclick="javascript:showElement('menu')"> +<span>Menu</span> +</a> + +<p> + +<hr/> +<h2><a name="content000">Continuation based C and GearsAgda</a></h2> +goto 文中心に記述する。LLVM/GCC で実装されている。コンパイラの Basic block に相当する +<p> +C form +<pre> + __code whileLoop(EnvPtr en, __code next(EnvPtr en)) { + if ( 0 >= en->varn ) goto next(en); + else { + en->varn = en->varn - 1; + en->vari = en->vari + 1; + goto whileLoop(en, next); + } + } + +</pre> +Agda は pure fuctional な depedent type language。証明を記述できる。goto 文は、以下の形式で記述する。 +<p> +Agda form +<p> + +<pre> + whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t + whileTest c10 next = next (record {varn = c10 ; vari = 0} ) + {-# 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 + test1 : Env + test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) + +</pre> +TERMINATING は停止性が確認できないことを示している。 +<p> + +<hr/> +<h2><a name="content001">Gears OS</a></h2> +CbC と dataGear で構成する OS。 +<p> + +<pre> + __code putdown_rfork(struct PhilsImpl* phils, __code next(...)) { + struct AtomicT_int* right_fork = phils->Rightfork; + goto right_fork->set(-1, putdown_lfork); + } + +</pre> +をメタ計算で表すと、 +<p> + +<pre> + __code putdown_rforkPhilsImpl_stub(struct Context* context) { + PhilsImpl* phils = (PhilsImpl*)GearImpl(context, Phils, phils); + enum Code next = Gearef(context, Phils)->next; + goto putdown_rforkPhilsImpl(context, phils, next); + } + __code putdown_lforkPhilsImpl(struct Context *context,struct PhilsImpl* phils, enum Code next) { + struct AtomicT_int* left_fork = phils->Leftfork; + Gearef(context, AtomicT_int)->atomicT_int = (union Data*) left_fork; + Gearef(context, AtomicT_int)->newData = -1; + Gearef(context, AtomicT_int)->next = C_thinkingPhilsImpl; + goto mcMeta(context, left_fork->set); + } + +</pre> +となる。メタレベルでは引数は context と次の codeGearの番号だけ。 +<p> +GearsAgda でも、同様の実装ができる。 +<p> +<img src="fig/meta_cg_dg.svg" width="80%" height="600"> + +<p> + +<hr/> +<h2><a name="content002">Gears OSのモデル検査</a></h2> + +<pre> + __ncode mcMeta(struct Context* context, enum Code next) { + context->next = next; // remember next Code Gear + int found = visit_StateDB(out, &mcti->state_db, &out,mcWorker->visit); + if (found) { + while(!(list = takeNextIterator(mcWorker->task_iter))) { + +</pre> +mcMeta で状態を記録し、非決定的な実行を網羅する。 +<p> +<img src="fig/model_checking.svg" width="80%" height="600"> + +<p> + +<hr/> +<h2><a name="content003">GearAgda の Hoare Logic</a></h2> + +<pre> + whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10) + → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) + → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t + +</pre> +このように loop を Segment に切り出す。Pre condtion と Post condition が付いている。これは命題で証明する必要がある。(容易) +<p> + +<pre> + TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) + → (r : Index) → (p : Invraiant r) → t + TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r) + ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) + ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) + +</pre> +減少列を使用して、停止性を保証する接続で停止性を含めて Hoare Logic による証明が可能。 +<p> + +<pre> + whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ + whileTestSpec1 _ _ x = tt + +</pre> +仕様は、継続で入力として受ける。 +<p> + +<pre> + proofGearsTermS : {c10 : ℕ } → ⊤ + proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → + TerminatingLoopS Env (λ env → varn env) + (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) + +</pre> +これは、プログラムが証明を値として渡すので、実際に証明になっている。接続するだけでよい。 +<p> + +<hr/> +<h2><a name="content004">Gears OS による赤黒木のモデル検査</a></h2> +木ではなくループ構造を使う。ノードは子供を iterator で返す。これを前述のモデル検査器で調べる。 +<p> +まだ、やってません。 +<p> +赤黒木は実装済み。 +<p> + +<hr/> +<h2><a name="content005">GearsAgda による赤黒木の証明</a></h2> +まず、Binary Tree +<p> + +<pre> + data bt {n : Level} (A : Set n) : Set n where + leaf : bt A + node : (key : ℕ) → (value : A) → + (left : bt A ) → (right : bt A ) → bt A + bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ + bt-depth leaf = 0 + bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ )) + +</pre> +普通のデータ構造 +<p> + +<pre> + find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A) + → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t + find key leaf st _ exit = exit leaf st + find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁ + find key n st _ exit | tri≈ ¬a b ¬c = exit n st + find key n@(node key₁ v tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st) + find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) + {-# TERMINATING #-} + find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t + find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where + find-loop1 : bt A → List (bt A) → t + find-loop1 tree st = find key tree st find-loop1 exit + insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t + insertTree tree key value exit = find-loop key tree [] $ λ t st → replaceNode key value t $ λ t1 → replace-loop key value t1 st exit + insertTest1 = insertTree leaf 1 1 (λ x → x ) + insertTest2 = insertTree insertTest1 2 1 (λ x → x ) + +</pre> +継続( GearsAgda 形式)を用いた実装。これに Hoare条件をつける。 +<p> + +<pre> + findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) + → treeInvariant tree ∧ stackInvariant key tree tree0 stack + → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → t ) → t + +</pre> +invariant はこんな感じ。 +<p> + +<pre> + data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where + t-leaf : treeInvariant leaf + t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂) + → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₂ value₂ t₃ t₄) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) + data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where + s-nil : stackInvariant key0 leaf leaf [] + s-right : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left : bt A} → {st : List (bt A)} + → key < key0 → stackInvariant key0(node key value left tree ) tree0 (node key value left tree ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value left tree ∷ st ) + s-left : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right : bt A} → {st : List (bt A)} + → key0 < key → stackInvariant key0(node key value tree right ) tree0 (node key value tree right ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value tree right ∷ st ) + data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where + +</pre> +簡単とは言えない。条件をrecord にまとめた方がよい。 +<p> + +<pre> + record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where + field + tree0 : bt A + ti : treeInvariant tree0 + si : stackInvariant key tree tree0 stack + ci : C tree stack -- data continuation + + +</pre> +ci はテストとか記述する部分。データの継続になっている。この部分をあとで追加できる。 +<p> + +<pre> + containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ + containsTree {n} {m} {A} {t} tree tree1 key value P RT = + TerminatingLoopS (bt A ∧ List (bt A) ) + {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p)) + ⟪ tree1 , [] ⟫ {!!} + $ λ p P loop → findPPC key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) + $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where + +</pre> +みたいな感じで証明する。 +<p> + +<pre> + insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ + insertTreeSpec0 _ _ _ = tt + +</pre> +仕様記述は、継続の入力で受ける。 +<p> + +<hr/> +<h2><a name="content006">GearsAgdaのモデル検査</a></h2> +GearsOS と同じように構成することにより、並列実行を simulation できる。モデル検査器そのものを Hoare Logic base で証明、あるいは、展開した(比較的膨大な)部分を全部証明する。あるいは、モデル検査を実行することにより並列分散プログラムを検証できるはず。 +<p> + +<hr/> +<h2><a name="content007">Invariant の種類</a></h2> + +<pre> + 等式 + 生成データを限定した data 記述 + 減少列 + 生成されるものの有限性 + P_1 -> P_n +</div> +<ol class="side" id="menu"> +GearsAgda : Meta continuation based Hoare Logic +<li><a href="#content000"> Continuation based C and GearsAgda</a> +<li><a href="#content001"> Gears OS</a> +<li><a href="#content002"> Gears OSのモデル検査</a> +<li><a href="#content003"> GearAgda の Hoare Logic</a> +<li><a href="#content004"> Gears OS による赤黒木のモデル検査</a> +<li><a href="#content005"> GearsAgda による赤黒木の証明</a> +<li><a href="#content006"> GearsAgdaのモデル検査</a> +<li><a href="#content007"> Invariant の種類</a> +</ol> + +<hr/> Shinji KONO <kono@ie.u-ryukyu.ac.jp> / Thu Jan 6 10:48:24 2022 +</body></html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/gearsAgda.ind Sat Apr 15 11:39:08 2023 +0900 @@ -0,0 +1,227 @@ +-title: GearsAgda : Meta continuation based Hoare Logic + +--Continuation based C and GearsAgda + +goto 文中心に記述する。LLVM/GCC で実装されている。コンパイラの Basic block に相当する + +C form + __code whileLoop(EnvPtr en, __code next(EnvPtr en)) { + if ( 0 >= en->varn ) goto next(en); + else { + en->varn = en->varn - 1; + en->vari = en->vari + 1; + goto whileLoop(en, next); + } + } + +Agda は pure fuctional な depedent type language。証明を記述できる。goto 文は、以下の形式で記述する。 + +Agda form + + whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t + whileTest c10 next = next (record {varn = c10 ; vari = 0} ) + + {-# 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 + + test1 : Env + test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) + +TERMINATING は停止性が確認できないことを示している。 + +--Gears OS + +CbC と dataGear で構成する OS。 + + __code putdown_rfork(struct PhilsImpl* phils, __code next(...)) { + struct AtomicT_int* right_fork = phils->Rightfork; + goto right_fork->set(-1, putdown_lfork); + } + +をメタ計算で表すと、 + + __code putdown_rforkPhilsImpl_stub(struct Context* context) { + PhilsImpl* phils = (PhilsImpl*)GearImpl(context, Phils, phils); + enum Code next = Gearef(context, Phils)->next; + goto putdown_rforkPhilsImpl(context, phils, next); + } + + __code putdown_lforkPhilsImpl(struct Context *context,struct PhilsImpl* phils, enum Code next) { + struct AtomicT_int* left_fork = phils->Leftfork; + Gearef(context, AtomicT_int)->atomicT_int = (union Data*) left_fork; + Gearef(context, AtomicT_int)->newData = -1; + Gearef(context, AtomicT_int)->next = C_thinkingPhilsImpl; + goto mcMeta(context, left_fork->set); + } + +となる。メタレベルでは引数は context と次の codeGearの番号だけ。 + +GearsAgda でも、同様の実装ができる。 + +<center><img src="fig/meta_cg_dg.svg"></center> + +--Gears OSのモデル検査 + + __ncode mcMeta(struct Context* context, enum Code next) { + context->next = next; // remember next Code Gear + int found = visit_StateDB(out, &mcti->state_db, &out,mcWorker->visit); + if (found) { + while(!(list = takeNextIterator(mcWorker->task_iter))) { + +mcMeta で状態を記録し、非決定的な実行を網羅する。 + +<center><img src="fig/model_checking.svg"></center> + +--GearAgda の Hoare Logic + + whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10) + → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) + → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t + +このように loop を Segment に切り出す。Pre condtion と Post condition が付いている。これは命題で証明する必要がある。(容易) + + TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) + → (r : Index) → (p : Invraiant r) → t + TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r) + ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) + ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) + +減少列を使用して、停止性を保証する接続で停止性を含めて Hoare Logic による証明が可能。 + + whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ + whileTestSpec1 _ _ x = tt + +仕様は、継続で入力として受ける。 + + proofGearsTermS : {c10 : ℕ } → ⊤ + proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → + TerminatingLoopS Env (λ env → varn env) + (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) + +これは、プログラムが証明を値として渡すので、実際に証明になっている。接続するだけでよい。 + +--Gears OS による赤黒木のモデル検査 + +木ではなくループ構造を使う。ノードは子供を iterator で返す。これを前述のモデル検査器で調べる。 + +まだ、やってません。 + +赤黒木は実装済み。 + +--GearsAgda による赤黒木の証明 + +まず、Binary Tree + + data bt {n : Level} (A : Set n) : Set n where + leaf : bt A + node : (key : ℕ) → (value : A) → + (left : bt A ) → (right : bt A ) → bt A + + bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ + bt-depth leaf = 0 + bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ )) + +普通のデータ構造 + + find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A) + → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t + find key leaf st _ exit = exit leaf st + find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁ + find key n st _ exit | tri≈ ¬a b ¬c = exit n st + find key n@(node key₁ v tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st) + find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) + + {-# TERMINATING #-} + find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t + find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where + find-loop1 : bt A → List (bt A) → t + find-loop1 tree st = find key tree st find-loop1 exit + + insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t + insertTree tree key value exit = find-loop key tree [] $ λ t st → replaceNode key value t $ λ t1 → replace-loop key value t1 st exit + + insertTest1 = insertTree leaf 1 1 (λ x → x ) + insertTest2 = insertTree insertTest1 2 1 (λ x → x ) + +継続( GearsAgda 形式)を用いた実装。これに Hoare条件をつける。 + + findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) + → treeInvariant tree ∧ stackInvariant key tree tree0 stack + → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → t ) → t + +invariant はこんな感じ。 + + data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where + t-leaf : treeInvariant leaf + t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂) + → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₂ value₂ t₃ t₄) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) + + data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where + s-nil : stackInvariant key0 leaf leaf [] + s-right : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left : bt A} → {st : List (bt A)} + → key < key0 → stackInvariant key0(node key value left tree ) tree0 (node key value left tree ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value left tree ∷ st ) + s-left : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right : bt A} → {st : List (bt A)} + → key0 < key → stackInvariant key0(node key value tree right ) tree0 (node key value tree right ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value tree right ∷ st ) + + data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where + +簡単とは言えない。条件をrecord にまとめた方がよい。 + + record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where + field + tree0 : bt A + ti : treeInvariant tree0 + si : stackInvariant key tree tree0 stack + ci : C tree stack -- data continuation + +ci はテストとか記述する部分。データの継続になっている。この部分をあとで追加できる。 + + containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ + containsTree {n} {m} {A} {t} tree tree1 key value P RT = + TerminatingLoopS (bt A ∧ List (bt A) ) + {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p)) + ⟪ tree1 , [] ⟫ {!!} + $ λ p P loop → findPPC key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) + $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where + +みたいな感じで証明する。 + + insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ + insertTreeSpec0 _ _ _ = tt + +仕様記述は、継続の入力で受ける。 + +--GearsAgdaのモデル検査 + +GearsOS と同じように構成することにより、並列実行を simulation できる。モデル検査器そのものを Hoare Logic base で証明、 +あるいは、展開した(比較的膨大な)部分を全部証明する。あるいは、モデル検査を実行することにより並列分散プログラムを +検証できるはず。 + + +--Invariant の種類 + + 等式 + 生成データを限定した data 記述 + 減少列 + 生成されるものの有限性 + P_1 -> P_n + + + + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/gearsAgda.md Sat Apr 15 11:39:08 2023 +0900 @@ -0,0 +1,242 @@ +GearsAgda : Meta continuation based Hoare Logic +==== + + +## Continuation based C and GearsAgda + +goto 文中心に記述する。LLVM/GCC で実装されている。コンパイラの Basic block に相当する + +C form +``` + __code whileLoop(EnvPtr en, __code next(EnvPtr en)) { + if ( 0 >= en->varn ) goto next(en); + else { + en->varn = en->varn - 1; + en->vari = en->vari + 1; + goto whileLoop(en, next); + } + } +``` +Agda は pure fuctional な depedent type language。証明を記述できる。goto 文は、以下の形式で記述する。 + +Agda form + +``` + whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t + whileTest c10 next = next (record {varn = c10 ; vari = 0} ) + {-# 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 + test1 : Env + test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) +``` +TERMINATING は停止性が確認できないことを示している。 + + + +## Gears OS +CbC と dataGear で構成する OS。 + +``` + __code putdown_rfork(struct PhilsImpl* phils, __code next(...)) { + struct AtomicT_int* right_fork = phils->Rightfork; + goto right_fork->set(-1, putdown_lfork); + } +``` +をメタ計算で表すと、 + +``` + __code putdown_rforkPhilsImpl_stub(struct Context* context) { + PhilsImpl* phils = (PhilsImpl*)GearImpl(context, Phils, phils); + enum Code next = Gearef(context, Phils)->next; + goto putdown_rforkPhilsImpl(context, phils, next); + } + __code putdown_lforkPhilsImpl(struct Context *context,struct PhilsImpl* phils, enum Code next) { + struct AtomicT_int* left_fork = phils->Leftfork; + Gearef(context, AtomicT_int)->atomicT_int = (union Data*) left_fork; + Gearef(context, AtomicT_int)->newData = -1; + Gearef(context, AtomicT_int)->next = C_thinkingPhilsImpl; + goto mcMeta(context, left_fork->set); + } +``` +となる。メタレベルでは引数は context と次の codeGearの番号だけ。 + +GearsAgda でも、同様の実装ができる。 + +<img src="fig/meta_cg_dg.svg" class="internal-embed"/> + + + + +## Gears OSのモデル検査 +``` + __ncode mcMeta(struct Context* context, enum Code next) { + context->next = next; // remember next Code Gear + int found = visit_StateDB(out, &mcti->state_db, &out,mcWorker->visit); + if (found) { + while(!(list = takeNextIterator(mcWorker->task_iter))) { +``` +mcMeta で状態を記録し、非決定的な実行を網羅する。 + +<img src="fig/model_checking.svg" class="internal-embed"/> + + + + +## GearAgda の Hoare Logic +``` + whileLoopSeg : {l : Level} {t : Set l} → {c10 : ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10) + → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) + → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t +``` +このように loop を Segment に切り出す。Pre condtion と Post condition が付いている。これは命題で証明する必要がある。(容易) + +``` + TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) + → (r : Index) → (p : Invraiant r) → t + TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r) + ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) + ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) +``` +減少列を使用して、停止性を保証する接続で停止性を含めて Hoare Logic による証明が可能。 + +``` + whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ + whileTestSpec1 _ _ x = tt +``` +仕様は、継続で入力として受ける。 + +``` + proofGearsTermS : {c10 : ℕ } → ⊤ + proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → + TerminatingLoopS Env (λ env → varn env) + (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) +``` +これは、プログラムが証明を値として渡すので、実際に証明になっている。接続するだけでよい。 + + + +## Gears OS による赤黒木のモデル検査 +木ではなくループ構造を使う。ノードは子供を iterator で返す。これを前述のモデル検査器で調べる。 + +まだ、やってません。 + +赤黒木は実装済み。 + + + +## GearsAgda による赤黒木の証明 +まず、Binary Tree + +``` + data bt {n : Level} (A : Set n) : Set n where + leaf : bt A + node : (key : ℕ) → (value : A) → + (left : bt A ) → (right : bt A ) → bt A + bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ + bt-depth leaf = 0 + bt-depth (node key value t t₁) = suc (Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ )) +``` +普通のデータ構造 + +``` + find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A) + → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t + find key leaf st _ exit = exit leaf st + find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁ + find key n st _ exit | tri≈ ¬a b ¬c = exit n st + find key n@(node key₁ v tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st) + find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) + {-# TERMINATING #-} + find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t + find-loop {n} {m} {A} {t} key tree st exit = find-loop1 tree st where + find-loop1 : bt A → List (bt A) → t + find-loop1 tree st = find key tree st find-loop1 exit + insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t + insertTree tree key value exit = find-loop key tree [] $ λ t st → replaceNode key value t $ λ t1 → replace-loop key value t1 st exit + insertTest1 = insertTree leaf 1 1 (λ x → x ) + insertTest2 = insertTree insertTest1 2 1 (λ x → x ) +``` +継続( GearsAgda 形式)を用いた実装。これに Hoare条件をつける。 + +``` + findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) + → treeInvariant tree ∧ stackInvariant key tree tree0 stack + → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → t ) → t +``` +invariant はこんな感じ。 + +``` + data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where + t-leaf : treeInvariant leaf + t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂) + → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₂ value₂ t₃ t₄) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) + data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where + s-nil : stackInvariant key0 leaf leaf [] + s-right : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left : bt A} → {st : List (bt A)} + → key < key0 → stackInvariant key0(node key value left tree ) tree0 (node key value left tree ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value left tree ∷ st ) + s-left : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right : bt A} → {st : List (bt A)} + → key0 < key → stackInvariant key0(node key value tree right ) tree0 (node key value tree right ∷ st ) → stackInvariant key0 tree tree0 (tree ∷ node key value tree right ∷ st ) + data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where +``` +簡単とは言えない。条件をrecord にまとめた方がよい。 + +``` + record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where + field + tree0 : bt A + ti : treeInvariant tree0 + si : stackInvariant key tree tree0 stack + ci : C tree stack -- data continuation + +``` +ci はテストとか記述する部分。データの継続になっている。この部分をあとで追加できる。 + +``` + containsTree : {n m : Level} {A : Set n} {t : Set m} → (tree tree1 : bt A) → (key : ℕ) → (value : A) → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ + containsTree {n} {m} {A} {t} tree tree1 key value P RT = + TerminatingLoopS (bt A ∧ List (bt A) ) + {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p)) + ⟪ tree1 , [] ⟫ {!!} + $ λ p P loop → findPPC key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) + $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where +``` +みたいな感じで証明する。 + +``` + insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ + insertTreeSpec0 _ _ _ = tt +``` +仕様記述は、継続の入力で受ける。 + + + +## GearsAgdaのモデル検査 +GearsOS と同じように構成することにより、並列実行を simulation できる。モデル検査器そのものを Hoare Logic base で証明、 +あるいは、展開した(比較的膨大な)部分を全部証明する。あるいは、モデル検査を実行することにより並列分散プログラムを +検証できるはず。 + + + +## Invariant の種類 +``` + 等式 + 生成データを限定した data 記述 + 減少列 + 生成されるものの有限性 + P_1 -> P_n + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/rbtree-gearsagda.mm Sat Apr 15 11:39:08 2023 +0900 @@ -0,0 +1,230 @@ +<map version="freeplane 1.9.13"> +<!--To view this file, download free mind mapping software Freeplane from https://www.freeplane.org --> +<node TEXT="rbtree-gearsagda" FOLDED="false" ID="ID_452131666" CREATED="1610381621610" MODIFIED="1681354145545" STYLE="oval"> +<font SIZE="18"/> +<hook NAME="MapStyle" zoom="0.75"> + <properties edgeColorConfiguration="#808080ff,#ff0000ff,#0000ffff,#00ff00ff,#ff00ffff,#00ffffff,#7c0000ff,#00007cff,#007c00ff,#7c007cff,#007c7cff,#7c7c00ff" fit_to_viewport="false" associatedTemplateLocation="template:/standard-1.6-noEdgeColor.mm" show_icon_for_attributes="true" show_note_icons="true"/> + +<map_styles> +<stylenode LOCALIZED_TEXT="styles.root_node" STYLE="oval" UNIFORM_SHAPE="true" VGAP_QUANTITY="24 pt"> +<font SIZE="24"/> +<stylenode LOCALIZED_TEXT="styles.predefined" POSITION="right" STYLE="bubble"> +<stylenode LOCALIZED_TEXT="default" ID="ID_207122690" COLOR="#000000" STYLE="fork"> +<arrowlink SHAPE="CUBIC_CURVE" COLOR="#000000" WIDTH="2" TRANSPARENCY="200" DASH="" FONT_SIZE="9" FONT_FAMILY="SansSerif" DESTINATION="ID_207122690" STARTARROW="NONE" ENDARROW="DEFAULT"/> +<font NAME="SansSerif" SIZE="10" BOLD="false" ITALIC="false"/> +<richcontent CONTENT-TYPE="plain/auto" TYPE="DETAILS"/> +<richcontent TYPE="NOTE" CONTENT-TYPE="plain/auto"/> +</stylenode> +<stylenode LOCALIZED_TEXT="defaultstyle.details"/> +<stylenode LOCALIZED_TEXT="defaultstyle.attributes"> +<font SIZE="9"/> +</stylenode> +<stylenode LOCALIZED_TEXT="defaultstyle.note" COLOR="#000000" BACKGROUND_COLOR="#ffffff" TEXT_ALIGN="LEFT"/> +<stylenode LOCALIZED_TEXT="defaultstyle.floating"> +<edge STYLE="hide_edge"/> +<cloud COLOR="#f0f0f0" SHAPE="ROUND_RECT"/> +</stylenode> +<stylenode LOCALIZED_TEXT="defaultstyle.selection" BACKGROUND_COLOR="#afd3f7" BORDER_COLOR_LIKE_EDGE="false" BORDER_COLOR="#afd3f7"/> +</stylenode> +<stylenode LOCALIZED_TEXT="styles.user-defined" POSITION="right" STYLE="bubble"> +<stylenode LOCALIZED_TEXT="styles.topic" COLOR="#18898b" STYLE="fork"> +<font NAME="Liberation Sans" SIZE="10" BOLD="true"/> +</stylenode> +<stylenode LOCALIZED_TEXT="styles.subtopic" COLOR="#cc3300" STYLE="fork"> +<font NAME="Liberation Sans" SIZE="10" BOLD="true"/> +</stylenode> +<stylenode LOCALIZED_TEXT="styles.subsubtopic" COLOR="#669900"> +<font NAME="Liberation Sans" SIZE="10" BOLD="true"/> +</stylenode> +<stylenode LOCALIZED_TEXT="styles.important" ID="ID_3752836"> +<icon BUILTIN="yes"/> +<arrowlink COLOR="#003399" TRANSPARENCY="255" DESTINATION="ID_3752836"/> +</stylenode> +</stylenode> +<stylenode LOCALIZED_TEXT="styles.AutomaticLayout" POSITION="right" STYLE="bubble"> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level.root" COLOR="#000000" STYLE="oval" SHAPE_HORIZONTAL_MARGIN="10 pt" SHAPE_VERTICAL_MARGIN="10 pt"> +<font SIZE="18"/> +</stylenode> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,1" COLOR="#0033ff"> +<font SIZE="16"/> +</stylenode> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,2" COLOR="#00b439"> +<font SIZE="14"/> +</stylenode> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,3" COLOR="#990000"> +<font SIZE="12"/> +</stylenode> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,4" COLOR="#111111"> +<font SIZE="10"/> +</stylenode> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,5"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,6"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,7"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,8"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,9"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,10"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,11"/> +</stylenode> +</stylenode> +</map_styles> +</hook> +<node TEXT="GearAgdanによるRed Black Tree の検証" POSITION="right" ID="ID_1707429913" CREATED="1681354146375" MODIFIED="1681354149504"/> +<node TEXT="Gears OS" POSITION="left" ID="ID_1627768067" CREATED="1681370097231" MODIFIED="1681370135147"> +<node TEXT="Continuation based C" ID="ID_886365419" CREATED="1681370135452" MODIFIED="1681370144727"/> +<node TEXT="CodeGear and DataGear" ID="ID_1505619678" CREATED="1681370145576" MODIFIED="1681370169360"/> +<node TEXT="GearsAgda" ID="ID_1483093782" CREATED="1681370170247" MODIFIED="1681370174624"/> +<node TEXT="lightweigt continuation" ID="ID_709373441" CREATED="1681370232271" MODIFIED="1681370241482"/> +</node> +<node TEXT="meta computation" POSITION="left" ID="ID_587222105" CREATED="1681370246638" MODIFIED="1681370255183"> +<node TEXT="IO" ID="ID_939386664" CREATED="1681370255664" MODIFIED="1681370261532"/> +<node TEXT="Hoare Logic" ID="ID_468705414" CREATED="1681370262977" MODIFIED="1681370270967"/> +</node> +<node TEXT="meata computation in GearsAgda" POSITION="left" ID="ID_1679966111" CREATED="1681370285647" MODIFIED="1681370300383"> +<node TEXT="Gears Form" ID="ID_562028595" CREATED="1681370303175" MODIFIED="1681370328863"/> +<node TEXT="Meta computation" ID="ID_532649685" CREATED="1681370334319" MODIFIED="1681370340118"/> +<node TEXT="Segment" ID="ID_1391622726" CREATED="1681370342818" MODIFIED="1681370346242"/> +<node TEXT="stub" ID="ID_1481524131" CREATED="1681370347413" MODIFIED="1681370350369"/> +<node TEXT="CodeGear table" ID="ID_528079968" CREATED="1681370352629" MODIFIED="1681370366378"/> +</node> +<node TEXT="Hoare Logic" POSITION="left" ID="ID_590542814" CREATED="1681370375413" MODIFIED="1681370379970"> +<node TEXT="command base" ID="ID_1041738747" CREATED="1681370380249" MODIFIED="1681370383059"/> +<node TEXT="first order" ID="ID_1511997811" CREATED="1681370399684" MODIFIED="1681370403829"/> +<node TEXT="soundness" ID="ID_783227970" CREATED="1681370407410" MODIFIED="1681370413286"> +<node TEXT="separated from program" ID="ID_549960702" CREATED="1681370413548" MODIFIED="1681370423487"/> +</node> +<node TEXT="no proof support" ID="ID_94897053" CREATED="1681370433921" MODIFIED="1681370438778"/> +</node> +<node TEXT="GearsAgda" POSITION="left" ID="ID_613685836" CREATED="1681370441463" MODIFIED="1681370446502"> +<node TEXT="written in Agda" ID="ID_883451142" CREATED="1681370450642" MODIFIED="1681370456415"> +<node TEXT="proof assistance" ID="ID_567095247" CREATED="1681370456760" MODIFIED="1681370462431"/> +</node> +<node TEXT="any lightweight continuation form" ID="ID_512231980" CREATED="1681370472049" MODIFIED="1681370490394"/> +<node TEXT="close to basic unit in a compiler" ID="ID_1639405885" CREATED="1681370493600" MODIFIED="1681370507300"/> +<node TEXT="concurrency" ID="ID_1969768669" CREATED="1681370510538" MODIFIED="1681370522360"/> +<node TEXT="meta computation" ID="ID_1341787488" CREATED="1681370523208" MODIFIED="1681370528202"> +<node TEXT="Hoare Logic style" ID="ID_1596917933" CREATED="1681370535368" MODIFIED="1681370546348"/> +<node TEXT="with invariant" ID="ID_1946393368" CREATED="1681370547204" MODIFIED="1681370553272"/> +</node> +<node TEXT="data with proofs" ID="ID_1144050858" CREATED="1681370596859" MODIFIED="1681370601940"> +<node TEXT="invariant" ID="ID_375933480" CREATED="1681370605320" MODIFIED="1681370610877"/> +<node TEXT="much simpler" ID="ID_245103686" CREATED="1681370613781" MODIFIED="1681370622639"/> +</node> +</node> +<node TEXT="concurrency" POSITION="right" ID="ID_1659998734" CREATED="1681370628915" MODIFIED="1681370636745"> +<node TEXT="codeGear-wise concurency" ID="ID_1216124303" CREATED="1681370637291" MODIFIED="1681370656059"/> +<node TEXT="assuming finite computation in a codeGear" ID="ID_573537896" CREATED="1681370657029" MODIFIED="1681370677168"/> +<node TEXT="scheduler" ID="ID_327350914" CREATED="1681370679365" MODIFIED="1681370685685"> +<node TEXT="in meta computation" ID="ID_1272612921" CREATED="1681370686271" MODIFIED="1681370693104"/> +<node TEXT="code table" ID="ID_1779321838" CREATED="1681370741527" MODIFIED="1681370746964"> +<node TEXT="all codeGear" ID="ID_1073597539" CREATED="1681370747218" MODIFIED="1681370752548"/> +<node TEXT="numbered" ID="ID_1618653220" CREATED="1681370753308" MODIFIED="1681370756196"/> +<node TEXT="stub" ID="ID_573578192" CREATED="1681370756935" MODIFIED="1681370759362"/> +</node> +<node TEXT="Context" ID="ID_1995851564" CREATED="1681370693516" MODIFIED="1681370697602"> +<node TEXT="current code" ID="ID_1885258842" CREATED="1681370728219" MODIFIED="1681370732220"/> +<node TEXT="all dataGear" ID="ID_1859577487" CREATED="1681370733587" MODIFIED="1681370739913"/> +</node> +<node TEXT="communication" ID="ID_387799092" CREATED="1681370705533" MODIFIED="1681370712647"/> +</node> +<node TEXT="model checking" ID="ID_1191776209" CREATED="1681370766180" MODIFIED="1681370771240"/> +<node TEXT="proofs on concurrenct" ID="ID_1117350246" CREATED="1681370771658" MODIFIED="1681370781273"/> +</node> +<node TEXT="while program" POSITION="right" ID="ID_710382637" CREATED="1681370805471" MODIFIED="1681370811890"/> +<node TEXT="binary tree" POSITION="right" ID="ID_1922786513" CREATED="1681370796432" MODIFIED="1681370804204"> +<node TEXT="stack invariant" ID="ID_1448419661" CREATED="1681370821482" MODIFIED="1681370830261"/> +<node TEXT="tree invariant" ID="ID_243832132" CREATED="1681370830768" MODIFIED="1681370835246"/> +<node TEXT="replace invariant" ID="ID_1303870466" CREATED="1681370835840" MODIFIED="1681370840736"/> +</node> +<node TEXT="red black tree" POSITION="right" ID="ID_263237724" CREATED="1681370787198" MODIFIED="1681370792658"> +<node TEXT="red and black" ID="ID_385223552" CREATED="1681370848145" MODIFIED="1681370856270"/> +<node TEXT="parent and grand parent" ID="ID_517970079" CREATED="1681370857076" MODIFIED="1681370866920"> +<node TEXT="in stack" ID="ID_901165358" CREATED="1681370867215" MODIFIED="1681370872234"/> +</node> +<node TEXT="concurrency" ID="ID_23246060" CREATED="1681370878663" MODIFIED="1681370883733"> +<node TEXT="root replacement" ID="ID_184711355" CREATED="1681370884231" MODIFIED="1681370892725"> +<node TEXT="transaction" ID="ID_1256246418" CREATED="1681370893169" MODIFIED="1681370898372"/> +</node> +<node TEXT="non destructive" ID="ID_1377710910" CREATED="1681370903423" MODIFIED="1681370909214"> +<node TEXT="read sharing" ID="ID_1853077777" CREATED="1681370910265" MODIFIED="1681370917627"/> +</node> +</node> +</node> +<node TEXT="complied code" POSITION="right" ID="ID_1551916219" CREATED="1681370926034" MODIFIED="1681370931197"> +<node TEXT="gearsAgda → CbC conversion" ID="ID_159756131" CREATED="1681370931496" MODIFIED="1681370953438"/> +<node TEXT="combine multiple codeGear" ID="ID_1952851358" CREATED="1681371036240" MODIFIED="1681371047551"> +<node TEXT="optimization" ID="ID_256515995" CREATED="1681371048689" MODIFIED="1681371053081"/> +</node> +</node> +<node TEXT="is this reliable?" POSITION="right" ID="ID_189224322" CREATED="1681370969828" MODIFIED="1681370979059"> +<node TEXT="with proofs" ID="ID_114174861" CREATED="1681370979357" MODIFIED="1681370985340"> +<node TEXT="relative to the theory" ID="ID_194349290" CREATED="1681370985587" MODIFIED="1681371003316"/> +</node> +<node TEXT="invariant gives all property" ID="ID_955091732" CREATED="1681371007176" MODIFIED="1681371020551"/> +</node> +<node TEXT="is this scale?" POSITION="right" ID="ID_1442547192" CREATED="1681371022394" MODIFIED="1681371028550"> +<node TEXT="size of invariant" ID="ID_66636375" CREATED="1681470579922" MODIFIED="1681470584136"/> +<node TEXT="polynominal of cases of invariant" ID="ID_1431513531" CREATED="1681470584691" MODIFIED="1681470597800"/> +<node TEXT="not all combination is possible" ID="ID_1626555105" CREATED="1681470604805" MODIFIED="1681470612527"/> +<node TEXT="we don't need to fill all the proof" ID="ID_1601614737" CREATED="1681470615256" MODIFIED="1681470627377"> +<node TEXT="incremental" ID="ID_1230800920" CREATED="1681470627899" MODIFIED="1681470630690"/> +<node TEXT="partial" ID="ID_649982266" CREATED="1681470631099" MODIFIED="1681470634557"/> +</node> +</node> +<node TEXT="contents" POSITION="right" ID="ID_1884614552" CREATED="1681470012072" MODIFIED="1681470018912"> +<node TEXT="verified red black tree" ID="ID_72137676" CREATED="1681470019151" MODIFIED="1681470047634"/> +<node TEXT="importance" ID="ID_510340227" CREATED="1681470049510" MODIFIED="1681470056562"> +<node TEXT="conversion to classical form" ID="ID_312471113" CREATED="1681470523375" MODIFIED="1681470532568"> +<node TEXT="destructive" ID="ID_1083852390" CREATED="1681470532868" MODIFIED="1681470536236"/> +<node TEXT="B-tree" ID="ID_1942790971" CREATED="1681470545925" MODIFIED="1681470551384"/> +</node> +<node TEXT="sequencial" ID="ID_783108258" CREATED="1681470056922" MODIFIED="1681470064048"/> +<node TEXT="concurrent" ID="ID_924506929" CREATED="1681470065130" MODIFIED="1681470068278"/> +</node> +<node TEXT="GearsAgda" ID="ID_1614171466" CREATED="1681470071381" MODIFIED="1681470074368"> +<node TEXT="lightweight contination" ID="ID_351064745" CREATED="1681470074675" MODIFIED="1681470097157"/> +<node TEXT="CbC" ID="ID_280197854" CREATED="1681470108615" MODIFIED="1681470110151"/> +</node> +<node TEXT="classical approach" ID="ID_439782904" CREATED="1681470111745" MODIFIED="1681470120213"> +<node TEXT="Hoare Logic" ID="ID_182843234" CREATED="1681470120549" MODIFIED="1681470123261"/> +<node TEXT="conversion to Haskell" ID="ID_18215857" CREATED="1681470123809" MODIFIED="1681470131336"/> +<node TEXT="verified but ..." ID="ID_86587986" CREATED="1681470188224" MODIFIED="1681470199159"/> +</node> +<node TEXT="GearsAgda" ID="ID_1624783880" CREATED="1681470180677" MODIFIED="1681470219506"> +<node TEXT="invariant" ID="ID_1822140966" CREATED="1681470228788" MODIFIED="1681470232318"> +<node TEXT="denotational semantics" ID="ID_1070066378" CREATED="1681470408330" MODIFIED="1681470415583"/> +</node> +<node TEXT="agda introduction" ID="ID_1367482138" CREATED="1681470219860" MODIFIED="1681470227830"/> +<node TEXT="simple while loop" ID="ID_594789165" CREATED="1681470293741" MODIFIED="1681470299458"/> +<node TEXT="loop connector" ID="ID_351381557" CREATED="1681470305517" MODIFIED="1681470311087"> +<node TEXT="reduction parameter" ID="ID_1854148894" CREATED="1681470317762" MODIFIED="1681470324065"/> +</node> +</node> +<node TEXT="binary tree" ID="ID_1045767712" CREATED="1681470238269" MODIFIED="1681470245777"> +<node TEXT="invariant" ID="ID_753395200" CREATED="1681470246095" MODIFIED="1681470248201"> +<node TEXT="tree" ID="ID_1179203442" CREATED="1681470248688" MODIFIED="1681470254441"/> +<node TEXT="stack" ID="ID_743804922" CREATED="1681470255070" MODIFIED="1681470256626"/> +<node TEXT="replace" ID="ID_1919439558" CREATED="1681470257216" MODIFIED="1681470260232"/> +</node> +<node TEXT="program guidance" ID="ID_1331715304" CREATED="1681470429863" MODIFIED="1681470434889"> +<node TEXT="differential of invariant" ID="ID_1547779379" CREATED="1681470435636" MODIFIED="1681470444235"/> +</node> +</node> +<node TEXT="red black tree" ID="ID_233668516" CREATED="1681470263078" MODIFIED="1681470266745"/> +<node TEXT="concurrency" ID="ID_1836297821" CREATED="1681470271427" MODIFIED="1681470275872"> +<node TEXT="segmented" ID="ID_290000164" CREATED="1681470276209" MODIFIED="1681470282080"/> +<node TEXT="code table" ID="ID_278977606" CREATED="1681470350363" MODIFIED="1681470354017"/> +<node TEXT="scheduler" ID="ID_111624804" CREATED="1681470354785" MODIFIED="1681470364123"> +<node TEXT="fairness" ID="ID_1334406786" CREATED="1681470365738" MODIFIED="1681470368781"/> +</node> +<node TEXT="temporal logic" ID="ID_1823540844" CREATED="1681470371933" MODIFIED="1681470376053"/> +</node> +<node TEXT="execution" ID="ID_95297285" CREATED="1681470455878" MODIFIED="1681470458355"> +<node TEXT="data gear with proof is executable" ID="ID_1369250602" CREATED="1681470459700" MODIFIED="1681470472621"/> +<node TEXT="need not to fill the proof" ID="ID_1356375326" CREATED="1681470474612" MODIFIED="1681470483972"/> +</node> +<node TEXT="scalability" ID="ID_1468980711" CREATED="1681470382482" MODIFIED="1681470389280"> +<node TEXT="invariant library" ID="ID_1421089406" CREATED="1681470391295" MODIFIED="1681470395791"/> +</node> +</node> +</node> +</map>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/rbtree.ind Sat Apr 15 11:39:08 2023 +0900 @@ -0,0 +1,307 @@ +-title: GearsAgdaによる Red Black Tree の検証 + +-author: 河野真治 + +--abstract: + +--検証された Red Black Treeの重要性 + +OSを含むアプリケーションの + +--CbCに証明を付け加えた GearsAgda + +CbC は goto 文中心に記述する言語で、\verb+__code+ という単位で実行される。この実行単位は +有限な時間(OSのtickなど)で実行することが想定されている。つまり、不定なloop はgoto文の +外で組み合わされる。 + +CbC はLLVM/GCC で実装されている。コンパイラの Basic block に相当すると考えてもよい。 +C form では例えば以下のように記述する。ここでは変数は record Env に格納されている。 + + __code whileLoop(Env *en, __code next(Env *en)) { + if ( 0 >= en->varn ) goto next(en); + else { + en->varn = en->varn - 1; + en->vari = en->vari + 1; + goto whileLoop(en, next); + } + } + +Agda は pure fuctional な depedent type languageで証明を記述できる。CbC の実行単位 codeGear は +以下の形式 Agda form で記述する。常に不定の型{\tt t}を返すのが特徴になっている。 + +Agda ではCの構造体に対応するのは record で、以下のように定義する。 + + record Env ( c : ℕ ) : Set where + field + varn : ℕ + vari : ℕ + +これにより、codeGear からは指定された継続(continuation)を呼ぶしか型的に緩されない。これが、 +CbCのgoto文に相当する。変数の初期化を行う codeGear は以下のようになる。\verb+record {}+ +が record の初期化になっている。 + + whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t + whileTest c10 next = next (record {varn = c10 ; vari = 0} ) + +ここで、\verb+ a → b → c + は、\verb+ ( a → b ) → c + であり、Curry化に対応している。 +例えば、仕様は + + whileTestSpec1 : (c10 : ℕ) → (e1 : Env c10 ) → vari e1 ≡ c10 → ⊤ + whileTestSpec1 _ _ x = tt + +という形に書ける。ここで、⊤は、tt というただひとつの値を持つ型 + + data ⊤ : Set where + tt : ⊤ + +である。これにより、 + + initTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : (en : Env c10 ) → vari en ≡ c10 → t) → t + initTest c10 next = next (record {vari = c10 ; varn = 0 }) refl + +という風に初期化が正しく値を設定していることを証明付きで書ける。ここで + + data _≡_ {A : Set } (x y : A) : Set where + refl {x : A} → x ≡ x + +で、x = x つまり、自分自身は等しいという自然演繹の等式の推論になっている。この等しさは、λ項の既約項同士の +単一化なので、かなり複雑な操作になる。なので、一般的には等式の証明は自明にはならない。Agda では +式変形をサポートしているので、少し見やすくすることが可能になってる。 + +実際に whilteTestSpec1 を検証するには + + test0 : {l : Level} {t : Set l} → (c10 : ℕ) → ⊤ + test0 c10 = initTest c10 (λ en eq → whileTestSpec1 c10 en eq ) + +とする。initTest は値を提供している。Agda では証明は証明操作を表すλ項なので値になっている。 + +仕様は複雑なプログラムの動作の結果として満たされるものなので、プログラムの内部に記述する必要がある。 + +initTest の\verb+vari en ≡ c10+ の証明は、その場で refl で行われている。whilteTestSpec1 はそれを +受け取っているだけになっている。test1 での en は「任意のEnv record」なので、\verb+vari en ≡ c10+ の証明 +は持っていない。 + +--古典的な手法 + +プログラムを検証する方法としては、Hoare Logic \cite{hoare} が知られている。これは、プログラムを command で記述し、 +前提に成立する条件 Pre と 実行後に成立する条件 Post との + + {Pre} command {Post} + +の三つ組で条件を command 毎に記述していく方法である。command を例えばアセンブラ的な命令にすれば、プログラムの正しさを +証明できる。loop の停止性の証明は、command 対してそれぞれ別に行う必要がある。 + +この方法では command 毎に Hoare logic のSoundnessを定義する必要がある。実際に Hoare logic をAgdaで実装した +例がある\cite{}。 + +--GearsAgda でのプログラム検証手法 + +プログラムの仕様はそのままAgdaの変数として持ち歩いているが、loop に関する証明を行うにはいくつか問題がある。 + +普通に while 文を書くと、Agdaが警告を出す。 + + {-# 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 + + test1 : Env + test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) + +\verb+{-# TERMINATING #-}+ はAgdaが 停止性が確認できないことを示している。 + +--simple while loop と証明付きデータ構造 + +loop の証明には、性質が保存する invariant (不変条件) と、停止性を示す reduction parameter (loopのたびに減少する自然数) +の二つを使う。この時に、invariant を別な条件として使うと、プログラム全体が複雑になる。そこで、 +データ構造そのものに invariant を付加するとよい。上の例題では、 + + record Env ( c : ℕ ) : Set where + field + varn : ℕ + vari : ℕ + n+i=c : varn + vari ≡ c + +とすると良い。この invariant を発見するのは一般的には難しいが、loop の構造とデータ構造、つまり、アルゴリズムとデータ構造 +から決まる。 + +whileLoop にinvariantの証明を足し、軽量継続で loop を分割すると、停止性を codeGear の段階で Agda が判断する必要がなくなる。 + + whileLoopSeg : {l : Level} {t : Set l} → (c10 : ℕ ) → (env : Env c10 ) + → (next : (e1 : Env c10 ) → varn e1 < varn env → t) + → (exit : (e1 : Env c10 ) → vari e1 ≡ c10 → t) → t + whileLoopSeg c10 env next exit with ( suc zero ≤? (varn env) ) + whileLoopSeg c10 env next exit | no p = exit env ? + whileLoopSeg c10 env next exit | yes p = next env1 ? where + +ここでは肝心の証明は \verb+?+ で省略している。Agda は、この様に証明を延期することができる。実際のコードでは +証明が提供されている。 + +停止性を示す reducde と、loop中にinvariantが保存することから、loop を Agda で直接に証明することができる。 + + TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → ( reduce : Index → ℕ) + → (loop : (r : Index) → (next : (r1 : Index) → reduce r1 < reduce r → t ) → t) + → (r : Index) → t + TerminatingLoopS {_} {t} Index reduce loop r with <-cmp 0 (reduce r) + ... | tri≈ ¬a b ¬c = loop r (λ r1 lt → ⊥-elim (lemma3 b lt) ) + ... | tri< a ¬b ¬c = loop r (λ r1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) lt1 ) where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j lt = loop r1 (λ r2 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 (suc j) r r1 n≤j lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a lt + ... | tri≈ ¬a b ¬c = loop r1 (λ r2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) + +ここで、\verb+tri≈+などは、二つの自然数を比較した <,=,> の三つの場合を表す data である。 +\verb+<-cmp 0 (reduce r)+ で、その三つの場合を作っている。そして、 \verb+... | tri> ¬a ¬b c = \+という形 +で受ける。\verb+⊥-elim ( nat-≤> c n≤j ) +は、矛盾の削除則である。 + +TerminatingLoopS では、loop からの脱出は記述されていない。indexが 0 以下になることはありえないので、 +loop はその前に終了しているはずである。それは、whileLoopSeg でのreduce の証明がそれを +保証している。つまり脱出条件は、TerminatingLoopS ではなく、whileLoopSeg で記述されている。 + +つまり、TerminatingLoopS は loop の接続を表す connector と考えることができる。 + +実際の証明は + + proofGearsTermS : (c10 : ℕ ) → ⊤ + proofGearsTermS c10 = + TerminatingLoopS (Env c10) (λ env → varn env) (λ n2 loop → whileLoopSeg c10 n2 loop (λ ne pe → whileTestSpec1 c10 ne pe ) ) + record { varn = 0 ; vari = c10 ; n+i=c = refl } + +というようになる。最初の初期化の証明と同じように、プログラムは値の部分にあり実際に実行されていて、 +それが仕様を満たしている証明を\verb+whileTestSpec1 c10 ne pe+が受け取っている。loop 変数が +whileLoopSeg の軽量継続を停止性込みで接続している。 + +--Hoare Logic との比較 + +Hoare Logicでは、command と条件の書き方を規定して、その規定の中で Logic のSoundnessを示している。 +条件の接続の段階で証明が必要であり、さらに Soundness での汎用的な証明が必要になる。commandによる +記述はアセンブラ的になる。 + +GearsAgda では、commandではなく、GearAgda の形式を満たして入れば良い。codeGear中で +dataGear の持つ条件を証明することになる。Soundness は connector に閉じていて、比較的容易に +証明される。さらに、? で証明を省略してもコード自体の実行は可能である。 + +この二つは、基本的に平行していて、Hoare Logic を理解していれば、GearsAgdaを理解することは問題ない。 +また、Agda を知っていれば、これが Hoare Logic だというように説明することも可能である。 + +これが可能になっているのは、GearsAgda の軽量継続による分解であり、任意の関数呼び出しては、 +それに合わせて、TerminatingLoopS に相当するものを記述する必要がある。 + +ただし、GearsAgda 自体が軽量継続による制限から、アセンブラ的(コンパイラの基本単位)になっている +ので、一般的な人向けのプログラミング言語のような可読性はない。 + +--binary tree + +二分木では、要素は自然のkeyによって順序付られている。普通のプログラミングでは、その順序付けは +明示されていない。GearsAgda で、それを invariant として記述することができる。 + +GearsAgda は、軽量継続による制約により再帰呼び出しはしないことになっている。これにより、 +CbC との直接の対応が可能になっている。なので、二分木への挿入 insert は、 + + find による挿入点の探索と、stackの構成 + stackをほどきながら木を置換していく操作 + +の二段階の構成になる。Haskell などでは、工夫された高階関数が使われるので stack は明示されない。 + + data bt {n : Level} (A : Set n) : Set n where + leaf : bt A + node : (key : ℕ) → (value : A) → + (left : bt A ) → (right : bt A ) → bt A + + data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where + t-leaf : treeInvariant leaf + t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf) + t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → treeInvariant (node key₁ value₁ t₁ t₂) + → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) + t-left : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) + t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂) + → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₂ value₂ t₃ t₄) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) + +これが二分木のデータ構造と invariant の実装になる。これは、invariant というよりは、順序付された二分木の可能な値全部の集合 +であり、二分木の表示的意味論\cite{}そのものになっている。 + +ここで、\reb+(key < key₁)+は、Agdaの型であり、そこには順序を示す data 構造が配る。つまり、二分木の順序は木の構成時に証明する +必要がある。 + +さらに、stack が木をたどった順に構成されていることと、木が置き換わっていることを示す invariant が必要である。 + + data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where + s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ []) + s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} + → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st) + s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} + → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st) + + data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt A ) → Set n where + r-leaf : replacedTree key value leaf (node key value leaf leaf) + r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) + r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} + → k < key → replacedTree key value t2 t → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) + r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} + → key < k → replacedTree key value t1 t → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) + +木の構造は同じ順序を持っていても、同じ形にはならない。このreplacedTree は、そういう場合が考慮されていない。 + + + findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) + → treeInvariant tree ∧ stackInvariant key tree tree0 stack + → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t + findP key leaf tree0 st Pre _ exit = exit leaf st Pre (case1 refl) + findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁ + findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl) + findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st) + ⟪ ? , ? ⟫ ? + findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) + ⟪ ? , ? ⟫ ? + +ここでも、実際の証明は? と省略している。ここで、木の深さをloopの停止条件として使っている。 + + replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) + → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) + → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value (child-replaced key tree) tree1 → t) → t + +repplaceのプログラムはさらに煩雑なので型だけを示す。 + +最終的に、これらを loop connector で接続して証明付きのプログラムが完成する。 + + insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree + → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t + insertTreeP {n} {m} {A} {t} tree key value P0 exit = + TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫ ⟪ P0 , s-nil ⟫ + $ λ p P loop → findP key (proj1 p) tree (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) + $ λ t s P C → replaceNodeP key value t C (proj1 P) + $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A ) + {λ p → replacePR key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) (λ _ _ _ → Lift n ⊤ ) } + (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt } + $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) P1 + (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt ) + $ λ tree repl P → exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫ + +このプログラムは順序付きの二分木のinvariantと、それが置換されているinvariantを返すので、そこから、 +必要な仕様をすべて導出することができる。例えば、木がソートされていること、置換したもの以外は保存されていることなどである。 + + +--red black tree + +赤黒木は、バランスした二分木の実装の一つである。木のノードに赤と黒の状態を持たせ、黒のノードの個数を左右でバランスさせる。 +かなり複雑な操作だが、ここでは非破壊的な赤黒木を使うので + + + +--Concurrency + +--実際に実行するには + +--証明のスケーラビリティ + +--まとめ +