Mercurial > hg > Papers > 2023 > moririn-sigos

changeset 5:7cb97e1d76c0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 12 May 2023 19:41:59 +0900
parents 854b01e2ce98
children 9e85fa1cc6a8
files presen.ind rbtree-gearsagda.mm
diffstat 2 files changed, 128 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presen.ind	Fri May 12 19:41:59 2023 +0900
@@ -0,0 +1,63 @@
+-title: GearsAgdaによる Red Black Tree の検証
+
+-author: 森逸汰 河野真治 
+
+
+---Presentation
+
+---Gears OS 上のRedBlack treeの検証
+
+----Gears OS
+
+----codeGear
+
+----dataGear
+
+----metaGear
+
+----context
+
+----証明支援系
+
+-----Agda
+
+-----Pure Functional Language
+
+-----Curry Howard Isomorphism
+
+-----dependent types
+
+-----ZF Set theory
+
+----GearsAgda
+
+----codeGear description in Agda
+
+----dataGear = record in Agda
+
+-----story
+
+------simple while program
+
+------Hoare Logic
+
+------binary tree
+
+-------invariant
+
+-------tree
+
+-------stack
+
+-------replace
+
+------concurrency
+
+------meta gear
+
+------context
+
+------red black tree
+
+------red black tree invariant
+
--- a/rbtree-gearsagda.mm	Mon Apr 17 20:31:28 2023 +0900
+++ b/rbtree-gearsagda.mm	Fri May 12 19:41:59 2023 +0900
@@ -1,14 +1,14 @@
-<map version="freeplane 1.9.13">
+<map version="freeplane 1.11.1">
 <!--To view this file, download free mind mapping software Freeplane from https://www.freeplane.org -->
 <node TEXT="rbtree-gearsagda" FOLDED="false" ID="ID_452131666" CREATED="1610381621610" MODIFIED="1681354145545" STYLE="oval">
 <font SIZE="18"/>
 <hook NAME="MapStyle" zoom="0.75">
-    <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"/>
+    <properties edgeColorConfiguration="#808080ff,#ff0000ff,#0000ffff,#00ff00ff,#ff00ffff,#00ffffff,#7c0000ff,#00007cff,#007c00ff,#7c007cff,#007c7cff,#7c7c00ff" show_icon_for_attributes="true" associatedTemplateLocation="template:/standard-1.6-noEdgeColor.mm" show_note_icons="true" fit_to_viewport="false"/>
 
 <map_styles>
 <stylenode LOCALIZED_TEXT="styles.root_node" STYLE="oval" UNIFORM_SHAPE="true" VGAP_QUANTITY="24 pt">
 <font SIZE="24"/>
-<stylenode LOCALIZED_TEXT="styles.predefined" POSITION="right" STYLE="bubble">
+<stylenode LOCALIZED_TEXT="styles.predefined" POSITION="bottom_or_right" STYLE="bubble">
 <stylenode LOCALIZED_TEXT="default" ID="ID_207122690" COLOR="#000000" STYLE="fork">
 <arrowlink SHAPE="CUBIC_CURVE" COLOR="#000000" WIDTH="2" TRANSPARENCY="200" DASH="" FONT_SIZE="9" FONT_FAMILY="SansSerif" DESTINATION="ID_207122690" STARTARROW="NONE" ENDARROW="DEFAULT"/>
 <font NAME="SansSerif" SIZE="10" BOLD="false" ITALIC="false"/>
@@ -26,7 +26,7 @@
 </stylenode>
 <stylenode LOCALIZED_TEXT="defaultstyle.selection" BACKGROUND_COLOR="#afd3f7" BORDER_COLOR_LIKE_EDGE="false" BORDER_COLOR="#afd3f7"/>
 </stylenode>
