Mercurial > hg > Papers > 2019 > ryokka-sigss

view ryokka-sigss.mm @ 8:83d000399c9d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix invisible char
author ryokka
date Tue, 18 Dec 2018 04:08:28 +0900
parents 493983f2c9db
children a87fec07fd78
line wrap: on
line source

<map version="1.0.1">
<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
<node CREATED="1542710800707" ID="ID_311099003" MODIFIED="1542710817736" TEXT="HoareLogic &#x3092;&#x7528;&#x3044;&#x305f; CbC &#x306e;&#x691c;&#x8a3c;">
<node CREATED="1542710937504" ID="ID_569346512" MODIFIED="1542710954774" POSITION="right" TEXT="&#x76ee;&#x6b21;">
<node CREATED="1542710833654" ID="ID_422945004" MODIFIED="1542710848431" TEXT="&#x7814;&#x7a76;&#x76ee;&#x7684;">
<node CREATED="1542712135796" ID="ID_1556598404" MODIFIED="1542712159908" TEXT="&#x52d5;&#x4f5c;&#x3059;&#x308b;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;&#x306f;&#x9ad8;&#x3044;&#x4fe1;&#x983c;&#x6027;&#x3092;&#x6301;&#x3063;&#x3066;&#x3044;&#x3066;&#x307b;&#x3057;&#x3044;"/>
<node CREATED="1542712161341" ID="ID_1089776093" MODIFIED="1542712318458" TEXT="&#x305d;&#x306e;&#x305f;&#x3081;&#x5f53;&#x7814;&#x7a76;&#x5ba4;&#x3067;&#x306f; CodeGear, DataGear &#x3068;&#x3044;&#x3046;&#x5358;&#x4f4d;&#x3092;&#x7528;&#x3044;&#x3066;&#x8a18;&#x8ff0;&#x3059;&#x308b;&#x624b;&#x6cd5;&#x3092;&#x63d0;&#x6848;&#x3057;&#x3066;&#x3044;&#x308b;"/>
<node CREATED="1542712325826" ID="ID_1328437172" MODIFIED="1542713353200" TEXT="&#x51e6;&#x7406;&#x306e;&#x5358;&#x4f4d;&#x3067;&#x3042;&#x308b; CodeGear &#x3092;&#x7d99;&#x7d9a;&#x3057;&#x3066;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30df;&#x30f3;&#x30b0;&#x3092;&#x3059;&#x308b;"/>
<node CREATED="1542713354500" ID="ID_1839316214" MODIFIED="1544604145156" TEXT="&#x3053;&#x306e;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30df;&#x30f3;&#x30b0;&#x30b9;&#x30bf;&#x30a4;&#x30eb;&#x306f;&#x3001;&#x95a2;&#x6570;&#x578b;&#x8a00;&#x8a9e;&#x306e;&#x7d99;&#x7d9a;&#x6e21;&#x3057;&#x306e;&#x8a18;&#x8ff0;&#x3068;&#x7b49;&#x4fa1;&#x3067;&#x3042;&#x308b;"/>
<node CREATED="1544602583680" ID="ID_1768414893" MODIFIED="1544604155058" TEXT="&#x7d99;&#x7d9a;&#x6e21;&#x3057;&#x306e;&#x8a18;&#x8ff0;&#x3068; HoareLogic &#x306f;&#x76f8;&#x6027;&#x826f;&#x304f;&#x8a18;&#x8ff0;&#x304c;&#x3067;&#x304d;&#x308b;&#x306e;&#x3067;&#x306f;&#x306a;&#x3044;&#x304b;&#x3068;&#x8003;&#x3048;&#x3066;&#x3044;&#x308b;"/>
<node CREATED="1544604130156" ID="ID_1466381113" MODIFIED="1544604233204" TEXT="&#x672c;&#x7814;&#x7a76;&#x3067;&#x306f; Agda &#x4e0a;&#x3067; &#x7d99;&#x7d9a;&#x6e21;&#x3057;&#x8a18;&#x8ff0;&#x3068; Hoare Logic &#x3092;&#x7528;&#x3044;&#x3066; SingleLinkedQueue &#x306b;&#x5bfe;&#x3057;&#x3066;&#x691c;&#x8a3c;&#x3092;&#x884c;&#x3063;&#x305f;(&#x884c;&#x3044;&#x305f;&#x3044;)"/>
</node>
<node CREATED="1542710849360" ID="ID_1011962353" MODIFIED="1542710855151" TEXT="&#x7814;&#x7a76;&#x6982;&#x8981;">
<node CREATED="1544604865596" ID="ID_778442777" MODIFIED="1544605176196" TEXT="&#x7d99;&#x7d9a;&#x6e21;&#x3057;&#x8a18;&#x8ff0;&#x3092;&#x3057;&#x305f; Agda &#x3067;&#x3001;Hoare Logic &#x3092;&#x7d44;&#x307f;&#x5408;&#x308f;&#x305b;&#x3066;&#x306e;&#x8a3c;&#x660e;&#x3092;&#x884c;&#x3046;"/>
<node CREATED="1544604886373" ID="ID_742333345" MODIFIED="1544605273294" TEXT="&#x901a;&#x5e38;&#x306f;&#x95a2;&#x6570;&#x3054;&#x3068;&#x306e;&#x691c;&#x8a3c;&#x304c;&#x53b3;&#x3057;&#x305d;&#x3046;">
<node CREATED="1544605273841" ID="ID_1047842205" MODIFIED="1544605304755" TEXT="HoareLogic &#x30d9;&#x30fc;&#x30b9;&#x3060;&#x3068;&#x305d;&#x308c;&#x305e;&#x308c;&#x306e;&#x95a2;&#x6570;&#x3054;&#x3068;&#x306b;&#x691c;&#x8a3c;&#x304c;&#x3067;&#x304d;&#x305d;&#x3046;">
<icon BUILTIN="forward"/>
</node>
</node>
</node>
<node CREATED="1544605418893" ID="ID_1631394138" MODIFIED="1544605424146" TEXT="GearsOS">
<node CREATED="1544605447524" ID="ID_1203956494" MODIFIED="1544605454361" TEXT="&#x6982;&#x8981;">
<node CREATED="1544605455331" ID="ID_1049429958" MODIFIED="1544605459641" TEXT="CbC"/>
<node CREATED="1544605471951" ID="ID_1170775991" MODIFIED="1544605484612" TEXT="&#x3071;&#x308b;&#x3059;&#x3055;&#x3093;&#x306e;&#x4fee;&#x8ad6;&#x3042;&#x305f;&#x308a;&#x304b;&#x3089;&#x62fe;&#x3063;&#x3066;&#x304f;&#x308b;"/>
</node>
</node>
<node CREATED="1542710861598" ID="ID_1569648968" MODIFIED="1544603739021" TEXT="Agda">
<node CREATED="1544603740555" ID="ID_1970865370" MODIFIED="1544603746306" TEXT="Agda &#x306b;&#x3064;&#x3044;&#x3066;">
<node CREATED="1544604331911" ID="ID_1316542521" MODIFIED="1544604340263" TEXT="Agda &#x3068;&#x306f;?"/>
<node CREATED="1544604340903" ID="ID_1025874674" MODIFIED="1544604470238" TEXT="Agda &#x306e;&#x30c7;&#x30fc;&#x30bf;&#x3001;&#x6587;&#x6cd5;&#x8a18;&#x8ff0;"/>
</node>
<node CREATED="1544603752778" ID="ID_1655285120" MODIFIED="1544604330094" TEXT="&#x691c;&#x8a3c;&#x306b;&#x95a2;&#x3059;&#x308b;&#x8a71;">
<node CREATED="1544604295278" ID="ID_1571024257" MODIFIED="1544604451101" TEXT="Curry Howard &#x3068;&#x304b;&#x66f8;&#x3044;&#x305f;&#x307b;&#x3046;&#x304c;&#x3044;&#x3044;?"/>
<node CREATED="1544604345175" ID="ID_1245079261" MODIFIED="1544604485703" TEXT="Agda &#x3067;&#x306e;&#x8a3c;&#x660e;"/>
</node>
<node CREATED="1542710855615" ID="ID_633104128" MODIFIED="1544605442284" TEXT="GearsOS&#x3068;Agda">
<node CREATED="1544603433154" ID="ID_1178446548" MODIFIED="1544603443456" TEXT="CbC &#x306b;&#x3064;&#x3044;&#x3066;"/>
<node CREATED="1544603444224" ID="ID_1582475028" MODIFIED="1544603454233" TEXT="CodeGear, DataGear"/>
<node CREATED="1544603454927" ID="ID_1017938996" MODIFIED="1544604274110" TEXT="Agda &#x3067;&#x306e; CodeGear, DataGear(&#x7d99;&#x7d9a;&#x6e21;&#x3057;&#x8a18;&#x8ff0;&#x306e;&#x8aac;&#x660e;&#x3082;)"/>
<node CREATED="1544604389725" ID="ID_1200091175" MODIFIED="1544604415749" TEXT="Agda &#x3067;&#x306e; CbC &#x306e;&#x691c;&#x8a3c;"/>
</node>
<node CREATED="1544955510685" ID="ID_1378359833" MODIFIED="1544955531798" TEXT="&#x7b49;&#x5f0f;&#x5909;&#x5f62;&#x306e;&#x8a3c;&#x660e;">
<node CREATED="1544955536030" ID="ID_1351263237" MODIFIED="1544955550375" TEXT="x==y &#x3092;&#x8a3c;&#x660e;&#x3057;&#x305f;&#x3044;"/>
<node CREATED="1544955552292" ID="ID_1396517005" MODIFIED="1544955578075" TEXT="Reasoning &#x3092; &#x4e09;&#x3064;&#x306e; ? &#x3067;&#x304b;&#x304f;"/>
<node CREATED="1544955585146" ID="ID_569206138" MODIFIED="1544955596370" TEXT="&#x4e8c;&#x3064;&#x76ee;&#x3092;&#x898b;&#x308b;&#x3068;&#x524d;&#x5f8c;&#x306b;&#x5fc5;&#x8981;&#x306a;&#x5f0f;&#x304c;&#x308f;&#x304b;&#x308b;"/>
<node CREATED="1544955597250" ID="ID_1715686699" MODIFIED="1544955611283" TEXT="&#x5909;&#x5f62;&#x3059;&#x308b;&#x5f0f;&#x3092;&#x7f85;&#x5217;&#x3059;&#x308b;"/>
<node CREATED="1544955612652" ID="ID_985696591" MODIFIED="1544955630412" TEXT="&#x5909;&#x5f62;&#x3059;&#x308b;&#x63a8;&#x8ad6;&#x898f;&#x5247;(x==x1)">
<node CREATED="1544955633523" ID="ID_1341233417" MODIFIED="1544955646711" TEXT="x1==y &#x3092;&#x8a3c;&#x660e;&#x3059;&#x308c;&#x3070;&#x826f;&#x3044;"/>
</node>
</node>
</node>
<node CREATED="1542710864438" ID="ID_1474492130" MODIFIED="1542710910000" TEXT="HoareLogic">
<node CREATED="1544952943134" ID="ID_10179037" MODIFIED="1544952949971" TEXT="While Program">
<node CREATED="1544952991409" ID="ID_596599032" MODIFIED="1544952997567" TEXT="Skip"/>
<node CREATED="1544952998071" ID="ID_1502092759" MODIFIED="1544953002143" TEXT="Abort"/>
<node CREATED="1544953002729" ID="ID_652512656" MODIFIED="1544953004935" TEXT="Seq"/>
<node CREATED="1544953005280" ID="ID_1999779347" MODIFIED="1544953009167" TEXT="PComm"/>
<node CREATED="1544953009656" ID="ID_143829516" MODIFIED="1544953010671" TEXT="If"/>
<node CREATED="1544953010967" ID="ID_1707380993" MODIFIED="1544953012496" TEXT="While"/>
</node>
<node CREATED="1544953033123" ID="ID_1125077236" MODIFIED="1544953048274" TEXT="PreCondition Command PostCondition">
<node CREATED="1544953059289" ID="ID_554375384" MODIFIED="1544953065212" TEXT="HTProof">
<node CREATED="1544953087539" ID="ID_500044924" MODIFIED="1544953091662" TEXT="SkipRule"/>
<node CREATED="1544953092210" ID="ID_1398126479" MODIFIED="1544953097342" TEXT="AbortRule"/>
<node CREATED="1544953097973" ID="ID_1347734292" MODIFIED="1544953100799" TEXT="SeqRule"/>
<node CREATED="1544953101143" ID="ID_810877387" MODIFIED="1544953114392" TEXT="PrimCommRule"/>
<node CREATED="1544953115159" ID="ID_1693437242" MODIFIED="1544953119888" TEXT="IfRule"/>
<node CREATED="1544953120428" ID="ID_403099872" MODIFIED="1544953122745" TEXT="WhileRule"/>
<node CREATED="1544953131201" ID="ID_1694881778" MODIFIED="1544953193197" TEXT="WeakningRule"/>
</node>
<node CREATED="1544953067155" ID="ID_991425650" MODIFIED="1544953077405" TEXT="Axiom "/>
<node CREATED="1544953078010" ID="ID_1967448460" MODIFIED="1544953082901" TEXT="Totology"/>
</node>
<node CREATED="1544953213492" ID="ID_1313761757" MODIFIED="1544953220280" TEXT="Example"/>
<node CREATED="1544954625664" ID="ID_856350466" MODIFIED="1544954638560" TEXT="&#x8a3c;&#x660e;&#x306e;&#x624b;&#x9806;">
<node CREATED="1544954639048" ID="ID_707405060" MODIFIED="1544954655114" TEXT="Program&#x306b;&#x6cbf;&#x3063;&#x3066;&#x30eb;&#x30fc;&#x30eb;&#x3092;&#x69cb;&#x7bc9;&#x3059;&#x308b;"/>
<node CREATED="1544954656137" ID="ID_1099647645" MODIFIED="1544954693892" TEXT="While Program &#x306b;&#x76f8;&#x4f3c;&#x306a;Program &#x306e;&#x69cb;&#x7bc9;&#x65b9;&#x6cd5;&#x306b;&#x306a;&#x308b;"/>
<node CREATED="1544954695449" ID="ID_167702231" MODIFIED="1544954726159" TEXT="&#x30eb;&#x30fc;&#x30eb;&#x306e; Axiom &#x90e8;&#x5206;&#x3092; ? &#x3068;&#x3059;&#x308b;&#x3068;&#x8a3c;&#x660e;&#x3059;&#x3079;&#x304d;&#x8ad6;&#x7406;&#x5f0f;&#x304c;&#x5f97;&#x3089;&#x308c;&#x308b;"/>
<node CREATED="1544954728375" ID="ID_733013199" MODIFIED="1544954791492" TEXT="&#x8a3c;&#x660e;&#x3092;&#x30e9;&#x30e0;&#x30c0;&#x3053;&#x3046;&#x3068;&#x3057;&#x3066;&#x69cb;&#x7bc9;&#x3059;&#x308b;"/>
<node CREATED="1544954794025" ID="ID_1862482735" MODIFIED="1544954833648" TEXT="Invaliant &#x306e;&#x3088;&#x3046;&#x306b; PostCondition &#x3068; PreCondition &#x304c;&#x5408;&#x308f;&#x306a;&#x3044;&#x5834;&#x5408;&#x306f;">
<node CREATED="1544954837647" ID="ID_605650861" MODIFIED="1544954853144" TEXT="WeakningRule&#x3092;&#x4f7f;&#x3046;"/>
</node>
<node CREATED="1544954861191" ID="ID_1632760763" MODIFIED="1544954884779" TEXT="&#x3059;&#x3079;&#x3066;&#x304c;&#x63a5;&#x7d9a;&#x3055;&#x308c;&#x308b;&#x3068;&#x8a3c;&#x660e;&#x304c;&#x7d42;&#x308f;&#x308b;"/>
<node CREATED="1544954887674" ID="ID_49477826" MODIFIED="1544954897316" TEXT="&#x505c;&#x6b62;&#x6027;&#x306f;&#x3053;&#x3053;&#x3067;&#x306f;&#x307e;&#x3060;&#x8a3c;&#x660e;&#x3057;&#x3066;&#x3044;&#x306a;&#x3044;">
<node CREATED="1544954900504" ID="ID_333078697" MODIFIED="1544954920046" TEXT="Agda &#x3067;&#x306f; TERMINATING &#x3068;&#x3044;&#x3046;&#x30a2;&#x30ce;&#x30c6;&#x30fc;&#x30b7;&#x30e7;&#x30f3;&#x3067;&#x6291;&#x5236;&#x3059;&#x308b;"/>
</node>
</node>
<node CREATED="1544603916933" ID="ID_912615419" MODIFIED="1544953262787" TEXT="CodeGear, DataGear">
<node CREATED="1544953301023" ID="ID_1936819038" MODIFIED="1544953341105" TEXT="add PreCondition to CodeGear Argument"/>
<node CREATED="1544953364369" ID="ID_1897331085" MODIFIED="1544953383252" TEXT="use Conversion CodeGear as a WeakningRule"/>
</node>
<node CREATED="1544953390779" ID="ID_1221989718" MODIFIED="1544953393861" TEXT="Example"/>
</node>
<node CREATED="1544953534749" ID="ID_757078127" MODIFIED="1544953544019" TEXT="&#x6bd4;&#x8f03;&#x3068;&#x8a55;&#x4fa1;">
<node CREATED="1544953548644" ID="ID_660804708" MODIFIED="1544953586327" TEXT="HoareLogic &#x306f; Program &#x306e;&#x69cb;&#x9020;&#x3068;&#x8a3c;&#x660e;&#x304c;&#x5225;"/>
<node CREATED="1544953593558" ID="ID_1222836750" MODIFIED="1544953605696" TEXT="&#x505c;&#x6b62;&#x6027;&#x306f;&#x307e;&#x3060;&#x672a;&#x5b9f;&#x88c5;"/>
<node CREATED="1544953607664" ID="ID_1418415681" MODIFIED="1544953624184" TEXT="CodeGear">
<node CREATED="1544953624446" ID="ID_1333500913" MODIFIED="1544953647627" TEXT="Program &#x3068;&#x8a3c;&#x660e;&#x304c;&#x5bfe;&#x5fdc;&#x3057;&#x3066;&#x308b;"/>
<node CREATED="1544953649212" ID="ID_1043705676" MODIFIED="1544953685286" TEXT="while Program &#x3068;&#x9055;&#x3063;&#x3066;CodeGear&#x306e;&#x8a18;&#x8ff0;&#x304c;&#x81ea;&#x7531;"/>
<node CREATED="1544953687507" ID="ID_213969675" MODIFIED="1544953714064" TEXT="&#x8a3c;&#x660e;&#x304c;&#x30e1;&#x30bf;&#x8a08;&#x7b97;&#x306e;&#x5165;&#x529b;&#x3068;&#x51fa;&#x529b;&#x306b;&#x5bfe;&#x5fdc;&#x3059;&#x308b;"/>
<node CREATED="1544953717022" ID="ID_960276791" MODIFIED="1544953734255" TEXT="&#x5165;&#x529b;&#x304c;PreCondition &#x3067;"/>
<node CREATED="1544953736673" ID="ID_13390002" MODIFIED="1544953757401" TEXT="&#x7d99;&#x7d9a;&#x306e;&#x547c;&#x3073;&#x51fa;&#x3057;&#x304c; PostCondition &#x306b;&#x306a;&#x308b;"/>
</node>
<node CREATED="1544953777092" ID="ID_1972622252" MODIFIED="1544953797711" TEXT="CodeGear&#x3067;HoareLogic &#x3092;&#x7c21;&#x6f54;&#x306b;&#x8a18;&#x8ff0;&#x3067;&#x304d;&#x308b;&#x3053;&#x3068;&#x304c;&#x308f;&#x304b;&#x3063;&#x305f;"/>
</node>
<node CREATED="1544953399717" ID="ID_1659003334" MODIFIED="1544953407985" TEXT="&#x5c06;&#x6765;&#x306e;&#x8ab2;&#x984c;">
<node CREATED="1544953411825" ID="ID_1766627105" MODIFIED="1544953435986" TEXT="HoareLogic &#x90e8;&#x5206;&#x3092;&#x30e1;&#x30bf;&#x8a08;&#x7b97;&#x3068;&#x3057;&#x3066;&#x8a18;&#x8ff0;"/>
<node CREATED="1544953456250" ID="ID_37105044" MODIFIED="1544953464613" TEXT="&#x5143;&#x306e;&#x8a08;&#x7b97;&#x306e;&#x8a18;&#x8ff0;&#x3092;&#x4fdd;&#x5b58;&#x3059;&#x308b;"/>
<node CREATED="1544953465598" ID="ID_454238122" MODIFIED="1544953488516" TEXT="RedBlackTree"/>
<node CREATED="1544953489813" ID="ID_286112576" MODIFIED="1544953506149" TEXT="Synchronized Queue">
<node CREATED="1544953803400" ID="ID_1363325581" MODIFIED="1544953823216" TEXT="&#x4e26;&#x5217;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;&#x3092;&#x72b6;&#x614b;&#x9077;&#x79fb;&#x306b;&#x5909;&#x63db;&#x3059;&#x308b;"/>
<node CREATED="1544953824288" ID="ID_649570454" MODIFIED="1544953862724" TEXT="Temporal Logic &#x306a;&#x30d7;&#x30ed;&#x30d1;&#x30c6;&#x30a3;&#x3092;&#x72b6;&#x614b;&#x9077;&#x79fb;&#x3068;&#x3057;&#x3066;&#x8a18;&#x8ff0;&#x3059;&#x308b;"/>
<node CREATED="1544953864581" ID="ID_1141579119" MODIFIED="1544953928385" TEXT="Omega Automaton &#x306e;&#x53d7;&#x7406;&#x6761;&#x4ef6;&#x3068;&#x3057;&#x3066;&#x8a3c;&#x660e;&#x3059;&#x308b;"/>
</node>
<node CREATED="1544953525955" ID="ID_796699968" MODIFIED="1544953529433" TEXT="GearsOS"/>
</node>
<node CREATED="1544952979891" ID="ID_1616071429" MODIFIED="1544952986481" TEXT="&#x307e;&#x3068;&#x3081;"/>
</node>
<node CREATED="1542710960435" ID="ID_167048397" MODIFIED="1542710984521" POSITION="right" TEXT="&#x7814;&#x7a76;"/>
<node CREATED="1545030891993" ID="ID_424599902" MODIFIED="1545030897348" POSITION="left" TEXT="&#x7814;&#x7a76;&#x76ee;&#x7684;">
<node CREATED="1545031695286" ID="ID_1807380852" MODIFIED="1545031828376" TEXT="OS &#x3084;&#x30a2;&#x30d7;&#x30ea;&#x30b1;&#x30fc;&#x30b7;&#x30e7;&#x30f3;&#x306e;&#x4fe1;&#x983c;&#x6027;&#x3092;&#x3042;&#x3052;&#x305f;&#x3044;"/>
<node CREATED="1545031829304" ID="ID_848338957" MODIFIED="1545031877618" TEXT="&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;&#x81ea;&#x4f53;&#x306e;&#x30d0;&#x30b0;&#x304c;&#x306a;&#x3044;&#x3053;&#x3068;&#x304c;&#x91cd;&#x8981;"/>
<node CREATED="1545031881555" ID="ID_1890176001" MODIFIED="1545031901586" TEXT="&#x5927;&#x534a;&#x306e;&#x30d0;&#x30b0;&#x306f;&#x7c21;&#x5358;&#x306a;&#x3082;&#x306e;&#x3067;&#x3042;&#x308b;"/>
<node CREATED="1545031915332" ID="ID_1766422576" MODIFIED="1545031926012" TEXT="&#x672c;&#x6765;&#x306a;&#x3089;&#x5f53;&#x305f;&#x308a;&#x524d;&#x306b;&#x898b;&#x3064;&#x304b;&#x308b;&#x30a8;&#x30e9;&#x30fc;&#x3092;&#x7c21;&#x5358;&#x306b;&#x898b;&#x3064;&#x3051;&#x305f;&#x3044;"/>
<node CREATED="1545031934733" ID="ID_819406039" MODIFIED="1545031952333" TEXT="&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;&#x306e;&#x8a3c;&#x660e;&#x306b;&#x306f; HoareLogic &#x304c;&#x5b58;&#x5728;&#x3059;&#x308b;"/>
<node CREATED="1545031953430" ID="ID_189897321" MODIFIED="1545031992503" TEXT="&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30df;&#x30f3;&#x30b0;&#x306e;&#x65b9;&#x6cd5;&#x8ad6;&#x81ea;&#x4f53;&#x306b; HoareLogic &#x3092;&#x7d44;&#x307f;&#x8fbc;&#x3080;&#x30a2;&#x30d7;&#x30ed;&#x30fc;&#x30c1;"/>
<node CREATED="1545031995576" ID="ID_455588060" MODIFIED="1545032022728" TEXT="&#x305d;&#x306e;&#x305f;&#x3081;&#x306b;&#x306f;&#x65e2;&#x5b58;&#x306e;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30df;&#x30f3;&#x30b0;&#x8a00;&#x8a9e;&#x3067;&#x306f;&#x30c0;&#x30e1;&#x306a;&#x306e;&#x304b;&#x3082;&#x3057;&#x308c;&#x306a;&#x3044;"/>
<node CREATED="1545032024743" ID="ID_862300550" MODIFIED="1545032052066" TEXT="HoareLogic &#x304c;&#x5e83;&#x307e;&#x3089;&#x306a;&#x3044;&#x7406;&#x7531;">
<node CREATED="1545032068115" ID="ID_1062003354" MODIFIED="1545032100996" TEXT="&#x65e2;&#x5b58;&#x306e;&#x8a00;&#x8a9e;&#x306b;&#x306f; HoareLogic &#x3092;&#x66f8;&#x304f;&#x5834;&#x6240;&#x304c;&#x306a;&#x3044;"/>
<node CREATED="1545032104901" ID="ID_298160802" MODIFIED="1545032113668" TEXT="&#x4e0d;&#x5f53;&#x306b;&#x96e3;&#x3057;&#x3044;&#x3068;&#x601d;&#x308f;&#x308c;&#x3066;&#x3044;&#x308b;">
<node CREATED="1545032129477" ID="ID_952723861" MODIFIED="1545032134998" TEXT="&#x683c;&#x8abf;&#x9ad8;&#x3044;"/>
</node>
</node>
<node CREATED="1545032140487" ID="ID_1131641415" MODIFIED="1545032158255" TEXT="&#x7c21;&#x5358;&#x306a;&#x30a8;&#x30e9;&#x30fc;&#x3092;&#x898b;&#x3064;&#x3051;&#x308b;&#x305f;&#x3081;&#x306e;&#x8a3c;&#x660e;&#x304c;&#x96e3;&#x3057;&#x3044;&#x306f;&#x305a;&#x306f;&#x306a;&#x3044;"/>
<node CREATED="1545032159792" ID="ID_1116096354" MODIFIED="1545032164071" TEXT="&#x7c21;&#x5358;&#x306a;&#x3082;&#x306e;&#x304b;&#x3089;&#x59cb;&#x3081;&#x308b;"/>
<node CREATED="1545032299337" ID="ID_1249663292" MODIFIED="1545032321657" TEXT="Gears &#x306f; HoareLogic &#x3068;&#x306e;&#x76f8;&#x6027;&#x304c;&#x826f;&#x3044;&#x3088;&#x3046;&#x306b;&#x8a2d;&#x8a08;&#x3055;&#x308c;&#x305f;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30df;&#x30f3;&#x30b0;&#x8a00;&#x8a9e;&#x306b;&#x306a;&#x3063;&#x3066;&#x3044;&#x308b;"/>
<node CREATED="1545032436351" ID="ID_1535666009" MODIFIED="1545032467432" TEXT="WhileProgram &#x3068;&#x540c;&#x3058;&#x5f62;&#x3067; Gears &#x3067;&#x8a3c;&#x660e;&#x304c;&#x3067;&#x304d;&#x308b;"/>
</node>
<node CREATED="1545030901019" ID="ID_901428450" MODIFIED="1545030905483" POSITION="left" TEXT="&#x8ad6;&#x6587;&#x306e;&#x6d41;&#x308c;">
<node CREATED="1545031348434" ID="ID_685170876" MODIFIED="1545031357009" TEXT="&#x73fe;&#x72b6;">
<node CREATED="1545031359867" ID="ID_1180031106" MODIFIED="1545031386298" TEXT="kernel &#x306e;&#x691c;&#x8a3c;&#x4f8b;">
<node CREATED="1545031393090" ID="ID_410307657" MODIFIED="1545031412419" TEXT="C&#x306b;&#x3088;&#x308b;&#x5b9f;&#x88c5;&#x3068;&#x95a2;&#x6570;&#x578b;&#x8a00;&#x8a9e;&#x306e;&#x8a18;&#x8ff0;&#x3068;&#x8a3c;&#x660e;&#x3092;&#x884c;&#x3046;"/>
</node>
<node CREATED="1545031418116" ID="ID_536836987" MODIFIED="1545031432052" TEXT="&#x4f4e;&#x30ec;&#x30d9;&#x30eb;&#x8a18;&#x8ff0;&#x5411;&#x3051;&#x306e;&#x95a2;&#x6570;&#x578b;&#x8a00;&#x8a9e;">
<node CREATED="1545031433208" ID="ID_1290789880" MODIFIED="1545031441435" TEXT="ATS"/>
<node CREATED="1545031442323" ID="ID_894719933" MODIFIED="1545031444003" TEXT="Rust"/>
<node CREATED="1545031555795" ID="ID_813031602" MODIFIED="1545031611781" TEXT="&#x8a3c;&#x660e;&#x3092;&#x884c;&#x3046;&#x3060;&#x3051;&#x306e;&#x578b;&#x30b7;&#x30b9;&#x30c6;&#x30e0;&#x306f;&#x6301;&#x3063;&#x3066;&#x306a;&#x3044;"/>
</node>
<node CREATED="1545031472093" ID="ID_942826330" MODIFIED="1545031482407" TEXT="&#x8a3c;&#x660e;&#x652f;&#x63f4;&#x5411;&#x3051;&#x306e;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30df;&#x30f3;&#x30b0;&#x8a00;&#x8a9e;">
<node CREATED="1545031484349" ID="ID_24675818" MODIFIED="1545031491533" TEXT="Agda"/>
<node CREATED="1545031492670" ID="ID_54745078" MODIFIED="1545031494677" TEXT="Coq"/>
<node CREATED="1545031496988" ID="ID_1790735065" MODIFIED="1545031505366" TEXT="Issabella"/>
<node CREATED="1545031511911" ID="ID_1140265385" MODIFIED="1545031517464" TEXT="&#x5b9f;&#x884c;&#x306b;&#x306f;&#x5411;&#x304b;&#x306a;&#x3044;"/>
</node>
<node CREATED="1545031663383" ID="ID_1834440802" MODIFIED="1545031679864" TEXT="&#x8a3c;&#x660e;&#x306e;&#x8a18;&#x8ff0;&#x3068;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;&#x306e;&#x8a18;&#x8ff0;&#x304c;&#x5225;&#x3005;&#x306a;&#x306e;&#x304c;&#x554f;&#x984c;&#x3067;&#x306f;&#x306a;&#x3044;&#x304b;"/>
</node>
<node CREATED="1545031099382" ID="ID_1202631621" MODIFIED="1545031110989" TEXT="Agda &#x306e;&#x6982;&#x8981;">
<node CREATED="1545031122593" ID="ID_1888101637" MODIFIED="1545031128590" TEXT="&#x7b49;&#x5f0f;&#x5909;&#x5f62;"/>
<node CREATED="1545031131170" ID="ID_759945081" MODIFIED="1545031133318" TEXT="&#xff1f;"/>
</node>
<node CREATED="1545031223230" ID="ID_1271382711" MODIFIED="1545031233635" TEXT="Gears &#x306e;&#x6982;&#x8981;">
<node CREATED="1545031240448" ID="ID_1246355278" MODIFIED="1545031248659" TEXT="CbC &#x306e;&#x5b9f;&#x88c5;"/>
<node CREATED="1545031249811" ID="ID_1433130177" MODIFIED="1545031258084" TEXT="Agda &#x306b;&#x3088;&#x308b; Gears &#x306e;&#x8a18;&#x8ff0;"/>
</node>
<node CREATED="1545031141237" ID="ID_906133157" MODIFIED="1545031146348" TEXT="While Progarm"/>
<node CREATED="1545031153481" ID="ID_434127663" MODIFIED="1545031168863" TEXT="WhileProgram &#x306e; Agda &#x306b;&#x3088;&#x308b;&#x8a3c;&#x660e;"/>
<node CREATED="1545031170853" ID="ID_1197992113" MODIFIED="1545031185689" TEXT="Gears &#x306b;&#x3088;&#x308b;&#x4f8b;&#x984c;"/>
<node CREATED="1545031186560" ID="ID_1521714484" MODIFIED="1545031200105" TEXT="Gears &#x306b;&#x304a;&#x3051;&#x308b; HoareLogic &#x306e;&#x8a3c;&#x660e;"/>
</node>
<node CREATED="1545030910084" ID="ID_372949892" MODIFIED="1545030913012" POSITION="left" TEXT="&#x7d50;&#x679c;">
<node CREATED="1545030966535" ID="ID_1338356672" MODIFIED="1545030996904" TEXT="Agda &#x3067; WhileProgram &#x306e; HoareLogic &#x306b;&#x3088;&#x308b;&#x8a3c;&#x660e;&#x3092;&#x4f5c;&#x3063;&#x305f;"/>
<node CREATED="1545030999516" ID="ID_35075799" MODIFIED="1545031016585" TEXT="Gears &#x3067;&#x306e; HoareLogic &#x306e;&#x8a18;&#x8ff0;&#x3092;&#x3057;&#x305f;"/>
<node CREATED="1545031027240" ID="ID_981326333" MODIFIED="1545031044786" TEXT="&#x8a3c;&#x660e;&#x3068;&#x30d7;&#x30ed;&#x30b0;&#x30e9;&#x30e0;&#x306e;&#x8a18;&#x8ff0;&#x3092;&#x4e00;&#x4f53;&#x5316;&#x3057;&#x3066;&#x8a18;&#x8ff0;&#x3067;&#x304d;&#x305f;"/>
<node CREATED="1545031065628" ID="ID_457628232" MODIFIED="1545031085235" TEXT="&#x8a3c;&#x660e;&#x3092;&#x30e1;&#x30bf;&#x8a08;&#x7b97;&#x306e;&#x5f15;&#x6570;&#x306e;&#x53d7;&#x3051;&#x6e21;&#x3057;&#x3068;&#x3057;&#x3066;&#x8a18;&#x8ff0;&#x3067;&#x304d;&#x305f;"/>
</node>
</node>
</map>