Mercurial > hg > Papers > 2020 > ryokka-master

view ryokka-master.mm @ 8:b8ff2bd1a5af

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix hoare.tex
author ryokka
date Thu, 06 Feb 2020 21:49:08 +0900
parents 196ba119ca89
children
line wrap: on
line source

<map version="1.1.0">
<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
<node CREATED="1577179229340" ID="ID_1981253136" MODIFIED="1580210143896">
<richcontent TYPE="NODE"><html>
  <head>
    
  </head>
  <body>
    <p>
      Continuation based C &#12391;&#12398;
    </p>
    <p>
      HoareLogic &#12434;&#29992;&#12356;&#12383;&#20181;&#27096;&#35352;&#36848;&#12392;&#26908;&#35388;
    </p>
  </body>
</html></richcontent>
<font NAME="SansSerif" SIZE="14"/>
<node CREATED="1577179287926" ID="ID_1165984884" MODIFIED="1579169646928" POSITION="right" TEXT="&#x306f;&#x3058;&#x3081;&#x306b;">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577179299434" ID="ID_372153190" MODIFIED="1579169646928" POSITION="right" TEXT="Continuation based C">
<font NAME="SansSerif" SIZE="14"/>
<node CREATED="1577179793073" ID="ID_1307352612" MODIFIED="1579169646928" TEXT="CodeGear">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577179805065" ID="ID_1214581036" MODIFIED="1579169646928" TEXT="DataGear">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577179939889" ID="ID_1188251116" MODIFIED="1579169646928" TEXT="Meta CodeGear,DataGear">
<font NAME="SansSerif" SIZE="14"/>
</node>
</node>
<node CREATED="1577179329845" ID="ID_1008088180" MODIFIED="1579169646927" POSITION="right" TEXT="Agda">
<font NAME="SansSerif" SIZE="14"/>
<node CREATED="1577182682220" ID="ID_1522532015" MODIFIED="1579169646927" TEXT="&#x5165;&#x9580;">
<font NAME="SansSerif" SIZE="14"/>
</node>
</node>
<node CREATED="1577179349458" ID="ID_739318439" MODIFIED="1579169646927" POSITION="right" TEXT="Hoare Logic">
<font NAME="SansSerif" SIZE="14"/>
<node CREATED="1578999031670" ID="ID_517062300" MODIFIED="1579169646927" TEXT="&#x5165;&#x9580;">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577179370109" ID="ID_809388614" MODIFIED="1579169646927" TEXT="whileTest (Hoare Logic &#x306e;&#x4f8b;)">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577179360283" FOLDED="true" ID="ID_501247037" MODIFIED="1580733240320" TEXT="Agda &#x3068; Hoare Logic">
<font NAME="SansSerif" SIZE="14"/>
<node CREATED="1577179441565" ID="ID_1388092541" MODIFIED="1579169646927" TEXT="&#x8a18;&#x8ff0;">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577179468054" ID="ID_545191696" MODIFIED="1579169646926" TEXT="Soundness &#x95a2;&#x9023;">
<font NAME="SansSerif" SIZE="14"/>
</node>
</node>
</node>
<node CREATED="1580733258780" ID="ID_309485478" MODIFIED="1580733267818" POSITION="right" TEXT="Continuation based C &#x3068; Agda">
<node CREATED="1580733268446" ID="ID_1382286556" MODIFIED="1580733276190" TEXT="Agda &#x3068; CbC &#x306e;&#x5bfe;&#x5fdc;"/>
<node CREATED="1580733278420" ID="ID_1658404824" MODIFIED="1580733301471" TEXT="CbC &#x306e;&#x30e1;&#x30bf;&#x8a08;&#x7b97;&#x3068; Agda">
<node CREATED="1580733301709" ID="ID_914616090" MODIFIED="1580733331759" TEXT="Agda &#x306f; CbC &#x306e;&#x4e0a;&#x4f4d;&#x8a00;&#x8a9e;&#x306e;&#x4e00;&#x3064;&#x3068;&#x3057;&#x3066;&#x4f7f;&#x308f;&#x308c;&#x305d;&#x3046;..."/>
</node>
</node>
<node CREATED="1577179318540" ID="ID_402362033" MODIFIED="1579169646926" POSITION="right" TEXT="Continuation based C &#x3068; HoareLogic">
<font NAME="SansSerif" SIZE="14"/>
<node CREATED="1580733080230" ID="ID_1644923722" MODIFIED="1580733118392" TEXT="Hoare Logic &#x3068; CbC &#x306e;&#x5bfe;&#x5fdc;">
<node CREATED="1580733118792" ID="ID_415990499" MODIFIED="1580733144465" TEXT="Command &#x305f;&#x3061;(&#x3068;&#x3044;&#x3046;&#x304b; HTProof &#x306e;&#x6982;&#x5f62;&#xff1f;)"/>
</node>
<node CREATED="1577182741707" ID="ID_1751180005" MODIFIED="1580733188604" TEXT="Hoare Logic &#x30d9;&#x30fc;&#x30b9;&#x306e;&#x691c;&#x8a3c;">
<font NAME="SansSerif" SIZE="14"/>
<node CREATED="1580733190923" ID="ID_1861833651" MODIFIED="1580733195484" TEXT="while Test &#x306e;&#x4f8b;"/>
</node>
</node>
<node CREATED="1577179295267" ID="ID_747054126" MODIFIED="1579169646925" POSITION="right" TEXT="&#x307e;&#x3068;&#x3081;">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577179315283" ID="ID_1375073128" MODIFIED="1579169646925" POSITION="left" TEXT="Gears OS">
<font NAME="SansSerif" SIZE="14"/>
<node CREATED="1577179820187" ID="ID_519165935" MODIFIED="1579169646925" TEXT="-interface">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577179862592" ID="ID_1991286966" MODIFIED="1579169646925" TEXT="Gears OS &#x306e;&#x691c;&#x8a3c;">
<font NAME="SansSerif" SIZE="14"/>
</node>
</node>
<node CREATED="1577179492520" ID="ID_1327764636" MODIFIED="1579169646912" POSITION="left" TEXT="&#x3067;&#x304d;&#x305f;&#x3089;&#x3044;&#x3044;&#x306a;(Binary-Tree)">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577182694546" ID="ID_764943519" MODIFIED="1579169646926" POSITION="left" TEXT="BinaryTree &#x3068; RedBlack Tree(Agda)">
<font NAME="SansSerif" SIZE="14"/>
<node CREATED="1577182754406" ID="ID_1200857877" MODIFIED="1579169646926" TEXT="HoareLogic">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577182712718" ID="ID_283296995" MODIFIED="1579169646926" TEXT="BinaryTree &#x306e; &#x6761;&#x4ef6;&#x3064;&#x304d;&#x306e;&#x3084;&#x3064;&#x306e;&#x8a71;">
<font NAME="SansSerif" SIZE="14"/>
</node>
<node CREATED="1577182765996" ID="ID_740598781" MODIFIED="1579169646926" TEXT="RedBlackTree">
<font NAME="SansSerif" SIZE="14"/>
</node>
</node>
<node CREATED="1580721326343" ID="ID_1512980116" MODIFIED="1580721341151" POSITION="left" TEXT="Agda &#x3068; CbC &#x306e;&#x5bfe;&#x5fdc;&#x306b;&#x3064;&#x3044;&#x3066;">
<node CREATED="1580721373542" ID="ID_1954543280" MODIFIED="1580721383972" TEXT="CbC">
<node CREATED="1580721384201" ID="ID_115992653" MODIFIED="1580733814782" TEXT="&#x5f53;&#x7814;&#x7a76;&#x5ba4;&#x3067;&#x958b;&#x767a;&#x3057;&#x3066;&#x308b;">
<icon BUILTIN="full-1"/>
</node>
<node CREATED="1580721396170" ID="ID_499703619" MODIFIED="1580733823040" TEXT="C&#x306e;&#x4e0b;&#x4f4d;&#x8a00;&#x8a9e;">
<icon BUILTIN="full-2"/>
</node>
<node CREATED="1580721408290" ID="ID_998450693" MODIFIED="1580733826688" TEXT="&#x7d99;&#x7d9a;&#x3092;&#x30d9;&#x30fc;&#x30b9;&#x3068;&#x3057;&#x305f;&#x8a00;&#x8a9e;">
<icon BUILTIN="full-3"/>
</node>
<node CREATED="1580733361534" ID="ID_533829353" MODIFIED="1580733828942" TEXT="&#x30e1;&#x30bf;&#x30ec;&#x30d9;&#x30eb;&#x306e;&#x8a08;&#x7b97;&#x3092;&#x5206;&#x96e2;&#x3057;&#x3066;&#x3044;&#x308b;">
<icon BUILTIN="full-4"/>
</node>
</node>
<node CREATED="1580721461991" ID="ID_591117015" MODIFIED="1580721463942" TEXT="Agda">
<node CREATED="1580733533448" ID="ID_769096207" MODIFIED="1580733929041" TEXT="&#x4eca;&#x66f8;&#x3044;&#x3066;&#x308b;&#x3084;&#x3064;">
<node CREATED="1580721464218" ID="ID_21769693" MODIFIED="1580733816784" TEXT="&#x5b9a;&#x7406;&#x8a3c;&#x660e;&#x652f;&#x63f4;&#x7cfb;&#x8a00;&#x8a9e;">
<icon BUILTIN="full-1"/>
</node>
<node CREATED="1580721533881" ID="ID_1399874964" MODIFIED="1580733831368" TEXT="CbC &#x306e;&#x4e0a;&#x4f4d;&#x8a00;&#x8a9e;">
<icon BUILTIN="full-2"/>
</node>
<node CREATED="1580721541271" ID="ID_947618755" MODIFIED="1580733833446" TEXT="CPS &#x3067;&#x672b;&#x5c3e;&#x518d;&#x5e30;&#x306e;&#x5f62;&#x306b;&#x3059;&#x308b;&#x3068; CbC &#x3068;&#x5bfe;&#x5fdc;">
<icon BUILTIN="full-3"/>
</node>
<node CREATED="1580733406249" ID="ID_366137551" MODIFIED="1580733836038" TEXT="CbC &#x304b;&#x3089;&#x898b;&#x308b;&#x3068; &#x30ce;&#x30fc;&#x30de;&#x30eb;&#x3068;&#x30e1;&#x30bf;&#x30ec;&#x30d9;&#x30eb;&#x304c;&#x4e00;&#x7dd2;">
<icon BUILTIN="full-4"/>
<node CREATED="1580733453908" ID="ID_798759509" MODIFIED="1580733676720" TEXT="(&#x691c;&#x8a3c;&#x4ee5;&#x5916;&#x306e;&#x30e1;&#x30bf;&#x8a08;&#x7b97;&#x304c;&#x884c;&#x3048;&#x306a;&#x3044;)"/>
</node>
</node>
<node CREATED="1580733547354" ID="ID_1244670000" MODIFIED="1580733554106" TEXT="&#x3042;&#x3063;&#x3068;&#x3093;&#x3055;&#x3093;&#x304c;&#x66f8;&#x3044;&#x305f;&#x3084;&#x3064;">
<node CREATED="1580733555545" ID="ID_1619441901" MODIFIED="1580733819409" TEXT="Agda &#x4e0a;&#x3067;&#x306e; CbC &#x8a00;&#x8a9e;&#x5b9f;&#x88c5;&#x307f;&#x305f;&#x3044;&#x306a;&#x306e;">
<icon BUILTIN="full-1"/>
</node>
<node CREATED="1580733573052" ID="ID_1738251390" MODIFIED="1580733838805" TEXT="CbC &#x306e;&#x8a18;&#x8ff0;&#x3068;&#x7b49;&#x4fa1;(&#x306e;&#x306f;&#x305a;)">
<icon BUILTIN="full-2"/>
</node>
<node CREATED="1580733594205" ID="ID_1706512006" MODIFIED="1580733842123" TEXT="goto &#x3060;&#x3063;&#x305f;&#x308a; metagoto &#x307f;&#x305f;&#x3044;&#x306a;&#x306e;&#x4f7f;&#x3063;&#x3066;&#x66f8;&#x304f;">
<icon BUILTIN="full-3"/>
</node>
<node CREATED="1580733640095" ID="ID_464738583" MODIFIED="1580733844698" TEXT="&#x4e0a;&#x3068;&#x540c;&#x69d8;&#x306b;&#x540c;&#x4e00;&#x8996;&#x3067;&#x304d;&#x308b;">
<icon BUILTIN="full-4"/>
<node CREATED="1580733704500" ID="ID_1089033110" MODIFIED="1580733756379" TEXT="Agda &#x4e0a;&#x306e; CbC &#x5b9f;&#x88c5;&#x306a;&#x306e;&#x3067;&#x4e00;&#x5fdc;&#x4ed6;&#x306e;&#x8a08;&#x7b97;&#x3082;&#x5b9f;&#x88c5;&#x3059;&#x308c;&#x3070;&#x884c;&#x3051;&#x308b;&#x2026;&#xff1f;"/>
<node CREATED="1580733757793" ID="ID_352478839" MODIFIED="1580733785660" TEXT="&#x305f;&#x3060;&#x3057;&#x73fe;&#x6642;&#x70b9;&#x3067; Hoare  Logic &#x30d9;&#x30fc;&#x30b9;&#x3067;&#x8a3c;&#x660e;&#x3067;&#x304d;&#x308b;&#x304b;&#x304c;&#x308f;&#x304b;&#x3089;&#x306a;&#x3044;"/>
</node>
</node>
</node>
</node>
</node>
</map>