-<stylenode LOCALIZED_TEXT="styles.user-defined" POSITION="right" STYLE="bubble">
+<stylenode LOCALIZED_TEXT="styles.user-defined" POSITION="bottom_or_right" STYLE="bubble">
 <stylenode LOCALIZED_TEXT="styles.topic" COLOR="#18898b" STYLE="fork">
 <font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
 </stylenode>
@@ -41,7 +41,7 @@
 <arrowlink COLOR="#003399" TRANSPARENCY="255" DESTINATION="ID_3752836"/>
 </stylenode>
 </stylenode>
-<stylenode LOCALIZED_TEXT="styles.AutomaticLayout" POSITION="right" STYLE="bubble">
+<stylenode LOCALIZED_TEXT="styles.AutomaticLayout" POSITION="bottom_or_right" STYLE="bubble">
 <stylenode LOCALIZED_TEXT="AutomaticLayout.level.root" COLOR="#000000" STYLE="oval" SHAPE_HORIZONTAL_MARGIN="10 pt" SHAPE_VERTICAL_MARGIN="10 pt">
 <font SIZE="18"/>
 </stylenode>
@@ -68,25 +68,25 @@
 </stylenode>
 </map_styles>
 </hook>
-<node TEXT="GearAgdanによるRed Black Tree の検証" POSITION="right" ID="ID_1707429913" CREATED="1681354146375" MODIFIED="1681354149504"/>
-<node TEXT="Gears OS" POSITION="left" ID="ID_1627768067" CREATED="1681370097231" MODIFIED="1681370135147">
+<node TEXT="GearAgdanによるRed Black Tree の検証" POSITION="bottom_or_right" ID="ID_1707429913" CREATED="1681354146375" MODIFIED="1681354149504"/>
+<node TEXT="Gears OS" POSITION="top_or_left" ID="ID_1627768067" CREATED="1681370097231" MODIFIED="1681370135147">
 <node TEXT="Continuation based C" ID="ID_886365419" CREATED="1681370135452" MODIFIED="1681370144727"/>
 <node TEXT="CodeGear and DataGear" ID="ID_1505619678" CREATED="1681370145576" MODIFIED="1681370169360"/>
 <node TEXT="GearsAgda" ID="ID_1483093782" CREATED="1681370170247" MODIFIED="1681370174624"/>
 <node TEXT="lightweigt continuation" ID="ID_709373441" CREATED="1681370232271" MODIFIED="1681370241482"/>
 </node>
-<node TEXT="meta computation" POSITION="left" ID="ID_587222105" CREATED="1681370246638" MODIFIED="1681370255183">
+<node TEXT="meta computation" POSITION="top_or_left" ID="ID_587222105" CREATED="1681370246638" MODIFIED="1681370255183">
 <node TEXT="IO" ID="ID_939386664" CREATED="1681370255664" MODIFIED="1681370261532"/>
 <node TEXT="Hoare Logic" ID="ID_468705414" CREATED="1681370262977" MODIFIED="1681370270967"/>
 </node>
-<node TEXT="meata computation in GearsAgda" POSITION="left" ID="ID_1679966111" CREATED="1681370285647" MODIFIED="1681370300383">
+<node TEXT="meata computation in GearsAgda" POSITION="top_or_left" ID="ID_1679966111" CREATED="1681370285647" MODIFIED="1681370300383">
 <node TEXT="Gears Form" ID="ID_562028595" CREATED="1681370303175" MODIFIED="1681370328863"/>
 <node TEXT="Meta computation" ID="ID_532649685" CREATED="1681370334319" MODIFIED="1681370340118"/>
 <node TEXT="Segment" ID="ID_1391622726" CREATED="1681370342818" MODIFIED="1681370346242"/>
 <node TEXT="stub" ID="ID_1481524131" CREATED="1681370347413" MODIFIED="1681370350369"/>
 <node TEXT="CodeGear table" ID="ID_528079968" CREATED="1681370352629" MODIFIED="1681370366378"/>
 </node>
