|
0
|
1 <map version="freeplane 1.8.0">
|
|
|
2 <!--To view this file, download free mind mapping software Freeplane from http://freeplane.sourceforge.net -->
|
|
|
3 <node TEXT="GearsOSのAPI" FOLDED="false" ID="ID_1391122564" CREATED="1607406106629" MODIFIED="1607406119323" STYLE="oval">
|
|
|
4 <font SIZE="18"/>
|
|
|
5 <hook NAME="MapStyle">
|
|
|
6 <properties edgeColorConfiguration="#808080ff,#ff0000ff,#0000ffff,#00ff00ff,#ff00ffff,#00ffffff,#7c0000ff,#00007cff,#007c00ff,#7c007cff,#007c7cff,#7c7c00ff" fit_to_viewport="false"/>
|
|
|
7
|
|
|
8 <map_styles>
|
|
|
9 <stylenode LOCALIZED_TEXT="styles.root_node" STYLE="oval" UNIFORM_SHAPE="true" VGAP_QUANTITY="24.0 pt">
|
|
|
10 <font SIZE="24"/>
|
|
|
11 <stylenode LOCALIZED_TEXT="styles.predefined" POSITION="right" STYLE="bubble">
|
|
|
12 <stylenode LOCALIZED_TEXT="default" ICON_SIZE="12.0 pt" COLOR="#000000" STYLE="fork">
|
|
|
13 <font NAME="SansSerif" SIZE="10" BOLD="false" ITALIC="false"/>
|
|
|
14 </stylenode>
|
|
|
15 <stylenode LOCALIZED_TEXT="defaultstyle.details"/>
|
|
|
16 <stylenode LOCALIZED_TEXT="defaultstyle.attributes">
|
|
|
17 <font SIZE="9"/>
|
|
|
18 </stylenode>
|
|
|
19 <stylenode LOCALIZED_TEXT="defaultstyle.note" COLOR="#000000" BACKGROUND_COLOR="#ffffff" TEXT_ALIGN="LEFT"/>
|
|
|
20 <stylenode LOCALIZED_TEXT="defaultstyle.floating">
|
|
|
21 <edge STYLE="hide_edge"/>
|
|
|
22 <cloud COLOR="#f0f0f0" SHAPE="ROUND_RECT"/>
|
|
|
23 </stylenode>
|
|
|
24 </stylenode>
|
|
|
25 <stylenode LOCALIZED_TEXT="styles.user-defined" POSITION="right" STYLE="bubble">
|
|
|
26 <stylenode LOCALIZED_TEXT="styles.topic" COLOR="#18898b" STYLE="fork">
|
|
|
27 <font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
|
|
|
28 </stylenode>
|
|
|
29 <stylenode LOCALIZED_TEXT="styles.subtopic" COLOR="#cc3300" STYLE="fork">
|
|
|
30 <font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
|
|
|
31 </stylenode>
|
|
|
32 <stylenode LOCALIZED_TEXT="styles.subsubtopic" COLOR="#669900">
|
|
|
33 <font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
|
|
|
34 </stylenode>
|
|
|
35 <stylenode LOCALIZED_TEXT="styles.important">
|
|
|
36 <icon BUILTIN="yes"/>
|
|
|
37 </stylenode>
|
|
|
38 </stylenode>
|
|
|
39 <stylenode LOCALIZED_TEXT="styles.AutomaticLayout" POSITION="right" STYLE="bubble">
|
|
|
40 <stylenode LOCALIZED_TEXT="AutomaticLayout.level.root" COLOR="#000000" STYLE="oval" SHAPE_HORIZONTAL_MARGIN="10.0 pt" SHAPE_VERTICAL_MARGIN="10.0 pt">
|
|
|
41 <font SIZE="18"/>
|
|
|
42 </stylenode>
|
|
|
43 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,1" COLOR="#0033ff">
|
|
|
44 <font SIZE="16"/>
|
|
|
45 </stylenode>
|
|
|
46 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,2" COLOR="#00b439">
|
|
|
47 <font SIZE="14"/>
|
|
|
48 </stylenode>
|
|
|
49 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,3" COLOR="#990000">
|
|
|
50 <font SIZE="12"/>
|
|
|
51 </stylenode>
|
|
|
52 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,4" COLOR="#111111">
|
|
|
53 <font SIZE="10"/>
|
|
|
54 </stylenode>
|
|
|
55 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,5"/>
|
|
|
56 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,6"/>
|
|
|
57 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,7"/>
|
|
|
58 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,8"/>
|
|
|
59 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,9"/>
|
|
|
60 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,10"/>
|
|
|
61 <stylenode LOCALIZED_TEXT="AutomaticLayout.level,11"/>
|
|
|
62 </stylenode>
|
|
|
63 </stylenode>
|
|
|
64 </map_styles>
|
|
|
65 </hook>
|
|
|
66 <hook NAME="AutomaticEdgeColor" COUNTER="5" RULE="ON_BRANCH_CREATION"/>
|
|
|
67 <node TEXT="プログラムの信頼性を保証するのは難しい" POSITION="right" ID="ID_182717011" CREATED="1607406127549" MODIFIED="1607409819862">
|
|
|
68 <edge COLOR="#ff0000"/>
|
|
|
69 <node TEXT="テストプログラムで全ては証明できない" ID="ID_1642945466" CREATED="1607406143787" MODIFIED="1607409818771"/>
|
|
|
70 <node TEXT="証明でアプローチしたい" ID="ID_328449335" CREATED="1607409771301" MODIFIED="1607409837716">
|
|
|
71 <node TEXT="agda" ID="ID_286995188" CREATED="1607409838103" MODIFIED="1607409841927"/>
|
|
|
72 <node TEXT="coq" ID="ID_104059977" CREATED="1607409842548" MODIFIED="1607409844388"/>
|
|
|
73 <node TEXT="モデル記述言語" ID="ID_1601862702" CREATED="1607409849304" MODIFIED="1607409856021"/>
|
|
|
74 </node>
|
|
|
75 <node TEXT="証明可能かつ動く実装が出来るのは限られる" ID="ID_1135633058" CREATED="1607409857312" MODIFIED="1607409869965">
|
|
|
76 <node TEXT="z" ID="ID_1351484358" CREATED="1607409870121" MODIFIED="1607409874526"/>
|
|
|
77 <node TEXT="C言語のように自由にプログラミングできない" ID="ID_1179551403" CREATED="1607409874775" MODIFIED="1607409894985"/>
|
|
|
78 </node>
|
|
|
79 </node>
|
|
|
80 <node TEXT="OSの信頼性" POSITION="right" ID="ID_14101489" CREATED="1607406133236" MODIFIED="1607410076159">
|
|
|
81 <edge COLOR="#0000ff"/>
|
|
|
82 <node TEXT="OS側の信頼性は高く保証される必要がある" ID="ID_415782527" CREATED="1607409802404" MODIFIED="1607409803889"/>
|
|
|
83 <node TEXT="アプリケーションはOSを前提にしている" ID="ID_1097881899" CREATED="1607409804234" MODIFIED="1607409808044"/>
|
|
|
84 <node TEXT="高い拡張性も持つ必要がある" ID="ID_942895988" CREATED="1607409902688" MODIFIED="1607409923018"/>
|
|
|
85 <node TEXT="証明可能かつ動くOSがほしい" ID="ID_1872416127" CREATED="1607409986379" MODIFIED="1607410002919"/>
|
|
|
86 <node TEXT="Gears/CbCで解決したい" ID="ID_1762270235" CREATED="1607410009412" MODIFIED="1607410076159">
|
|
|
87 <node TEXT="CodeGear" ID="ID_1507339587" CREATED="1607410015920" MODIFIED="1607410018257"/>
|
|
|
88 <node TEXT="MetaCodeGear" ID="ID_775893838" CREATED="1607410018670" MODIFIED="1607410023745">
|
|
|
89 <node TEXT="Metaで証明を挟む" ID="ID_566158152" CREATED="1607410026768" MODIFIED="1607410033878"/>
|
|
|
90 <node TEXT="信頼性の保証はMetaで行う" ID="ID_4745358" CREATED="1607410034270" MODIFIED="1607410045242"/>
|
|
|
91 </node>
|
|
|
92 <node TEXT="Agda <-> CbCで相互変換をする" ID="ID_1273550084" CREATED="1607410085979" MODIFIED="1607410097425">
|
|
|
93 <node TEXT="agdaからCbCの一方方向?" ID="ID_41779345" CREATED="1607410098476" MODIFIED="1607410108129"/>
|
|
|
94 </node>
|
|
|
95 </node>
|
|
|
96 </node>
|
|
|
97 <node TEXT="GearsOS" POSITION="left" ID="ID_1651648479" CREATED="1607406135887" MODIFIED="1607406139127">
|
|
|
98 <edge COLOR="#00ff00"/>
|
|
|
99 </node>
|
|
|
100 <node TEXT="" POSITION="left" ID="ID_1469562629" CREATED="1607410324461" MODIFIED="1607410324463">
|
|
|
101 <edge COLOR="#ff00ff"/>
|
|
|
102 </node>
|
|
|
103 <node TEXT="GearsのAPI" POSITION="right" ID="ID_164532708" CREATED="1607410326821" MODIFIED="1607410339785">
|
|
|
104 <edge COLOR="#00ffff"/>
|
|
|
105 <node TEXT="context" ID="ID_221503071" CREATED="1607410340389" MODIFIED="1607410345184">
|
|
|
106 <node TEXT="createContext" ID="ID_1897722231" CREATED="1607410347503" MODIFIED="1607410350601">
|
|
|
107 <node TEXT="コンストラクタに相当する" ID="ID_1993397173" CREATED="1607410359489" MODIFIED="1607410367244"/>
|
|
|
108 <node TEXT="構造体の初期化" ID="ID_145693211" CREATED="1607410375763" MODIFIED="1607410419367"/>
|
|
|
109 <node TEXT="enumの設定" ID="ID_929172173" CREATED="1607410419707" MODIFIED="1607410424172"/>
|
|
|
110 <node TEXT="現在は自動生成" ID="ID_1917526305" CREATED="1607410464668" MODIFIED="1607410469829"/>
|
|
|
111 </node>
|
|
|
112 <node TEXT="Meta計算" ID="ID_1460127604" CREATED="1607410350903" MODIFIED="1607410357673">
|
|
|
113 <node TEXT="Perlで生成される" ID="ID_1187821600" CREATED="1607410471357" MODIFIED="1607410475684"/>
|
|
|
114 <node TEXT="ほとんどはstub" ID="ID_1187732606" CREATED="1607410476147" MODIFIED="1607410491112">
|
|
|
115 <node TEXT="prevCodeGear" ID="ID_1246312422" CREATED="1607410492527" MODIFIED="1607410507814"/>
|
|
|
116 <node TEXT="contextから値を取り出す" ID="ID_539268101" CREATED="1607410508120" MODIFIED="1607410515547"/>
|
|
|
117 <node TEXT="contextへ値を積むのはCodeGearの末尾" ID="ID_958749071" CREATED="1607410521360" MODIFIED="1607410537963"/>
|
|
|
118 </node>
|
|
|
119 </node>
|
|
|
120 </node>
|
|
|
121 <node TEXT="" ID="ID_1080105775" CREATED="1607410345523" MODIFIED="1607410345523"/>
|
|
|
122 </node>
|
|
|
123 </node>
|
|
|
124 </map>
|
