Mercurial > hg > Papers > 2021 > soto-thesis

changeset 1:cfe0a2ed1d1d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add mindmap
author soto
date Tue, 12 Jan 2021 21:41:41 +0900
parents 3dba680da508
children 2c50fd1d115e
files CbC.mm prepaper/pre.pdf prepaper/pre.tex
diffstat 3 files changed, 72 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CbC.mm	Tue Jan 12 21:41:41 2021 +0900
@@ -0,0 +1,68 @@
+<map version="1.0.1">
+<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
+<node CREATED="1610431917883" ID="ID_69434326" MODIFIED="1610433286412" TEXT="CbC&#x306e;&#x8d64;&#x9ed2;&#x6728;&#x306e;&#x8a3c;&#x660e;">
+<node CREATED="1610433078641" ID="ID_1912873340" MODIFIED="1610433131450" POSITION="right" TEXT="&#x306f;&#x3058;&#x3081;&#x306b;">
+<node CREATED="1610434150646" ID="ID_1532099181" MODIFIED="1610434157499" TEXT="&#x7814;&#x7a76;&#x76ee;&#x7684;"/>
+<node CREATED="1610434158109" ID="ID_1226471708" MODIFIED="1610434164242" TEXT="&#x7814;&#x7a76;&#x6982;&#x8981;"/>
+</node>
+<node CREATED="1610434171089" ID="ID_1048180636" MODIFIED="1610434194541" POSITION="right" TEXT="&#x6280;&#x8853;&#x6982;&#x8981;">
+<node CREATED="1610432228093" ID="ID_1317029323" MODIFIED="1610433620048" TEXT="Continuation Based C">
+<node CREATED="1610432236227" ID="ID_242847633" MODIFIED="1610432245873" TEXT="Continuation"/>
+<node CREATED="1610433455134" ID="ID_1398717454" MODIFIED="1610433478565" TEXT="Code Gear"/>
+<node CREATED="1610433479634" ID="ID_888566501" MODIFIED="1610433485493" TEXT="Data Gear"/>
+<node CREATED="1610433485494" ID="ID_1166649887" MODIFIED="1610433521263" TEXT="Meta Code Gear"/>
+<node CREATED="1610433536146" ID="ID_59062075" MODIFIED="1610433549400" TEXT="Meta Data Gear"/>
+<node CREATED="1610433553287" ID="ID_1596638477" MODIFIED="1610433560141" TEXT="Pre Condition">
+<node CREATED="1610433560142" ID="ID_1776681384" MODIFIED="1610433560142" TEXT=""/>
+</node>
+<node CREATED="1610433570809" ID="ID_1025721984" MODIFIED="1610433580323" TEXT="Post Condition"/>
+</node>
+<node CREATED="1610431932711" ID="ID_767505064" MODIFIED="1610433204203" TEXT="&#x8a3c;&#x660e;&#x652f;&#x63f4;">
+<node CREATED="1610431945764" ID="ID_1193847646" MODIFIED="1610432145292" TEXT="Agda">
+<node CREATED="1610432788966" ID="ID_1994361987" MODIFIED="1610432881725" TEXT="&#x5165;&#x9580;">
+<node CREATED="1610432801462" ID="ID_1894671340" MODIFIED="1610432805634" TEXT="intro"/>
+<node CREATED="1610432792282" ID="ID_97957418" MODIFIED="1610432800788" TEXT="&#x95a2;&#x6570;&#x5b9a;&#x7fa9;"/>
+<node CREATED="1610432868425" ID="ID_1144310807" MODIFIED="1610432873243" TEXT="record"/>
+<node CREATED="1610432873441" ID="ID_1629098140" MODIFIED="1610432875737" TEXT="data"/>
+<node CREATED="1610432876085" ID="ID_596594431" MODIFIED="1610432881352" TEXT="&#x7701;&#x7565;&#x5f62;"/>
+<node CREATED="1610432881726" ID="ID_519285288" MODIFIED="1610432888078" TEXT="with"/>
+</node>
+</node>
+<node CREATED="1610431957797" ID="ID_321220359" MODIFIED="1610431961305" TEXT="Coq">
+<node CREATED="1610432888596" ID="ID_1347955101" MODIFIED="1610432892450" TEXT="&#x5165;&#x9580;"/>
+</node>
+<node CREATED="1610431961675" ID="ID_1373478938" MODIFIED="1610432197558" TEXT="World">
+<node CREATED="1610432892657" ID="ID_1019469599" MODIFIED="1610432895567" TEXT="&#x5165;&#x9580;"/>
+</node>
+</node>
+<node CREATED="1610432623419" ID="ID_1592479531" MODIFIED="1610433205441" TEXT="Tree">
+<node CREATED="1610432640387" ID="ID_1686448832" MODIFIED="1610432650648" TEXT="Binary Tree"/>
+<node CREATED="1610432650650" ID="ID_738181291" MODIFIED="1610433811349" TEXT="Red Black Tree">
+<node CREATED="1610432658855" ID="ID_996001351" MODIFIED="1610432720030" TEXT="Left Leaning Red Black Tree"/>
+</node>
+</node>
+<node CREATED="1610433157507" ID="ID_1903145870" MODIFIED="1610433165788" TEXT="Hoare Logic">
+<node CREATED="1610433694154" ID="ID_1719079398" MODIFIED="1610433699965" TEXT="&#x5165;&#x9580;"/>
+<node CREATED="1610433700986" ID="ID_875581830" MODIFIED="1610433710775" TEXT="&#x5b9f;&#x4f8b;"/>
+</node>
+</node>
+<node CREATED="1610434209123" ID="ID_1589930152" MODIFIED="1610434263511" POSITION="right" TEXT="&#x5b9f;&#x9a13;&#x5185;&#x5bb9;">
+<node CREATED="1610432426159" ID="ID_734023510" MODIFIED="1610433652122" TEXT="&#x5b9f;&#x88c5;">
+<node CREATED="1610432917273" ID="ID_689000830" MODIFIED="1610432939985" TEXT="Agda &#x3067;&#x306e; Continuation &#x8a18;&#x8ff0;&#x65b9;&#x6cd5;"/>
+<node CREATED="1610432991112" ID="ID_1694126929" MODIFIED="1610432994872" TEXT="&#x5b9f;&#x4f8b;"/>
+<node CREATED="1610433652536" ID="ID_311055322" MODIFIED="1610433660923" TEXT="RBT&#x306e;&#x5b9f;&#x88c5;&#x65b9;&#x6cd5;"/>
+</node>
+<node CREATED="1610432296061" ID="ID_734540745" MODIFIED="1610432348438" TEXT="&#x691c;&#x8a3c;">
+<node CREATED="1610432292173" ID="ID_1242317103" MODIFIED="1610433062080" TEXT="Hoare Logic&#x3092;&#x7528;&#x3044;&#x305f;&#x691c;&#x8a3c;&#x65b9;&#x6cd5;">
+<node CREATED="1610433723615" ID="ID_1187781832" MODIFIED="1610433757626" TEXT="Pre / Post Condition&#x3068;&#x306e;&#x4e00;&#x81f4;&#x3092;&#x898b;&#x308b;&#xff1f;"/>
+</node>
+<node CREATED="1610433010493" ID="ID_1348923701" MODIFIED="1610433014878" TEXT="&#x5b9f;&#x4f8b;"/>
+<node CREATED="1610433661468" ID="ID_944416824" MODIFIED="1610433668091" TEXT="RBT&#x306e;&#x691c;&#x8a3c;&#x65b9;&#x6cd5;"/>
+</node>
+<node CREATED="1610432352721" ID="ID_31433990" MODIFIED="1610433015385" TEXT="&#x5065;&#x5168;&#x6027;">
+<node CREATED="1610433015801" ID="ID_1186946772" MODIFIED="1610433023367" TEXT="&#x5b9f;&#x4f8b;"/>
+</node>
+</node>
+<node CREATED="1610434009821" ID="ID_1460697900" MODIFIED="1610434016168" POSITION="right" TEXT="&#x307e;&#x3068;&#x3081;"/>
+</node>
+</map>
Binary file prepaper/pre.pdf has changed
--- a/prepaper/pre.tex	Tue Dec 08 19:06:49 2020 +0900
+++ b/prepaper/pre.tex	Tue Jan 12 21:41:41 2021 +0900
@@ -5,7 +5,7 @@
 \usepackage[]{multicol}
 \usepackage{listings}
 %\pagestyle{fancy}
-\lhead{\parpic{\includegraphics[height=1\zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部工学科知能情報コース 中間発表予稿}
+\lhead{\parpic{\includegraphics[height=1\zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部工学科知能情報コース 予稿}
 \rhead{}
 \cfoot{}
 
@@ -79,11 +79,12 @@
 \begin{multicols*}{2}
     \input{tex/intro.tex} % 研究目的
     \input{tex/cbc.tex} % CbC の説明
-    \input{tex/agda.tex} % agda の説明
+    \input{tex/agda.tex} % agda の説明　levelの説明
+    \input{tex/continuation_agda.tex} % continuation agdaの説明
     \input{tex/hoare.tex} % Hoare Logic の説明
     % Hoare Logicでの検証方法
     \input{tex/rbtree.tex} % 赤黒木の説明
-    % \input{tex/spec.tex}% 手法
+    \input{tex/spec.tex}% 手法
     % btの実装
     % btの検証
     % rbtの実装