-<node TEXT="Hoare Logic" POSITION="left" ID="ID_590542814" CREATED="1681370375413" MODIFIED="1681370379970">
+<node TEXT="Hoare Logic" POSITION="top_or_left" ID="ID_590542814" CREATED="1681370375413" MODIFIED="1681370379970">
 <node TEXT="command base" ID="ID_1041738747" CREATED="1681370380249" MODIFIED="1681370383059"/>
 <node TEXT="first order" ID="ID_1511997811" CREATED="1681370399684" MODIFIED="1681370403829"/>
 <node TEXT="soundness" ID="ID_783227970" CREATED="1681370407410" MODIFIED="1681370413286">
@@ -94,7 +94,7 @@
 </node>
 <node TEXT="no proof support" ID="ID_94897053" CREATED="1681370433921" MODIFIED="1681370438778"/>
 </node>
-<node TEXT="GearsAgda" POSITION="left" ID="ID_613685836" CREATED="1681370441463" MODIFIED="1681370446502">
+<node TEXT="GearsAgda" POSITION="top_or_left" ID="ID_613685836" CREATED="1681370441463" MODIFIED="1681370446502">
 <node TEXT="written in Agda" ID="ID_883451142" CREATED="1681370450642" MODIFIED="1681370456415">
 <node TEXT="proof assistance" ID="ID_567095247" CREATED="1681370456760" MODIFIED="1681370462431"/>
 </node>
@@ -110,7 +110,53 @@
 <node TEXT="much simpler" ID="ID_245103686" CREATED="1681370613781" MODIFIED="1681370622639"/>
 </node>
 </node>
