|
0
|
1 <map version="freeplane 1.9.13">
|
|
|
2 <!--To view this file, download free mind mapping software Freeplane from https://www.freeplane.org -->
|
|
|
3 <node TEXT="rbtree-gearsagda" FOLDED="false" ID="ID_452131666" CREATED="1610381621610" MODIFIED="1681354145545" STYLE="oval">
|
|
|
4 <font SIZE="18"/>
|
|
|
5 <hook NAME="MapStyle" zoom="0.75">
|
|
|
6 <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"/>
|
|
|
7
|
|
|
8 <map_styles>
|
|
|
9 <stylenode LOCALIZED_TEXT="styles.root_node" STYLE="oval" UNIFORM_SHAPE="true" VGAP_QUANTITY="24 pt">
|
|
|
10 <font SIZE="24"/>
|
|
|
11 <stylenode LOCALIZED_TEXT="styles.predefined" POSITION="right" STYLE="bubble">
|
|
|
12 <stylenode LOCALIZED_TEXT="default" ID="ID_207122690" COLOR="#000000" STYLE="fork">
|
|
|
13 <arrowlink SHAPE="CUBIC_CURVE" COLOR="#000000" WIDTH="2" TRANSPARENCY="200" DASH="" FONT_SIZE="9" FONT_FAMILY="SansSerif" DESTINATION="ID_207122690" STARTARROW="NONE" ENDARROW="DEFAULT"/>
|
|
|
14 <font NAME="SansSerif" SIZE="10" BOLD="false" ITALIC="false"/>
|
|
|
15 <richcontent CONTENT-TYPE="plain/auto" TYPE="DETAILS"/>
|
|
|
16 <richcontent TYPE="NOTE" CONTENT-TYPE="plain/auto"/>
|
|
|
17 </stylenode>
|
|
|
18 <stylenode LOCALIZED_TEXT="defaultstyle.details"/>
|
|
|
19 <stylenode LOCALIZED_TEXT="defaultstyle.attributes">
|
|
|
20 <font SIZE="9"/>
|
|
|
21 </stylenode>
|
|
|
22 <stylenode LOCALIZED_TEXT="defaultstyle.note" COLOR="#000000" BACKGROUND_COLOR="#ffffff" TEXT_ALIGN="LEFT"/>
|
|
|
23 <stylenode LOCALIZED_TEXT="defaultstyle.floating">
|
|
|
24 <edge STYLE="hide_edge"/>
|
|
|
25 <cloud COLOR="#f0f0f0" SHAPE="ROUND_RECT"/>
|
|
|
26 </stylenode>
|
|
|
27 <stylenode LOCALIZED_TEXT="defaultstyle.selection" BACKGROUND_COLOR="#afd3f7" BORDER_COLOR_LIKE_EDGE="false" BORDER_COLOR="#afd3f7"/>
|
|
|
28 </stylenode>
|
|
|
29 <stylenode LOCALIZED_TEXT="styles.user-defined" POSITION="right" STYLE="bubble">
|
|
|
30 <stylenode LOCALIZED_TEXT="styles.topic" COLOR="#18898b" STYLE="fork">
|
|
|
31 <font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
|
|
|
32 </stylenode>
|
|
|
33 <stylenode LOCALIZED_TEXT="styles.subtopic" COLOR="#cc3300" STYLE="fork">
|
|
|
34 <font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
|
|
|
35 </stylenode>
|
|
|
36 <stylenode LOCALIZED_TEXT="styles.subsubtopic" COLOR="#669900">
|
|
|
37 <font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
|
|
|
38 </stylenode>
|
|
|
39 <stylenode LOCALIZED_TEXT="styles.important" ID="ID_3752836">
|
|
|
40 <icon BUILTIN="yes"/>
|
|
|
41 <arrowlink COLOR="#003399" TRANSPARENCY="255" DESTINATION="ID_3752836"/>
|
|
|
42 </stylenode>
|
|
|
43 </stylenode>
|
|
|
44 <stylenode LOCALIZED_TEXT="styles.AutomaticLayout" POSITION="right" STYLE="bubble">
|
|
|
45 <stylenode LOCALIZED_TEXT="AutomaticLayout.level.root" COLOR="#000000" STYLE="oval" SHAPE_HORIZONTAL_MARGIN="10 pt" SHAPE_VERTICAL_MARGIN="10 pt">
|
|
|
46 <font SIZE="18"/>
|
|
|
47 </stylenode>
|
|
|
48 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,1" COLOR="#0033ff">
|
|
|
49 <font SIZE="16"/>
|
|
|
50 </stylenode>
|
|
|
51 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,2" COLOR="#00b439">
|
|
|
52 <font SIZE="14"/>
|
|
|
53 </stylenode>
|
|
|
54 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,3" COLOR="#990000">
|
|
|
55 <font SIZE="12"/>
|
|
|
56 </stylenode>
|
|
|
57 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,4" COLOR="#111111">
|
|
|
58 <font SIZE="10"/>
|
|
|
59 </stylenode>
|
|
|
60 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,5"/>
|
|
|
61 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,6"/>
|
|
|
62 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,7"/>
|
|
|
63 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,8"/>
|
|
|
64 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,9"/>
|
|
|
65 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,10"/>
|
|
|
66 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,11"/>
|
|
|
67 </stylenode>
|
|
|
68 </stylenode>
|
|
|
69 </map_styles>
|
|
|
70 </hook>
|
|
|
71 <node TEXT="GearAgdanによるRed Black Tree の検証" POSITION="right" ID="ID_1707429913" CREATED="1681354146375" MODIFIED="1681354149504"/>
|
|
|
72 <node TEXT="Gears OS" POSITION="left" ID="ID_1627768067" CREATED="1681370097231" MODIFIED="1681370135147">
|
|
|
73 <node TEXT="Continuation based C" ID="ID_886365419" CREATED="1681370135452" MODIFIED="1681370144727"/>
|
|
|
74 <node TEXT="CodeGear and DataGear" ID="ID_1505619678" CREATED="1681370145576" MODIFIED="1681370169360"/>
|
|
|
75 <node TEXT="GearsAgda" ID="ID_1483093782" CREATED="1681370170247" MODIFIED="1681370174624"/>
|
|
|
76 <node TEXT="lightweigt continuation" ID="ID_709373441" CREATED="1681370232271" MODIFIED="1681370241482"/>
|
|
|
77 </node>
|
|
|
78 <node TEXT="meta computation" POSITION="left" ID="ID_587222105" CREATED="1681370246638" MODIFIED="1681370255183">
|
|
|
79 <node TEXT="IO" ID="ID_939386664" CREATED="1681370255664" MODIFIED="1681370261532"/>
|
|
|
80 <node TEXT="Hoare Logic" ID="ID_468705414" CREATED="1681370262977" MODIFIED="1681370270967"/>
|
|
|
81 </node>
|
|
|
82 <node TEXT="meata computation in GearsAgda" POSITION="left" ID="ID_1679966111" CREATED="1681370285647" MODIFIED="1681370300383">
|
|
|
83 <node TEXT="Gears Form" ID="ID_562028595" CREATED="1681370303175" MODIFIED="1681370328863"/>
|
|
|
84 <node TEXT="Meta computation" ID="ID_532649685" CREATED="1681370334319" MODIFIED="1681370340118"/>
|
|
|
85 <node TEXT="Segment" ID="ID_1391622726" CREATED="1681370342818" MODIFIED="1681370346242"/>
|
|
|
86 <node TEXT="stub" ID="ID_1481524131" CREATED="1681370347413" MODIFIED="1681370350369"/>
|
|
|
87 <node TEXT="CodeGear table" ID="ID_528079968" CREATED="1681370352629" MODIFIED="1681370366378"/>
|
|
|
88 </node>
|
|
|
89 <node TEXT="Hoare Logic" POSITION="left" ID="ID_590542814" CREATED="1681370375413" MODIFIED="1681370379970">
|
|
|
90 <node TEXT="command base" ID="ID_1041738747" CREATED="1681370380249" MODIFIED="1681370383059"/>
|
|
|
91 <node TEXT="first order" ID="ID_1511997811" CREATED="1681370399684" MODIFIED="1681370403829"/>
|
|
|
92 <node TEXT="soundness" ID="ID_783227970" CREATED="1681370407410" MODIFIED="1681370413286">
|
|
|
93 <node TEXT="separated from program" ID="ID_549960702" CREATED="1681370413548" MODIFIED="1681370423487"/>
|
|
|
94 </node>
|
|
|
95 <node TEXT="no proof support" ID="ID_94897053" CREATED="1681370433921" MODIFIED="1681370438778"/>
|
|
|
96 </node>
|
|
|
97 <node TEXT="GearsAgda" POSITION="left" ID="ID_613685836" CREATED="1681370441463" MODIFIED="1681370446502">
|
|
|
98 <node TEXT="written in Agda" ID="ID_883451142" CREATED="1681370450642" MODIFIED="1681370456415">
|
|
|
99 <node TEXT="proof assistance" ID="ID_567095247" CREATED="1681370456760" MODIFIED="1681370462431"/>
|
|
|
100 </node>
|
|
|
101 <node TEXT="any lightweight continuation form" ID="ID_512231980" CREATED="1681370472049" MODIFIED="1681370490394"/>
|
|
|
102 <node TEXT="close to basic unit in a compiler" ID="ID_1639405885" CREATED="1681370493600" MODIFIED="1681370507300"/>
|
|
|
103 <node TEXT="concurrency" ID="ID_1969768669" CREATED="1681370510538" MODIFIED="1681370522360"/>
|
|
|
104 <node TEXT="meta computation" ID="ID_1341787488" CREATED="1681370523208" MODIFIED="1681370528202">
|
|
|
105 <node TEXT="Hoare Logic style" ID="ID_1596917933" CREATED="1681370535368" MODIFIED="1681370546348"/>
|
|
|
106 <node TEXT="with invariant" ID="ID_1946393368" CREATED="1681370547204" MODIFIED="1681370553272"/>
|
|
|
107 </node>
|
|
|
108 <node TEXT="data with proofs" ID="ID_1144050858" CREATED="1681370596859" MODIFIED="1681370601940">
|
|
|
109 <node TEXT="invariant" ID="ID_375933480" CREATED="1681370605320" MODIFIED="1681370610877"/>
|
|
|
110 <node TEXT="much simpler" ID="ID_245103686" CREATED="1681370613781" MODIFIED="1681370622639"/>
|
|
|
111 </node>
|
|
|
112 </node>
|
|
|
113 <node TEXT="concurrency" POSITION="right" ID="ID_1659998734" CREATED="1681370628915" MODIFIED="1681370636745">
|
|
|
114 <node TEXT="codeGear-wise concurency" ID="ID_1216124303" CREATED="1681370637291" MODIFIED="1681370656059"/>
|
|
|
115 <node TEXT="assuming finite computation in a codeGear" ID="ID_573537896" CREATED="1681370657029" MODIFIED="1681370677168"/>
|
|
|
116 <node TEXT="scheduler" ID="ID_327350914" CREATED="1681370679365" MODIFIED="1681370685685">
|
|
|
117 <node TEXT="in meta computation" ID="ID_1272612921" CREATED="1681370686271" MODIFIED="1681370693104"/>
|
|
|
118 <node TEXT="code table" ID="ID_1779321838" CREATED="1681370741527" MODIFIED="1681370746964">
|
|
|
119 <node TEXT="all codeGear" ID="ID_1073597539" CREATED="1681370747218" MODIFIED="1681370752548"/>
|
|
|
120 <node TEXT="numbered" ID="ID_1618653220" CREATED="1681370753308" MODIFIED="1681370756196"/>
|
|
|
121 <node TEXT="stub" ID="ID_573578192" CREATED="1681370756935" MODIFIED="1681370759362"/>
|
|
|
122 </node>
|
|
|
123 <node TEXT="Context" ID="ID_1995851564" CREATED="1681370693516" MODIFIED="1681370697602">
|
|
|
124 <node TEXT="current code" ID="ID_1885258842" CREATED="1681370728219" MODIFIED="1681370732220"/>
|
|
|
125 <node TEXT="all dataGear" ID="ID_1859577487" CREATED="1681370733587" MODIFIED="1681370739913"/>
|
|
|
126 </node>
|
|
|
127 <node TEXT="communication" ID="ID_387799092" CREATED="1681370705533" MODIFIED="1681370712647"/>
|
|
|
128 </node>
|
|
|
129 <node TEXT="model checking" ID="ID_1191776209" CREATED="1681370766180" MODIFIED="1681370771240"/>
|
|
|
130 <node TEXT="proofs on concurrenct" ID="ID_1117350246" CREATED="1681370771658" MODIFIED="1681370781273"/>
|
|
|
131 </node>
|
|
|
132 <node TEXT="while program" POSITION="right" ID="ID_710382637" CREATED="1681370805471" MODIFIED="1681370811890"/>
|
|
|
133 <node TEXT="binary tree" POSITION="right" ID="ID_1922786513" CREATED="1681370796432" MODIFIED="1681370804204">
|
|
|
134 <node TEXT="stack invariant" ID="ID_1448419661" CREATED="1681370821482" MODIFIED="1681370830261"/>
|
|
|
135 <node TEXT="tree invariant" ID="ID_243832132" CREATED="1681370830768" MODIFIED="1681370835246"/>
|
|
|
136 <node TEXT="replace invariant" ID="ID_1303870466" CREATED="1681370835840" MODIFIED="1681370840736"/>
|
|
|
137 </node>
|
|
|
138 <node TEXT="red black tree" POSITION="right" ID="ID_263237724" CREATED="1681370787198" MODIFIED="1681370792658">
|
|
|
139 <node TEXT="red and black" ID="ID_385223552" CREATED="1681370848145" MODIFIED="1681370856270"/>
|
|
|
140 <node TEXT="parent and grand parent" ID="ID_517970079" CREATED="1681370857076" MODIFIED="1681370866920">
|
|
|
141 <node TEXT="in stack" ID="ID_901165358" CREATED="1681370867215" MODIFIED="1681370872234"/>
|
|
|
142 </node>
|
|
|
143 <node TEXT="concurrency" ID="ID_23246060" CREATED="1681370878663" MODIFIED="1681370883733">
|
|
|
144 <node TEXT="root replacement" ID="ID_184711355" CREATED="1681370884231" MODIFIED="1681370892725">
|
|
|
145 <node TEXT="transaction" ID="ID_1256246418" CREATED="1681370893169" MODIFIED="1681370898372"/>
|
|
|
146 </node>
|
|
|
147 <node TEXT="non destructive" ID="ID_1377710910" CREATED="1681370903423" MODIFIED="1681370909214">
|
|
|
148 <node TEXT="read sharing" ID="ID_1853077777" CREATED="1681370910265" MODIFIED="1681370917627"/>
|
|
|
149 </node>
|
|
|
150 </node>
|
|
|
151 </node>
|
|
|
152 <node TEXT="complied code" POSITION="right" ID="ID_1551916219" CREATED="1681370926034" MODIFIED="1681370931197">
|
|
|
153 <node TEXT="gearsAgda → CbC conversion" ID="ID_159756131" CREATED="1681370931496" MODIFIED="1681370953438"/>
|
|
|
154 <node TEXT="combine multiple codeGear" ID="ID_1952851358" CREATED="1681371036240" MODIFIED="1681371047551">
|
|
|
155 <node TEXT="optimization" ID="ID_256515995" CREATED="1681371048689" MODIFIED="1681371053081"/>
|
|
|
156 </node>
|
|
|
157 </node>
|
|
|
158 <node TEXT="is this reliable?" POSITION="right" ID="ID_189224322" CREATED="1681370969828" MODIFIED="1681370979059">
|
|
|
159 <node TEXT="with proofs" ID="ID_114174861" CREATED="1681370979357" MODIFIED="1681370985340">
|
|
|
160 <node TEXT="relative to the theory" ID="ID_194349290" CREATED="1681370985587" MODIFIED="1681371003316"/>
|
|
|
161 </node>
|
|
|
162 <node TEXT="invariant gives all property" ID="ID_955091732" CREATED="1681371007176" MODIFIED="1681371020551"/>
|
|
|
163 </node>
|
|
|
164 <node TEXT="is this scale?" POSITION="right" ID="ID_1442547192" CREATED="1681371022394" MODIFIED="1681371028550">
|
|
|
165 <node TEXT="size of invariant" ID="ID_66636375" CREATED="1681470579922" MODIFIED="1681470584136"/>
|
|
|
166 <node TEXT="polynominal of cases of invariant" ID="ID_1431513531" CREATED="1681470584691" MODIFIED="1681470597800"/>
|
|
|
167 <node TEXT="not all combination is possible" ID="ID_1626555105" CREATED="1681470604805" MODIFIED="1681470612527"/>
|
|
|
168 <node TEXT="we don't need to fill all the proof" ID="ID_1601614737" CREATED="1681470615256" MODIFIED="1681470627377">
|
|
|
169 <node TEXT="incremental" ID="ID_1230800920" CREATED="1681470627899" MODIFIED="1681470630690"/>
|
|
|
170 <node TEXT="partial" ID="ID_649982266" CREATED="1681470631099" MODIFIED="1681470634557"/>
|
|
|
171 </node>
|
|
|
172 </node>
|
|
|
173 <node TEXT="contents" POSITION="right" ID="ID_1884614552" CREATED="1681470012072" MODIFIED="1681470018912">
|
|
|
174 <node TEXT="verified red black tree" ID="ID_72137676" CREATED="1681470019151" MODIFIED="1681470047634"/>
|
|
|
175 <node TEXT="importance" ID="ID_510340227" CREATED="1681470049510" MODIFIED="1681470056562">
|
|
|
176 <node TEXT="conversion to classical form" ID="ID_312471113" CREATED="1681470523375" MODIFIED="1681470532568">
|
|
|
177 <node TEXT="destructive" ID="ID_1083852390" CREATED="1681470532868" MODIFIED="1681470536236"/>
|
|
|
178 <node TEXT="B-tree" ID="ID_1942790971" CREATED="1681470545925" MODIFIED="1681470551384"/>
|
|
|
179 </node>
|
|
|
180 <node TEXT="sequencial" ID="ID_783108258" CREATED="1681470056922" MODIFIED="1681470064048"/>
|
|
|
181 <node TEXT="concurrent" ID="ID_924506929" CREATED="1681470065130" MODIFIED="1681470068278"/>
|
|
|
182 </node>
|
|
|
183 <node TEXT="GearsAgda" ID="ID_1614171466" CREATED="1681470071381" MODIFIED="1681470074368">
|
|
|
184 <node TEXT="lightweight contination" ID="ID_351064745" CREATED="1681470074675" MODIFIED="1681470097157"/>
|
|
|
185 <node TEXT="CbC" ID="ID_280197854" CREATED="1681470108615" MODIFIED="1681470110151"/>
|
|
|
186 </node>
|
|
|
187 <node TEXT="classical approach" ID="ID_439782904" CREATED="1681470111745" MODIFIED="1681470120213">
|
|
|
188 <node TEXT="Hoare Logic" ID="ID_182843234" CREATED="1681470120549" MODIFIED="1681470123261"/>
|
|
|
189 <node TEXT="conversion to Haskell" ID="ID_18215857" CREATED="1681470123809" MODIFIED="1681470131336"/>
|
|
|
190 <node TEXT="verified but ..." ID="ID_86587986" CREATED="1681470188224" MODIFIED="1681470199159"/>
|
|
|
191 </node>
|
|
|
192 <node TEXT="GearsAgda" ID="ID_1624783880" CREATED="1681470180677" MODIFIED="1681470219506">
|
|
|
193 <node TEXT="invariant" ID="ID_1822140966" CREATED="1681470228788" MODIFIED="1681470232318">
|
|
|
194 <node TEXT="denotational semantics" ID="ID_1070066378" CREATED="1681470408330" MODIFIED="1681470415583"/>
|
|
|
195 </node>
|
|
|
196 <node TEXT="agda introduction" ID="ID_1367482138" CREATED="1681470219860" MODIFIED="1681470227830"/>
|
|
|
197 <node TEXT="simple while loop" ID="ID_594789165" CREATED="1681470293741" MODIFIED="1681470299458"/>
|
|
|
198 <node TEXT="loop connector" ID="ID_351381557" CREATED="1681470305517" MODIFIED="1681470311087">
|
|
|
199 <node TEXT="reduction parameter" ID="ID_1854148894" CREATED="1681470317762" MODIFIED="1681470324065"/>
|
|
|
200 </node>
|
|
|
201 </node>
|
|
|
202 <node TEXT="binary tree" ID="ID_1045767712" CREATED="1681470238269" MODIFIED="1681470245777">
|
|
|
203 <node TEXT="invariant" ID="ID_753395200" CREATED="1681470246095" MODIFIED="1681470248201">
|
|
|
204 <node TEXT="tree" ID="ID_1179203442" CREATED="1681470248688" MODIFIED="1681470254441"/>
|
|
|
205 <node TEXT="stack" ID="ID_743804922" CREATED="1681470255070" MODIFIED="1681470256626"/>
|
|
|
206 <node TEXT="replace" ID="ID_1919439558" CREATED="1681470257216" MODIFIED="1681470260232"/>
|
|
|
207 </node>
|
|
|
208 <node TEXT="program guidance" ID="ID_1331715304" CREATED="1681470429863" MODIFIED="1681470434889">
|
|
|
209 <node TEXT="differential of invariant" ID="ID_1547779379" CREATED="1681470435636" MODIFIED="1681470444235"/>
|
|
|
210 </node>
|
|
|
211 </node>
|
|
|
212 <node TEXT="red black tree" ID="ID_233668516" CREATED="1681470263078" MODIFIED="1681470266745"/>
|
|
|
213 <node TEXT="concurrency" ID="ID_1836297821" CREATED="1681470271427" MODIFIED="1681470275872">
|
|
|
214 <node TEXT="segmented" ID="ID_290000164" CREATED="1681470276209" MODIFIED="1681470282080"/>
|
|
|
215 <node TEXT="code table" ID="ID_278977606" CREATED="1681470350363" MODIFIED="1681470354017"/>
|
|
|
216 <node TEXT="scheduler" ID="ID_111624804" CREATED="1681470354785" MODIFIED="1681470364123">
|
|
|
217 <node TEXT="fairness" ID="ID_1334406786" CREATED="1681470365738" MODIFIED="1681470368781"/>
|
|
|
218 </node>
|
|
|
219 <node TEXT="temporal logic" ID="ID_1823540844" CREATED="1681470371933" MODIFIED="1681470376053"/>
|
|
|
220 </node>
|
|
|
221 <node TEXT="execution" ID="ID_95297285" CREATED="1681470455878" MODIFIED="1681470458355">
|
|
|
222 <node TEXT="data gear with proof is executable" ID="ID_1369250602" CREATED="1681470459700" MODIFIED="1681470472621"/>
|
|
|
223 <node TEXT="need not to fill the proof" ID="ID_1356375326" CREATED="1681470474612" MODIFIED="1681470483972"/>
|
|
|
224 </node>
|
|
|
225 <node TEXT="scalability" ID="ID_1468980711" CREATED="1681470382482" MODIFIED="1681470389280">
|
|
|
226 <node TEXT="invariant library" ID="ID_1421089406" CREATED="1681470391295" MODIFIED="1681470395791"/>
|
|
|
227 </node>
|
|
|
228 </node>
|
|
|
229 </node>
|
|
|
230 </map>
|
