|
0
|
1 <map version="1.1.0">
|
|
|
2 <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
|
|
4
|
3 <node CREATED="1577179229340" ID="ID_1981253136" MODIFIED="1580210143896">
|
|
1
|
4 <richcontent TYPE="NODE"><html>
|
|
|
5 <head>
|
|
|
6
|
|
|
7 </head>
|
|
|
8 <body>
|
|
|
9 <p>
|
|
|
10 Continuation based C での
|
|
|
11 </p>
|
|
|
12 <p>
|
|
4
|
13 HoareLogic を用いた仕様記述と検証
|
|
1
|
14 </p>
|
|
|
15 </body>
|
|
|
16 </html></richcontent>
|
|
|
17 <font NAME="SansSerif" SIZE="14"/>
|
|
|
18 <node CREATED="1577179287926" ID="ID_1165984884" MODIFIED="1579169646928" POSITION="right" TEXT="はじめに">
|
|
|
19 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
20 </node>
|
|
1
|
21 <node CREATED="1577179299434" ID="ID_372153190" MODIFIED="1579169646928" POSITION="right" TEXT="Continuation based C">
|
|
|
22 <font NAME="SansSerif" SIZE="14"/>
|
|
|
23 <node CREATED="1577179793073" ID="ID_1307352612" MODIFIED="1579169646928" TEXT="CodeGear">
|
|
|
24 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
25 </node>
|
|
1
|
26 <node CREATED="1577179805065" ID="ID_1214581036" MODIFIED="1579169646928" TEXT="DataGear">
|
|
|
27 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
28 </node>
|
|
1
|
29 <node CREATED="1577179939889" ID="ID_1188251116" MODIFIED="1579169646928" TEXT="Meta CodeGear,DataGear">
|
|
|
30 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
31 </node>
|
|
|
32 </node>
|
|
1
|
33 <node CREATED="1577179329845" ID="ID_1008088180" MODIFIED="1579169646927" POSITION="right" TEXT="Agda">
|
|
|
34 <font NAME="SansSerif" SIZE="14"/>
|
|
|
35 <node CREATED="1577182682220" ID="ID_1522532015" MODIFIED="1579169646927" TEXT="入門">
|
|
|
36 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
37 </node>
|
|
|
38 </node>
|
|
1
|
39 <node CREATED="1577179349458" ID="ID_739318439" MODIFIED="1579169646927" POSITION="right" TEXT="Hoare Logic">
|
|
|
40 <font NAME="SansSerif" SIZE="14"/>
|
|
|
41 <node CREATED="1578999031670" ID="ID_517062300" MODIFIED="1579169646927" TEXT="入門">
|
|
|
42 <font NAME="SansSerif" SIZE="14"/>
|
|
|
43 </node>
|
|
|
44 <node CREATED="1577179370109" ID="ID_809388614" MODIFIED="1579169646927" TEXT="whileTest (Hoare Logic の例)">
|
|
|
45 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
46 </node>
|
|
5
|
47 <node CREATED="1577179360283" FOLDED="true" ID="ID_501247037" MODIFIED="1580733240320" TEXT="Agda と Hoare Logic">
|
|
1
|
48 <font NAME="SansSerif" SIZE="14"/>
|
|
|
49 <node CREATED="1577179441565" ID="ID_1388092541" MODIFIED="1579169646927" TEXT="記述">
|
|
|
50 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
51 </node>
|
|
1
|
52 <node CREATED="1577179468054" ID="ID_545191696" MODIFIED="1579169646926" TEXT="Soundness 関連">
|
|
|
53 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
54 </node>
|
|
|
55 </node>
|
|
|
56 </node>
|
|
5
|
57 <node CREATED="1580733258780" ID="ID_309485478" MODIFIED="1580733267818" POSITION="right" TEXT="Continuation based C と Agda">
|
|
|
58 <node CREATED="1580733268446" ID="ID_1382286556" MODIFIED="1580733276190" TEXT="Agda と CbC の対応"/>
|
|
|
59 <node CREATED="1580733278420" ID="ID_1658404824" MODIFIED="1580733301471" TEXT="CbC のメタ計算と Agda">
|
|
|
60 <node CREATED="1580733301709" ID="ID_914616090" MODIFIED="1580733331759" TEXT="Agda は CbC の上位言語の一つとして使われそう..."/>
|
|
0
|
61 </node>
|
|
|
62 </node>
|
|
5
|
63 <node CREATED="1577179318540" ID="ID_402362033" MODIFIED="1579169646926" POSITION="right" TEXT="Continuation based C と HoareLogic">
|
|
1
|
64 <font NAME="SansSerif" SIZE="14"/>
|
|
5
|
65 <node CREATED="1580733080230" ID="ID_1644923722" MODIFIED="1580733118392" TEXT="Hoare Logic と CbC の対応">
|
|
|
66 <node CREATED="1580733118792" ID="ID_415990499" MODIFIED="1580733144465" TEXT="Command たち(というか HTProof の概形？)"/>
|
|
0
|
67 </node>
|
|
5
|
68 <node CREATED="1577182741707" ID="ID_1751180005" MODIFIED="1580733188604" TEXT="Hoare Logic ベースの検証">
|
|
1
|
69 <font NAME="SansSerif" SIZE="14"/>
|
|
5
|
70 <node CREATED="1580733190923" ID="ID_1861833651" MODIFIED="1580733195484" TEXT="while Test の例"/>
|
|
0
|
71 </node>
|
|
|
72 </node>
|
|
1
|
73 <node CREATED="1577179295267" ID="ID_747054126" MODIFIED="1579169646925" POSITION="right" TEXT="まとめ">
|
|
|
74 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
75 </node>
|
|
1
|
76 <node CREATED="1577179315283" ID="ID_1375073128" MODIFIED="1579169646925" POSITION="left" TEXT="Gears OS">
|
|
|
77 <font NAME="SansSerif" SIZE="14"/>
|
|
|
78 <node CREATED="1577179820187" ID="ID_519165935" MODIFIED="1579169646925" TEXT="-interface">
|
|
|
79 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
80 </node>
|
|
1
|
81 <node CREATED="1577179862592" ID="ID_1991286966" MODIFIED="1579169646925" TEXT="Gears OS の検証">
|
|
|
82 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
83 </node>
|
|
|
84 </node>
|
|
1
|
85 <node CREATED="1577179492520" ID="ID_1327764636" MODIFIED="1579169646912" POSITION="left" TEXT="できたらいいな(Binary-Tree)">
|
|
|
86 <font NAME="SansSerif" SIZE="14"/>
|
|
0
|
87 </node>
|
|
5
|
88 <node CREATED="1577182694546" ID="ID_764943519" MODIFIED="1579169646926" POSITION="left" TEXT="BinaryTree と RedBlack Tree(Agda)">
|
|
|
89 <font NAME="SansSerif" SIZE="14"/>
|
|
|
90 <node CREATED="1577182754406" ID="ID_1200857877" MODIFIED="1579169646926" TEXT="HoareLogic">
|
|
|
91 <font NAME="SansSerif" SIZE="14"/>
|
|
|
92 </node>
|
|
|
93 <node CREATED="1577182712718" ID="ID_283296995" MODIFIED="1579169646926" TEXT="BinaryTree の 条件つきのやつの話">
|
|
|
94 <font NAME="SansSerif" SIZE="14"/>
|
|
|
95 </node>
|
|
|
96 <node CREATED="1577182765996" ID="ID_740598781" MODIFIED="1579169646926" TEXT="RedBlackTree">
|
|
|
97 <font NAME="SansSerif" SIZE="14"/>
|
|
|
98 </node>
|
|
|
99 </node>
|
|
|
100 <node CREATED="1580721326343" ID="ID_1512980116" MODIFIED="1580721341151" POSITION="left" TEXT="Agda と CbC の対応について">
|
|
|
101 <node CREATED="1580721373542" ID="ID_1954543280" MODIFIED="1580721383972" TEXT="CbC">
|
|
|
102 <node CREATED="1580721384201" ID="ID_115992653" MODIFIED="1580733814782" TEXT="当研究室で開発してる">
|
|
|
103 <icon BUILTIN="full-1"/>
|
|
|
104 </node>
|
|
|
105 <node CREATED="1580721396170" ID="ID_499703619" MODIFIED="1580733823040" TEXT="Cの下位言語">
|
|
|
106 <icon BUILTIN="full-2"/>
|
|
|
107 </node>
|
|
|
108 <node CREATED="1580721408290" ID="ID_998450693" MODIFIED="1580733826688" TEXT="継続をベースとした言語">
|
|
|
109 <icon BUILTIN="full-3"/>
|
|
|
110 </node>
|
|
|
111 <node CREATED="1580733361534" ID="ID_533829353" MODIFIED="1580733828942" TEXT="メタレベルの計算を分離している">
|
|
|
112 <icon BUILTIN="full-4"/>
|
|
|
113 </node>
|
|
|
114 </node>
|
|
|
115 <node CREATED="1580721461991" ID="ID_591117015" MODIFIED="1580721463942" TEXT="Agda">
|
|
|
116 <node CREATED="1580733533448" ID="ID_769096207" MODIFIED="1580733929041" TEXT="今書いてるやつ">
|
|
|
117 <node CREATED="1580721464218" ID="ID_21769693" MODIFIED="1580733816784" TEXT="定理証明支援系言語">
|
|
|
118 <icon BUILTIN="full-1"/>
|
|
|
119 </node>
|
|
|
120 <node CREATED="1580721533881" ID="ID_1399874964" MODIFIED="1580733831368" TEXT="CbC の上位言語">
|
|
|
121 <icon BUILTIN="full-2"/>
|
|
|
122 </node>
|
|
|
123 <node CREATED="1580721541271" ID="ID_947618755" MODIFIED="1580733833446" TEXT="CPS で末尾再帰の形にすると CbC と対応">
|
|
|
124 <icon BUILTIN="full-3"/>
|
|
|
125 </node>
|
|
|
126 <node CREATED="1580733406249" ID="ID_366137551" MODIFIED="1580733836038" TEXT="CbC から見ると ノーマルとメタレベルが一緒">
|
|
|
127 <icon BUILTIN="full-4"/>
|
|
|
128 <node CREATED="1580733453908" ID="ID_798759509" MODIFIED="1580733676720" TEXT="(検証以外のメタ計算が行えない)"/>
|
|
|
129 </node>
|
|
|
130 </node>
|
|
|
131 <node CREATED="1580733547354" ID="ID_1244670000" MODIFIED="1580733554106" TEXT="あっとんさんが書いたやつ">
|
|
|
132 <node CREATED="1580733555545" ID="ID_1619441901" MODIFIED="1580733819409" TEXT="Agda 上での CbC 言語実装みたいなの">
|
|
|
133 <icon BUILTIN="full-1"/>
|
|
|
134 </node>
|
|
|
135 <node CREATED="1580733573052" ID="ID_1738251390" MODIFIED="1580733838805" TEXT="CbC の記述と等価(のはず)">
|
|
|
136 <icon BUILTIN="full-2"/>
|
|
|
137 </node>
|
|
|
138 <node CREATED="1580733594205" ID="ID_1706512006" MODIFIED="1580733842123" TEXT="goto だったり metagoto みたいなの使って書く">
|
|
|
139 <icon BUILTIN="full-3"/>
|
|
|
140 </node>
|
|
|
141 <node CREATED="1580733640095" ID="ID_464738583" MODIFIED="1580733844698" TEXT="上と同様に同一視できる">
|
|
|
142 <icon BUILTIN="full-4"/>
|
|
|
143 <node CREATED="1580733704500" ID="ID_1089033110" MODIFIED="1580733756379" TEXT="Agda 上の CbC 実装なので一応他の計算も実装すれば行ける…？"/>
|
|
|
144 <node CREATED="1580733757793" ID="ID_352478839" MODIFIED="1580733785660" TEXT="ただし現時点で Hoare Logic ベースで証明できるかがわからない"/>
|
|
|
145 </node>
|
|
|
146 </node>
|
|
|
147 </node>
|
|
|
148 </node>
|
|
0
|
149 </node>
|
|
|
150 </map>
|