-<node TEXT="concurrency" POSITION="right" ID="ID_1659998734" CREATED="1681370628915" MODIFIED="1681370636745">
+<node TEXT="Presentation" POSITION="top_or_left" ID="ID_353783059" CREATED="1683887345844" MODIFIED="1683887354414">
+<node TEXT="Gears OS 上のRedBlack treeの検証" ID="ID_1491219391" CREATED="1683887359703" MODIFIED="1683887388887"/>
+<node TEXT="Gears OS" ID="ID_1283437220" CREATED="1683887392034" MODIFIED="1683887398709">
+<node TEXT="codeGear" ID="ID_852344528" CREATED="1683887400011" MODIFIED="1683887407526"/>
+<node TEXT="dataGear" ID="ID_902863002" CREATED="1683887408406" MODIFIED="1683887411233"/>
+<node TEXT="metaGear" ID="ID_1291359998" CREATED="1683887412417" MODIFIED="1683887416612"/>
+<node TEXT="context" ID="ID_1278338900" CREATED="1683887417374" MODIFIED="1683887420098"/>
+</node>
+<node TEXT="証明支援系" ID="ID_1151818435" CREATED="1683887427527" MODIFIED="1683887447307">
+<node TEXT="Agda" ID="ID_1588116344" CREATED="1683887449127" MODIFIED="1683887485328">
+<node TEXT="Pure Functional Language" ID="ID_380370390" CREATED="1683887485905" MODIFIED="1683887494711"/>
+<node TEXT="Curry Howard Isomorphism" ID="ID_1101016180" CREATED="1683887495105" MODIFIED="1683887509331"/>
+<node TEXT="dependent types" ID="ID_1254854471" CREATED="1683887511992" MODIFIED="1683887517351"/>
+<node TEXT="ZF Set theory" ID="ID_1470282970" CREATED="1683887520133" MODIFIED="1683887530950"/>
+</node>
+</node>
+<node TEXT="GearsAgda" ID="ID_561488040" CREATED="1683887538980" MODIFIED="1683887549597">
+<node TEXT="codeGear description in Agda" ID="ID_221445719" CREATED="1683887550068" MODIFIED="1683887560243"/>
+<node TEXT="dataGear = record in Agda" ID="ID_1464798893" CREATED="1683887562362" MODIFIED="1683887572050"/>
+</node>
+<node TEXT="" ID="ID_300192434" CREATED="1683887585196" MODIFIED="1683887675626">
+<node TEXT="story" ID="ID_971285216" CREATED="1683887585747" MODIFIED="1683887675625">
+<node TEXT="simple while program" ID="ID_1466788813" CREATED="1683887591179" MODIFIED="1683887597947">
+<node TEXT="Hoare Logic" ID="ID_1790836041" CREATED="1683887625141" MODIFIED="1683887631021"/>
+</node>
+<node TEXT="binary tree" ID="ID_1289118233" CREATED="1683887600009" MODIFIED="1683887605568">
+<node TEXT="invariant" ID="ID_1391465057" CREATED="1683887632823" MODIFIED="1683887637443">
+<node TEXT="tree" ID="ID_563398809" CREATED="1683887637744" MODIFIED="1683887640242"/>
+<node TEXT="stack" ID="ID_113711870" CREATED="1683887641100" MODIFIED="1683887644268"/>
+<node TEXT="replace" ID="ID_1902027956" CREATED="1683887644699" MODIFIED="1683887646930"/>
+</node>
+</node>
+<node TEXT="concurrency" ID="ID_711927376" CREATED="1683887606003" MODIFIED="1683887611028">
+<node TEXT="meta gear" ID="ID_1861251046" CREATED="1683887658899" MODIFIED="1683887670736"/>
+<node TEXT="context" ID="ID_1053098679" CREATED="1683887671464" MODIFIED="1683887674103"/>
+</node>
+<node TEXT="red black tree" ID="ID_980116618" CREATED="1683887611641" MODIFIED="1683887617305">
+<node TEXT="red black tree invariant" ID="ID_437599501" CREATED="1683887648752" MODIFIED="1683887656910"/>
+</node>
+</node>
+<node TEXT="simple while program" ID="ID_1206362061" CREATED="1683887677689" MODIFIED="1683887683318"/>
+<node TEXT="binary tree" ID="ID_559363966" CREATED="1683887684951" MODIFIED="1683887691598"/>
+<node TEXT="concurrenct" ID="ID_205306235" CREATED="1683887692777" MODIFIED="1683887696069"/>
+<node TEXT="red black tree" ID="ID_798727234" CREATED="1683887696492" MODIFIED="1683887702100"/>
+</node>
+</node>
+<node TEXT="concurrency" POSITION="bottom_or_right" ID="ID_1659998734" CREATED="1681370628915" MODIFIED="1681370636745">
 <node TEXT="codeGear-wise concurency" ID="ID_1216124303" CREATED="1681370637291" MODIFIED="1681370656059"/>
 <node TEXT="assuming  finite computation in a codeGear" ID="ID_573537896" CREATED="1681370657029" MODIFIED="1681370677168"/>
 <node TEXT="scheduler" ID="ID_327350914" CREATED="1681370679365" MODIFIED="1681370685685">
@@ -129,13 +175,13 @@
 <node TEXT="model checking" ID="ID_1191776209" CREATED="1681370766180" MODIFIED="1681370771240"/>
 <node TEXT="proofs on concurrenct" ID="ID_1117350246" CREATED="1681370771658" MODIFIED="1681370781273"/>
 </node>
-<node TEXT="while program" POSITION="right" ID="ID_710382637" CREATED="1681370805471" MODIFIED="1681370811890"/>
-<node TEXT="binary tree" POSITION="right" ID="ID_1922786513" CREATED="1681370796432" MODIFIED="1681370804204">
+<node TEXT="while program" POSITION="bottom_or_right" ID="ID_710382637" CREATED="1681370805471" MODIFIED="1681370811890"/>
+<node TEXT="binary tree" POSITION="bottom_or_right" ID="ID_1922786513" CREATED="1681370796432" MODIFIED="1681370804204">
 <node TEXT="stack invariant" ID="ID_1448419661" CREATED="1681370821482" MODIFIED="1681370830261"/>
 <node TEXT="tree invariant" ID="ID_243832132" CREATED="1681370830768" MODIFIED="1681370835246"/>
 <node TEXT="replace invariant" ID="ID_1303870466" CREATED="1681370835840" MODIFIED="1681370840736"/>
 </node>
