Mercurial > hg > Papers > 2021 > anatofuz-master

changeset 0:b4d27c6b474f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add mindmap
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Tue, 08 Dec 2020 18:55:01 +0900
parents
children a5f3fe9966fb
files mindmap.mm
diffstat 1 files changed, 124 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/mindmap.mm	Tue Dec 08 18:55:01 2020 +0900
@@ -0,0 +1,124 @@
+<map version="freeplane 1.8.0">
+<!--To view this file, download free mind mapping software Freeplane from http://freeplane.sourceforge.net -->
+<node TEXT="GearsOSのAPI" FOLDED="false" ID="ID_1391122564" CREATED="1607406106629" MODIFIED="1607406119323" STYLE="oval">
+<font SIZE="18"/>
+<hook NAME="MapStyle">
+    <properties edgeColorConfiguration="#808080ff,#ff0000ff,#0000ffff,#00ff00ff,#ff00ffff,#00ffffff,#7c0000ff,#00007cff,#007c00ff,#7c007cff,#007c7cff,#7c7c00ff" fit_to_viewport="false"/>
+
+<map_styles>
+<stylenode LOCALIZED_TEXT="styles.root_node" STYLE="oval" UNIFORM_SHAPE="true" VGAP_QUANTITY="24.0 pt">
+<font SIZE="24"/>
+<stylenode LOCALIZED_TEXT="styles.predefined" POSITION="right" STYLE="bubble">
+<stylenode LOCALIZED_TEXT="default" ICON_SIZE="12.0 pt" COLOR="#000000" STYLE="fork">
+<font NAME="SansSerif" SIZE="10" BOLD="false" ITALIC="false"/>
+</stylenode>
+<stylenode LOCALIZED_TEXT="defaultstyle.details"/>
+<stylenode LOCALIZED_TEXT="defaultstyle.attributes">
+<font SIZE="9"/>
+</stylenode>
+<stylenode LOCALIZED_TEXT="defaultstyle.note" COLOR="#000000" BACKGROUND_COLOR="#ffffff" TEXT_ALIGN="LEFT"/>
+<stylenode LOCALIZED_TEXT="defaultstyle.floating">
+<edge STYLE="hide_edge"/>
+<cloud COLOR="#f0f0f0" SHAPE="ROUND_RECT"/>
+</stylenode>
+</stylenode>
+<stylenode LOCALIZED_TEXT="styles.user-defined" POSITION="right" STYLE="bubble">
+<stylenode LOCALIZED_TEXT="styles.topic" COLOR="#18898b" STYLE="fork">
+<font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
+</stylenode>
+<stylenode LOCALIZED_TEXT="styles.subtopic" COLOR="#cc3300" STYLE="fork">
+<font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
+</stylenode>
+<stylenode LOCALIZED_TEXT="styles.subsubtopic" COLOR="#669900">
+<font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
+</stylenode>
+<stylenode LOCALIZED_TEXT="styles.important">
+<icon BUILTIN="yes"/>
+</stylenode>
+</stylenode>
+<stylenode LOCALIZED_TEXT="styles.AutomaticLayout" POSITION="right" STYLE="bubble">
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level.root" COLOR="#000000" STYLE="oval" SHAPE_HORIZONTAL_MARGIN="10.0 pt" SHAPE_VERTICAL_MARGIN="10.0 pt">
+<font SIZE="18"/>
+</stylenode>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,1" COLOR="#0033ff">
+<font SIZE="16"/>
+</stylenode>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,2" COLOR="#00b439">
+<font SIZE="14"/>
+</stylenode>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,3" COLOR="#990000">
+<font SIZE="12"/>
+</stylenode>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,4" COLOR="#111111">
+<font SIZE="10"/>
+</stylenode>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,5"/>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,6"/>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,7"/>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,8"/>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,9"/>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,10"/>
+<stylenode LOCALIZED_TEXT="AutomaticLayout.level,11"/>
+</stylenode>
+</stylenode>
+</map_styles>
+</hook>
+<hook NAME="AutomaticEdgeColor" COUNTER="5" RULE="ON_BRANCH_CREATION"/>
+<node TEXT="プログラムの信頼性を保証するのは難しい" POSITION="right" ID="ID_182717011" CREATED="1607406127549" MODIFIED="1607409819862">
+<edge COLOR="#ff0000"/>
+<node TEXT="テストプログラムで全ては証明できない" ID="ID_1642945466" CREATED="1607406143787" MODIFIED="1607409818771"/>
+<node TEXT="証明でアプローチしたい" ID="ID_328449335" CREATED="1607409771301" MODIFIED="1607409837716">
+<node TEXT="agda" ID="ID_286995188" CREATED="1607409838103" MODIFIED="1607409841927"/>
+<node TEXT="coq" ID="ID_104059977" CREATED="1607409842548" MODIFIED="1607409844388"/>
+<node TEXT="モデル記述言語" ID="ID_1601862702" CREATED="1607409849304" MODIFIED="1607409856021"/>
+</node>
+<node TEXT="証明可能かつ動く実装が出来るのは限られる" ID="ID_1135633058" CREATED="1607409857312" MODIFIED="1607409869965">
+<node TEXT="z" ID="ID_1351484358" CREATED="1607409870121" MODIFIED="1607409874526"/>
+<node TEXT="C言語のように自由にプログラミングできない" ID="ID_1179551403" CREATED="1607409874775" MODIFIED="1607409894985"/>
+</node>
+</node>
+<node TEXT="OSの信頼性" POSITION="right" ID="ID_14101489" CREATED="1607406133236" MODIFIED="1607410076159">
+<edge COLOR="#0000ff"/>
+<node TEXT="OS側の信頼性は高く保証される必要がある" ID="ID_415782527" CREATED="1607409802404" MODIFIED="1607409803889"/>
+<node TEXT="アプリケーションはOSを前提にしている" ID="ID_1097881899" CREATED="1607409804234" MODIFIED="1607409808044"/>
+<node TEXT="高い拡張性も持つ必要がある" ID="ID_942895988" CREATED="1607409902688" MODIFIED="1607409923018"/>
+<node TEXT="証明可能かつ動くOSがほしい" ID="ID_1872416127" CREATED="1607409986379" MODIFIED="1607410002919"/>
+<node TEXT="Gears/CbCで解決したい" ID="ID_1762270235" CREATED="1607410009412" MODIFIED="1607410076159">
+<node TEXT="CodeGear" ID="ID_1507339587" CREATED="1607410015920" MODIFIED="1607410018257"/>
+<node TEXT="MetaCodeGear" ID="ID_775893838" CREATED="1607410018670" MODIFIED="1607410023745">
+<node TEXT="Metaで証明を挟む" ID="ID_566158152" CREATED="1607410026768" MODIFIED="1607410033878"/>
+<node TEXT="信頼性の保証はMetaで行う" ID="ID_4745358" CREATED="1607410034270" MODIFIED="1607410045242"/>
+</node>
+<node TEXT="Agda &lt;-&gt; CbCで相互変換をする" ID="ID_1273550084" CREATED="1607410085979" MODIFIED="1607410097425">
+<node TEXT="agdaからCbCの一方方向?" ID="ID_41779345" CREATED="1607410098476" MODIFIED="1607410108129"/>
+</node>
+</node>
+</node>
+<node TEXT="GearsOS" POSITION="left" ID="ID_1651648479" CREATED="1607406135887" MODIFIED="1607406139127">
+<edge COLOR="#00ff00"/>
+</node>
+<node TEXT="" POSITION="left" ID="ID_1469562629" CREATED="1607410324461" MODIFIED="1607410324463">
+<edge COLOR="#ff00ff"/>
+</node>
+<node TEXT="GearsのAPI" POSITION="right" ID="ID_164532708" CREATED="1607410326821" MODIFIED="1607410339785">
+<edge COLOR="#00ffff"/>
+<node TEXT="context" ID="ID_221503071" CREATED="1607410340389" MODIFIED="1607410345184">
+<node TEXT="createContext" ID="ID_1897722231" CREATED="1607410347503" MODIFIED="1607410350601">
+<node TEXT="コンストラクタに相当する" ID="ID_1993397173" CREATED="1607410359489" MODIFIED="1607410367244"/>
+<node TEXT="構造体の初期化" ID="ID_145693211" CREATED="1607410375763" MODIFIED="1607410419367"/>
+<node TEXT="enumの設定" ID="ID_929172173" CREATED="1607410419707" MODIFIED="1607410424172"/>
+<node TEXT="現在は自動生成" ID="ID_1917526305" CREATED="1607410464668" MODIFIED="1607410469829"/>
+</node>
+<node TEXT="Meta計算" ID="ID_1460127604" CREATED="1607410350903" MODIFIED="1607410357673">
+<node TEXT="Perlで生成される" ID="ID_1187821600" CREATED="1607410471357" MODIFIED="1607410475684"/>
+<node TEXT="ほとんどはstub" ID="ID_1187732606" CREATED="1607410476147" MODIFIED="1607410491112">
+<node TEXT="prevCodeGear" ID="ID_1246312422" CREATED="1607410492527" MODIFIED="1607410507814"/>
+<node TEXT="contextから値を取り出す" ID="ID_539268101" CREATED="1607410508120" MODIFIED="1607410515547"/>
+<node TEXT="contextへ値を積むのはCodeGearの末尾" ID="ID_958749071" CREATED="1607410521360" MODIFIED="1607410537963"/>
+</node>
+</node>
+</node>
+<node TEXT="" ID="ID_1080105775" CREATED="1607410345523" MODIFIED="1607410345523"/>
+</node>
+</node>
+</map>