-<node TEXT="red black tree" POSITION="right" ID="ID_263237724" CREATED="1681370787198" MODIFIED="1681370792658">
+<node TEXT="red black tree" POSITION="bottom_or_right" ID="ID_263237724" CREATED="1681370787198" MODIFIED="1681370792658">
 <node TEXT="red and black" ID="ID_385223552" CREATED="1681370848145" MODIFIED="1681370856270"/>
 <node TEXT="parent and grand parent" ID="ID_517970079" CREATED="1681370857076" MODIFIED="1681370866920">
 <node TEXT="in stack" ID="ID_901165358" CREATED="1681370867215" MODIFIED="1681370872234"/>
@@ -149,19 +195,19 @@
 </node>
 </node>
 </node>
-<node TEXT="complied code" POSITION="right" ID="ID_1551916219" CREATED="1681370926034" MODIFIED="1681370931197">
+<node TEXT="complied code" POSITION="bottom_or_right" ID="ID_1551916219" CREATED="1681370926034" MODIFIED="1681370931197">
 <node TEXT="gearsAgda  →　CbC conversion" ID="ID_159756131" CREATED="1681370931496" MODIFIED="1681370953438"/>
 <node TEXT="combine multiple codeGear" ID="ID_1952851358" CREATED="1681371036240" MODIFIED="1681371047551">
 <node TEXT="optimization" ID="ID_256515995" CREATED="1681371048689" MODIFIED="1681371053081"/>
 </node>
 </node>
-<node TEXT="is this reliable?" POSITION="right" ID="ID_189224322" CREATED="1681370969828" MODIFIED="1681370979059">
+<node TEXT="is this reliable?" POSITION="bottom_or_right" ID="ID_189224322" CREATED="1681370969828" MODIFIED="1681370979059">
 <node TEXT="with proofs" ID="ID_114174861" CREATED="1681370979357" MODIFIED="1681370985340">
 <node TEXT="relative to the theory" ID="ID_194349290" CREATED="1681370985587" MODIFIED="1681371003316"/>
 </node>
 <node TEXT="invariant gives all property" ID="ID_955091732" CREATED="1681371007176" MODIFIED="1681371020551"/>
 </node>
-<node TEXT="is this scale?" POSITION="right" ID="ID_1442547192" CREATED="1681371022394" MODIFIED="1681371028550">
+<node TEXT="is this scale?" POSITION="bottom_or_right" ID="ID_1442547192" CREATED="1681371022394" MODIFIED="1681371028550">
 <node TEXT="size of invariant" ID="ID_66636375" CREATED="1681470579922" MODIFIED="1681470584136"/>
 <node TEXT="polynominal of cases of invariant" ID="ID_1431513531" CREATED="1681470584691" MODIFIED="1681470597800"/>
 <node TEXT="not all combination is possible" ID="ID_1626555105" CREATED="1681470604805" MODIFIED="1681470612527"/>
@@ -170,7 +216,7 @@
 <node TEXT="partial" ID="ID_649982266" CREATED="1681470631099" MODIFIED="1681470634557"/>
 </node>
 </node>
-<node TEXT="contents" POSITION="right" ID="ID_1884614552" CREATED="1681470012072" MODIFIED="1681470018912">
+<node TEXT="contents" POSITION="bottom_or_right" ID="ID_1884614552" CREATED="1681470012072" MODIFIED="1681470018912">
 <node TEXT="verified red black tree" ID="ID_72137676" CREATED="1681470019151" MODIFIED="1681470047634"/>
 <node TEXT="importance" ID="ID_510340227" CREATED="1681470049510" MODIFIED="1681470056562">
 <node TEXT="conversion to classical form" ID="ID_312471113" CREATED="1681470523375" MODIFIED="1681470532568">