Mercurial > hg > Papers > 2018 > ryokka-sigos
changeset 3:576637483425
fix section, source code,etc
line wrap: on
line diff
--- a/Paper/auto/sigos.el Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/auto/sigos.el Thu Apr 19 20:28:12 2018 +0900 @@ -30,13 +30,13 @@ "amssymb" "caption") (LaTeX-add-labels - "fig:csds" - "fig:code_simple" - "fig:factorial" + "fig:cgdg" + "fig:meta-cgdg" "agda-interface-stack" "hoare-logic" "fig:hoare" - "fig:cbc-hoare") + "fig:cbc-hoare" + "fig:tree-hoare") (LaTeX-add-bibliographies)) :latex)
--- a/Paper/pic/MetaGear.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/MetaGear.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: MetaGear.pdf +%%Title: ./pic/MetaGear.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 792 532 %%HiResBoundingBox: 0.000000 0.000000 792.000000 532.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/cbc-hoare.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/cbc-hoare.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: cbc-hoare.pdf +%%Title: ./pic/cbc-hoare.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 580 175 %%HiResBoundingBox: 0.000000 0.000000 580.000000 175.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/cbc-subtype.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/cbc-subtype.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: cbc-subtype.pdf +%%Title: ./pic/cbc-subtype.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 1084 281 %%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/cbc_goto.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/cbc_goto.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: cbc_goto.pdf +%%Title: ./pic/cbc_goto.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 393 201 %%HiResBoundingBox: 0.000000 0.000000 393.000000 201.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/codeGear_dataGear.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/codeGear_dataGear.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: codeGear_dataGear.pdf +%%Title: ./pic/codeGear_dataGear.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 535 427 %%HiResBoundingBox: 0.000000 0.000000 535.000000 427.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/codeGear_dataGear_dependency.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/codeGear_dataGear_dependency.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: codeGear_dataGear_dependency.pdf +%%Title: ./pic/codeGear_dataGear_dependency.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 535 247 %%HiResBoundingBox: 0.000000 0.000000 535.000000 247.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/codesegment.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/codesegment.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: codesegment.pdf +%%Title: ./pic/codesegment.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 305 85 %%HiResBoundingBox: 0.000000 0.000000 305.000000 85.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/codesegment2.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/codesegment2.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: codesegment2.pdf +%%Title: ./pic/codesegment2.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 393 201 %%HiResBoundingBox: 0.000000 0.000000 393.000000 201.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/csds.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/csds.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: csds.pdf +%%Title: ./pic/csds.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 580 76 %%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/factorial.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/factorial.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: factorial.pdf +%%Title: ./pic/factorial.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 296 220 %%HiResBoundingBox: 0.000000 0.000000 296.000000 220.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/pic/funcLoop.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -0,0 +1,8 @@ +%%Title: ./pic/funcLoop.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 0 0 647 168 +%%HiResBoundingBox: 0.000000 0.000000 647.000000 168.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Thu Apr 19 19:27:00 2018 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/pic/funcLoopinAutomata.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -0,0 +1,8 @@ +%%Title: ./pic/funcLoopinAutomata.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 0 0 489 473 +%%HiResBoundingBox: 0.000000 0.000000 489.000000 473.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Thu Apr 19 19:27:00 2018 +
--- a/Paper/pic/gears-meta.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/gears-meta.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: gears-meta.pdf +%%Title: ./pic/gears-meta.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 653 243 %%HiResBoundingBox: 0.000000 0.000000 653.000000 243.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/gears_structure.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/gears_structure.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: gears_structure.pdf +%%Title: ./pic/gears_structure.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 713 418 %%HiResBoundingBox: 0.000000 0.000000 713.000000 418.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/gearsos.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/gearsos.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: gearsos.pdf +%%Title: ./pic/gearsos.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 1174 1004 %%HiResBoundingBox: 0.000000 0.000000 1174.000000 1004.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/generate_context.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/generate_context.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: generate_context.pdf +%%Title: ./pic/generate_context.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 508 408 %%HiResBoundingBox: 0.000000 0.000000 508.000000 408.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/generate_context2.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/generate_context2.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: generate_context2.pdf +%%Title: ./pic/generate_context2.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 706 355 %%HiResBoundingBox: 0.000000 0.000000 706.000000 355.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/generate_context3.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/generate_context3.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: generate_context3.pdf +%%Title: ./pic/generate_context3.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 706 274 %%HiResBoundingBox: 0.000000 0.000000 706.000000 274.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/goto.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/goto.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: goto.pdf +%%Title: ./pic/goto.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 305 85 %%HiResBoundingBox: 0.000000 0.000000 305.000000 85.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/hoare-logic.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/hoare-logic.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: hoare-logic.pdf +%%Title: ./pic/hoare-logic.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 580 76 %%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/meta-hierarchy.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/meta-hierarchy.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: meta-hierarchy.pdf +%%Title: ./pic/meta-hierarchy.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 832 283 %%HiResBoundingBox: 0.000000 0.000000 832.000000 283.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/meta.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/meta.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: meta.pdf +%%Title: ./pic/meta.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 958 148 %%HiResBoundingBox: 0.000000 0.000000 958.000000 148.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/metaCS.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/metaCS.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: metaCS.pdf +%%Title: ./pic/metaCS.pdf %%Creator: extractbb 20160307 %%BoundingBox: 31 511 515 732 %%HiResBoundingBox: 30.601520 511.100000 515.413800 732.012800 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/meta_cg_dg.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/meta_cg_dg.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: meta_cg_dg.pdf +%%Title: ./pic/meta_cg_dg.pdf %%Creator: extractbb 20160307 -%%BoundingBox: 0 0 608 522 -%%HiResBoundingBox: 0.000000 0.000000 608.000000 522.000000 +%%BoundingBox: 2 302 608 522 +%%HiResBoundingBox: 2.019531 302.382800 608.000000 522.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/meta_gear.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/meta_gear.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: meta_gear.pdf +%%Title: ./pic/meta_gear.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 788 229 %%HiResBoundingBox: 0.000000 0.000000 788.000000 229.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/metameta.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/metameta.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: metameta.pdf +%%Title: ./pic/metameta.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 472 184 %%HiResBoundingBox: 0.000000 0.000000 472.000000 184.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/modus-ponens.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/modus-ponens.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: modus-ponens.pdf +%%Title: ./pic/modus-ponens.pdf %%Creator: extractbb 20160307 %%BoundingBox: 96 684 500 799 %%HiResBoundingBox: 96.082030 683.554700 499.886700 799.296900 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Mon Jan 29 15:58:01 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/non-destructive-rbtree.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/non-destructive-rbtree.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: non-destructive-rbtree.pdf +%%Title: ./pic/non-destructive-rbtree.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 559 248 %%HiResBoundingBox: 0.000000 0.000000 559.000000 248.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/persistent_date_tree.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/persistent_date_tree.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: persistent_date_tree.pdf +%%Title: ./pic/persistent_date_tree.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 773 374 %%HiResBoundingBox: 0.000000 0.000000 773.000000 374.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/persistent_date_tree_2.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/persistent_date_tree_2.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: persistent_date_tree_2.pdf +%%Title: ./pic/persistent_date_tree_2.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 736 271 %%HiResBoundingBox: 0.000000 0.000000 736.000000 271.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/put.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/put.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: put.pdf +%%Title: ./pic/put.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 868 130 %%HiResBoundingBox: 0.000000 0.000000 868.000000 130.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/rbtree.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/rbtree.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: rbtree.pdf +%%Title: ./pic/rbtree.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 562 274 %%HiResBoundingBox: 0.000000 0.000000 562.000000 274.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/ryukyu.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/ryukyu.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ryukyu.pdf +%%Title: ./pic/ryukyu.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 595 842 %%HiResBoundingBox: 0.000000 0.000000 595.000000 842.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/subtype-arg.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/subtype-arg.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: subtype-arg.pdf +%%Title: ./pic/subtype-arg.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 1084 281 %%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/subtype-return.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/subtype-return.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: subtype-return.pdf +%%Title: ./pic/subtype-return.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 1084 281 %%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/taskManager.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/taskManager.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: taskManager.pdf +%%Title: ./pic/taskManager.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 1021 459 %%HiResBoundingBox: 0.000000 0.000000 1021.000000 459.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/twice_640.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/twice_640.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: twice_640.pdf +%%Title: ./pic/twice_640.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 360 216 %%HiResBoundingBox: 0.000000 0.000000 360.000000 216.000000 %%PDFVersion: 1.4 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/verification.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/verification.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: verification.pdf +%%Title: ./pic/verification.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 478 204 %%HiResBoundingBox: 0.000000 0.000000 478.000000 204.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/pic/worker.xbb Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/pic/worker.xbb Thu Apr 19 20:28:12 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: worker.pdf +%%Title: ./pic/worker.pdf %%Creator: extractbb 20160307 %%BoundingBox: 0 0 901 644 %%HiResBoundingBox: 0.000000 0.000000 901.000000 644.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Fri Apr 13 18:34:25 2018 +%%CreationDate: Thu Apr 19 19:27:00 2018
--- a/Paper/sigos.bib Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/sigos.bib Thu Apr 19 20:28:12 2018 +0900 @@ -46,7 +46,7 @@ year="2017", month="feb", volume="10", - number="2", + number="2", pages="5-5", URL="https://ci.nii.ac.jp/naid/170000148438/en/", DOI="", @@ -100,10 +100,11 @@ address = {SE-412 96 G\"{o}teborg, Sweden} } -@Comment attomisc{agda-tutorial, -@Comment title = {agda-tutorial}, -@Comment howpublished = {\url{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}}, -@Comment } +@article{ek2009formalizing, + title={Formalizing Arne Andersson trees and left-leaning Red-Black trees in Agda}, + author={Ek, Linus and Holmstr{\"o}m, Ola and Andjelkovic, Stevan} +} + @Comment \bibtem{Agda-Tutorial} @Comment % {Ulf Norell and James Chapman}: Dependently Typed Programming in Agda @Comment % \\\verb|http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf|
--- a/Paper/sigos.tex Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/sigos.tex Thu Apr 19 20:28:12 2018 +0900 @@ -12,31 +12,31 @@ \usepackage{amssymb} \lstset{ - language=C, - tabsize=2, - frame=single, - basicstyle={\ttfamily\footnotesize},% - identifierstyle={\footnotesize},% - commentstyle={\footnotesize\itshape},% - keywordstyle={\footnotesize\bfseries},% - ndkeywordstyle={\footnotesize},% - stringstyle={\footnotesize\ttfamily}, - breaklines=true, - captionpos=b, - columns=[l]{fullflexible},% - xrightmargin=0zw,% - xleftmargin=1zw,% - aboveskip=1zw, - numberstyle={\scriptsize},% - stepnumber=1, - numbersep=0.5zw,% - lineskip=-0.5ex, + language=C, + tabsize=2, + frame=single, + basicstyle={\ttfamily\footnotesize},% + identifierstyle={\footnotesize},% + commentstyle={\footnotesize\itshape},% + keywordstyle={\footnotesize\bfseries},% + ndkeywordstyle={\footnotesize},% + stringstyle={\footnotesize\ttfamily}, + breaklines=true, + captionpos=b, + columns=[l]{fullflexible},% + xrightmargin=0zw,% + xleftmargin=1zw,% + aboveskip=1zw, + numberstyle={\scriptsize},% + stepnumber=1, + numbersep=0.5zw,% + lineskip=-0.5ex, } \renewcommand{\lstlistingname}{Code} \usepackage{caption} \captionsetup[lstlisting]{font={small,tt}} -\input{dummy.tex} %% Font +\input{dummy.tex} %% Font % ユーザが定義したマクロなど． \makeatletter @@ -98,196 +98,128 @@ 動作するソフトウェアは高い信頼性を持つことが望ましい。 そのためにはソフトウェアが期待される動作をすることを保証する必要がある。 -期待される動作は仕様と呼ばれ、自然言語や論理によって記述される。 -また、ソフトウェアのが期待される動作をすることを保証するためには検証をする必要が +また、ソフトウェアが期待される動作をすることを保証するためには検証を行う必要が ある。 -ソフトウェアの検証手法には定理証明とモデル検査がある。 -定理証明では。ソフトウェアが満たすべき仕様を論理式で記述し、その論理式が常に正し -いことを証明する。 -定理証明支援系には依存型で証明を行なう Agda\cite{agda} や Coq\cite{coq} などが存 -在する。 +当研究室では検証の単位として CodeGear、DataGear という単位を用いてソフトウェアを +記述する手法を提案しており、 CodeGear 、 DataGear という単位を用いてプログラミン +グする言語として Countinuation based C\cite{kaito:2015} (以下CbC)を開発している。 +CbC はC言語と似た構文を持つ言語である。 +また、 CodeGear、DataGear を用いて信頼性と拡張性をメタレベルで保証する GearsOS + CbC で開発している。 -モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が正し -いことを確認する。モデル検査器には Spin\cite{spin} や、モデルを状態遷移系で記述 -する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。 + 本研究では検証を行うために証明支援系言語 Agda を使用している。 +Agda では型で証明したい論理式を書き、その型に合った実装を記述することで証明を記 +述することができる。 + +本論文では CodeGear、DataGear での記述を Agda で表現した。 +また、GearsOS で使われている interface の記述を Agda で表現し、その記述を通して +実装の仕様の一部に対して証明を行なった。 +さらに、 Agda で継続を用いた記述をした際得られた知見や、継続と hoare logic を使っ +た今後の検証の方針を示す。 -当研究室では検証の単位として CodeGear、DataGear という単位を用いてソフトウェアを記述する手法を提案している。 -また、 CodeGear 、 DataGear という単位を用いてプログラミングする言語としてCountinuation based C\cite{kaito:2015}を開発している。Continuation based C (CbC)はC言語と似た構文を持つ言語である。 +\section{CodeGear、 DataGear} -本論文では CbC で Interface と呼ばれる記述方法を Agda で表現し、その記述を通した -実装の仕様の一部に対して証明を行なった。 +Gears OS ではプログラムとデータの単位として CodeGear、 DataGear を用いる。 Gear + は並列実行の単位、データ分割、 Gear 間の接続等になる。 +CodeGear はプログラムの処理そのもので、図\ref{cgdg}で示しているように任意の数の +Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。 +また、CodeGear は接続された DataGear 意外には参照を行わない。 -\section{CodeGear, DataGear} +CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し +た後に元のコードに戻らず、 CodeGear ないで次の CodeGear へ継続を行う。その為、 + CodeGear 、 DataGear を使ったプログラミングは末尾再帰を強制したスタイルになる。 -CodeGear、 DataGear は当研究室で提案している検証の単位である。 -処理の単位を CodeGear、処理に使うデータの単位を DataGear とし、 -CodeGear を他の CodeGear と継続することでプログラムを構成する。 -図\ref{fig:csds}のように Input DataGear を受け取り、 CodeGear で Output -DataGear に変更を加えることでプログラムを記述していく。 -% CS,DSの図 + Gear の特徴として処理やデータ構造が CodeGear、 DataGear に閉じている。このため、 + 実行時間、メモリ使用量等を予測可能にできると考えている。 + また、 GearsOS 自体もこの CodeGear、 DataGear を用いた CbC(Continuation based C +) によって実装されている。 + \begin{figure}[htpb] \begin{center} - \scalebox{0.25}{\includegraphics{pic/csds.pdf}} + \scalebox{0.3}{\includegraphics{pic/codeGear_dataGear.pdf}} \end{center} - \caption{CodeGear と DataGear} - \label{fig:csds} + \caption{CodeGear と DataGear の関係} + \label{fig:cgdg} \end{figure} +% \section{メタ計算} +% % メタ計算の論文引用どうするかな… +% % メタプログラミング~系の本とかもいれていいのかな -\section{ CbC での CodeGear、 DataGear} -CbC での簡単な記述例をソースコード\ref{code_simple}、流れを図\ref{fig:code_simple}に示 -す。CbC では CodeGear を$\_\_$code キーワードを指定する。その際、Input -DataGear は関数の引数として定義される。 CodeGear は継続で次の CodeGear -に遷移するために関数末尾で goto キーワードの後に CodeGear 名と Input -DataGear を指定する必要がある。 +% メタ計算(リフレクション)とは、対象とするレベルとメタなレベルを分離し、対象レベルでの推論や計算に +% 関するメタな情報をメタレベルで明示的に記述し操作する。 -ソースコード\ref{code_simple}では cs0、 cs1 が CodeGear で a+b が cs0 の Output DataGear であり、 -cs1 の Input DataGear である。 +% メタ計算(自己反映計算)\cite{weko_5056_1} とはプログラムを記述する際に通常の処理 +% と分離し、他に記述しなければならない処理である。例えばプログラム実行時のメモリ管 +% 理やスレッド管理、資源管理等の計算がこれに当たる。 -\begin{lstlisting}[frame=lrbt,label=code_simple,caption={CodeGear の継続の例}] -__code cg0(int a, int b){ - goto cg1(a+b); -} +% GearsOS では継続の前にメタ計算を埋め込むことで CodeGear の中身を変更することなく +% 検証を行うことができる。 -__code cg1(int c){ - goto cg2(c); -} -\end{lstlisting} - +\section{Meta Gear} +Gears OS の Code Gear は関数に比べて細かく分割されているため、メタ計算をより +柔軟に記述できる。Code Gear と Data Gear にはそれぞれメタ計算の区分として +Meta Code Gear、Meta Data Gear が存在し、これらを用いてメタ計算を実装する。 +Meta Gear は 制限された Monad に相当し、型付きアセンブラよりは大きな表現単位を +提供する。 Haskell などの関数型プログラミング言語では実行環境が複雑て +゙あり、実行時の資源使用 を明確にすることができないが、Gears OS を記述して +いる CbC はスタック上に隠され た環境を持たないので、メタ計算で使用する資源を +明確にできる利点がある。Meta Code Gear は図\ref{fig:meta-cgdg} に示すように通常の Code Gear +の直後に遷移され、メタ計算を実行する。 また、Meta Code Gear は、その階層からさら +にメタ計算を記述することが可能である。 \begin{figure}[htpb] \begin{center} - \scalebox{0.6}{\includegraphics{pic/codesegment.pdf}} + \scalebox{0.3}{\includegraphics{pic/meta_cg_dg.pdf}} \end{center} - \caption{ソースコード\ref{code_simple}の流れ} - \label{fig:code_simple} + \caption{Meta CodeGear} + \label{fig:meta-cgdg} \end{figure} -CbC の継続は、呼び出し元の情報を持たずに処理を続ける。この継続を軽量継続と呼ぶ。 -ソースコード\ref{code_simple}は cs0 から cs1 へ継続した後、 cs0 には戻らずに次の継 -続に指定された CodeGear へ継続する。 -CbC でのループ処理の記述例をソースコード\ref{factorial}、流れを図\ref{fig:factorial}に示 -す。 -軽量継続では関数呼び出しのスタックは存在しないが、ソースコード\ref{factorial}の -ように計算中の値を DataGear で持つことでループ処理を行なうこともできる。 - -\begin{lstlisting}[frame=lrbt,label=factorial,caption={階乗を求め -る CbC プログラムの例}] -__code print_factorial(int prod) -{ - printf("factorial = %d\n",prod); - exit(0); -} - -__code factorial0(int prod, int x) -{ - if ( x >= 1) { - goto factorial0(prod*x, x-1); - }else{ - goto print_factorial(prod); - } - -} - -__code factorial(int x) -{ - goto factorial0(1, x); -} +% \section{Context} +% CbC で DataGear を扱う際、 Context と呼ばれる接続可能な CodeGear、 DataGear のリ +% スト、Temporal DataGear のためのメモリ空間等を持っている Meta DataGearである。 +% CbC で必要な CodeGear 、 DataGear を参照する際は Context を通してアクセスする必 +% 要がある。 -int main(int argc, char **argv) -{ - int i; - i = atoi(argv[1]); - - goto factorial(i); -} -\end{lstlisting} - -\begin{figure}[htpb] - \begin{center} - \scalebox{0.6}{\includegraphics{pic/factorial.pdf}} - \end{center} - \caption{階乗を求める CbC プログラムの流れ} - \label{fig:factorial} -\end{figure} - -\section{メタ計算} -% メタ計算の論文引用どうするかな… -% メタプログラミング~系の本とかもいれていいのかな +% \section{stub CodeGear} +% CodeGear が必要とする DataGear を取り出す際、 Context を通す必要がある。 +% しかし、 Context を直接扱えるようにするのは信頼性を損なう。そのため CbC では +% Context を通して必要なデータを取り出して次の Code Gear に接続する stub CodeGear +% を定義している。CodeGear は stub CodeGear を介してのみ必要な DataGear へアクセス +% することができる。 stub CodeGear は CodeGear 毎に生成され、次の CodeGear へと接 +% 続される。 +% stub CodeGear は CodeGear の Meta CodeGear に当たる。 -メタ計算(リフレクション)とは、対象とするレベルとメタなレベルを分離し、対象レベルでの推論や計算に -関するメタな情報をメタレベルで明示的に記述し操作する。 - -メタ計算(自己反映計算)\cite{weko_5056_1} とはプログラムを記述する際に通常の処理 -と分離し、他に記述しなければならない処理である。例えばプログラム実行時のメモリ管 -理やスレッド管理、資源管理等の計算がこれに当たる。 - - - -% \section{Meta CodeGear とMeta DataGear} +% \section{CbCによる Interface の記述と継続} -% CbC - - -% \section{Interface} +% CodeGear は通常の関数と比べ、細かく分割されるためメタ計算をより柔軟に記述でき +% る。 CodeGear 、 DataGear にはそれぞれメタレベルとして、 Meta CodeGear +% 、 Meta DataGear が存在する。 -% Interface では使用する DataGear とそれに対する処理を行う CodeGear の集合をま -% とめて定義する。 +% CbC で実装していくうちに、stub CodeGear の記述が煩雑になることが分かった。 +% そのため 既存の実装を モジュールとして扱うため Interface を導入した。 -% \lstinputlisting[label=interface, caption=CbCでのStack-Interfaceの記述] {src/interface.cbc} - -% DataGear に対して何らかの操作(API)を行う CodeGear とその +% Interface は DataGear に対して何らかの操作(API)を行う CodeGear とその % CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear % として定義される。 -% Interface を記述することでデータ構造の api と DataGear の結びつきを高め、呼び出しが容易になる。 - - -\section{Context} -CbC で DataGear を扱う際、 Context と呼ばれる接続可能な CodeGear、 DataGear のリ -スト、Temporal DataGear のためのメモリ空間等を持っている Meta DataGearである。 -CbC で必要な CodeGear 、 DataGear を参照する際は Context を通してアクセスする必 -要がある。 - -\section{stub CodeGear} -CodeGear が必要とする DataGear を取り出す際、 Context を通す必要がある。 -しかし、 Context を直接扱えるようにするのは信頼性を損なう。そのため CbC では -Context を通して必要なデータを取り出して次の Code Gear に接続する stub CodeGear -を定義している。CodeGear は stub CodeGear を介してのみ必要な DataGear へアクセス -することができる。 stub CodeGear は CodeGear 毎に生成され、次の CodeGear へと接 -続される。 -stub CodeGear は CodeGear の Meta CodeGear に当たる。 - - -\section{CbCによる Interface の記述と継続} +% 例として CbC による Stack Interface \ref{interface-define}, +% \ref{interface}がある。Stack への push 操作に注目すると、 +% 実態は SingleLinkedStack の push であることが\ref{interface}で分 +% かる。実際の SingleLinkedStack の push では Stack を指定する必要があるが、 +% Interface で実装した Stack では push 先の Stack が stackImpl として扱 +% われている。この stackImpl は$ Stack->push $で呼ばれた時の Stack と同じになる。 +% これにより、 ユーザーは実行時に Stack を指定する必要がなくなる。 -CodeGear は通常の関数と比べ、細かく分割されるためメタ計算をより柔軟に記述でき -る。 CodeGear 、 DataGear にはそれぞれメタレベルとして、 Meta CodeGear -、 Meta DataGear が存在する。 - -CbC で実装していくうちに、stub CodeGear の記述が煩雑になることが分かった。 -そのため 既存の実装を モジュールとして扱うため Interface を導入した。 - -Interface は DataGear に対して何らかの操作(API)を行う CodeGear とその -CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear -として定義される。 +% このように Interface 記述をすることで CbC で通常記述する必要がある一定の部分を省略し呼び出 +% しが容易になる。 -例として CbC による Stack Interface \ref{interface-define}, -\ref{interface}がある。Stack への push 操作に注目すると、 -実態は SingleLinkedStack の push であることが\ref{interface}で分 -かる。実際の SingleLinkedStack の push では Stack を指定する必要があるが、 -Interface で実装した Stack では push 先の Stack が stackImpl として扱 -われている。この stackImpl は$ Stack->push $で呼ばれた時の Stack と同じになる。 -これにより、 ユーザーは実行時に Stack を指定する必要がなくなる。 +% \lstinputlisting[label=interface-define, caption=CbCでのStack-Interfaceの定義] {src/interface.cbc} -このように Interface 記述をすることで CbC で通常記述する必要がある一定の部分を省略し呼び出 -しが容易になる。 - -\lstinputlisting[label=interface-define, caption=CbCでのStack-Interfaceの定義] {src/interface.cbc} - -\lstinputlisting[label=interface, caption=CbCでのStack-Interfaceの実装] {src/singleLinkedStackInterface.cbc} +% \lstinputlisting[label=interface, caption=CbCでのStack-Interfaceの実装] {src/singleLinkedStackInterface.cbc} \section{定理証明支援器 Agda での証明} @@ -301,20 +233,6 @@ Agda はインデントに意味を持つため、きちんと揃える必要がある。 また、スペースの有無は厳格にチェックされる。 -なお、 \verb/--/ の後はコメントである。 - -Agda のプログラムでは全てモジュール内部に記述されるため、まずはトップレベルにモ -ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一になる。 - -通常のモジュールをインポートする時は \verb/import/ キーワードを指定する。 -また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。 -モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードの後に -関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠 -す場合は \verb/hiding/ キーワードを用いる。 -なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/opestack に対する操作を定義しており、n/ キーワードを使うことで展開できる。 -モジュールをインポートする例をリスト~\ref{agda-import}に示す。 - -\lstinputlisting[label=agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda} Agda における型指定は $:$ を用いて行う。 @@ -432,299 +350,6 @@ \lstinputlisting[label=agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda} - -% \section{Natural Deduction} -% % Natural Deduction のお話。細かい規則は…書かなきゃいけないよね… -% % いらない規則は省略しようと、少なくとも3段論法を証明できるだけ置く。。。？ -% % とりあえず証明に使えるやつは全部書いて必要あるやつを詳しく。 - -% Natural Deduction (自然演繹)は Gentzen によって作られた論理及びその証明システムである。 -% % ~\cite{Girard:1989:PT:64805}。 -% 命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。 - -% Natural Deduction では次のように - -% \begin{eqnarray} -% \vdots \\ \nonumber -% A \\ \nonumber -% \end{eqnarray} - -% と書いた時、命題Aを証明したことを意味する。証明は木構造で表わされ、葉の命題は仮 -% 定となる。 - -% \begin{eqnarray} -% \label{exp:a_implies_b} -% A \\ \nonumber -% \vdots \\ \nonumber -% B \\ \nonumber -% \end{eqnarray} - -% 式\ref{exp:a_implies_b}のように A を仮定して B を導いたとする。 -% この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。 - -% ここで、推論規則により記号 $ \Rightarrow $ を導入する。 - -% \begin{prooftree} -% \AxiomC{[$ A $]} -% \noLine -% \UnaryInfC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ B $ } -% \RightLabel{ $ \Rightarrow \mathcal{I} $} -% \UnaryInfC{$ A \Rightarrow B $} -% \end{prooftree} - -% $ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。 -% A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。 -% このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。 -% なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。 - -% alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。 -% それを踏まえ、 natural deduction には以下のような規則が存在する。 - -% \begin{itemize} -% \item Hypothesis - -% 仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。 - -% $ A $ - -% \item Introductions - -% 導入。証明された論理式に対して記号を導入することで新たな証明を導く。 - - -% \begin{prooftree} -% \AxiomC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ A $ } -% \AxiomC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ B $ } -% \RightLabel{ $ \land \mathcal{I} $} -% \BinaryInfC{$ A \land B $} -% \end{prooftree} - -% \begin{prooftree} -% \AxiomC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ A $ } -% \RightLabel{ $ \lor 1 \mathcal{I} $} -% \UnaryInfC{$ A \lor B $} -% \end{prooftree} - -% \begin{prooftree} -% \AxiomC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ B $ } -% \RightLabel{ $ \lor 2 \mathcal{I} $} -% \UnaryInfC{$ A \lor B $} -% \end{prooftree} - -% \begin{prooftree} -% \AxiomC{[$ A $]} -% \noLine -% \UnaryInfC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ B $ } -% \RightLabel{ $ \Rightarrow \mathcal{I} $} -% \UnaryInfC{$ A \Rightarrow B $} -% \end{prooftree} - -% \item Eliminations - -% 除去。ある論理記号で構成された証明から別の証明を導く。 - -% \begin{prooftree} -% \AxiomC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ A \land B $ } -% \RightLabel{ $ \land 1 \mathcal{E} $} -% \UnaryInfC{$ A $} -% \end{prooftree} - -% \begin{prooftree} -% \AxiomC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ A \land B $ } -% \RightLabel{ $ \land 2 \mathcal{E} $} -% \UnaryInfC{$ B $} -% \end{prooftree} - -% \begin{prooftree} -% \AxiomC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ A \lor B $ } - -% \AxiomC{[$A$]} -% \noLine -% \UnaryInfC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ C $ } - -% \AxiomC{[$B$]} -% \noLine -% \UnaryInfC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ C $ } - -% \RightLabel{ $ \lor \mathcal{E} $} -% \TrinaryInfC{ $ C $ } -% \end{prooftree} - -% \begin{prooftree} -% \AxiomC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ A $ } - -% \AxiomC{ $ \vdots $} -% \noLine -% \UnaryInfC{ $ A \Rightarrow B $ } - -% \RightLabel{ $ \Rightarrow \mathcal{E} $} -% \BinaryInfC{$ B $} -% \end{prooftree} - -% \end{itemize} - -% 記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。 -% natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。 - -% それぞれの記号は以下のような意味を持つ -% \begin{itemize} -% \item $ \land $ -% conjunction。2つの命題が成り立つことを示す。 -% $ A \land B $ と記述すると、 A かつ B と考えることができる。 - -% \item $ \lor $ -% disjunction。2つの命題のうちどちらかが成り立つことを示す。 -% $ A \lor B $ と記述すると、 A または B と考えることができる。 - -% \item $ \Rightarrow $ -% implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。 -% $ A \Rightarrow B $ と記述すると、 A ならば B と考えることができる。 -% \end{itemize} - -% Natural Deduction では、これまでで説明したような規則を使い証明を行うことができる。 - -% 例として Natural Deduction で三段論法の証明を行う。 -% このとき、「A は B であり、 B は C である。よって A は C である」 が証明するべき -% 命題である。 - -% この命題では 「A は B であり」と 「B は C である」の二つの小さい命題に分けられる。 -% この「A は B であり」から、AからBが導出できることが分かり、これは $ A \Rightarrow B $ と表せる。 -% また、「B は C である」から、BからCが導出できることが分かる。これも「A は B であ -% り」の時と同様に $ B \Rightarrow C $ と表せる。 - - -% \begin{prooftree} -% \AxiomC{ $ [A] $ $_{(1)}$} -% \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } -% \RightLabel{ $ \land 1 \mathcal{E} $ } -% \UnaryInfC{ $ (A \Rightarrow B) $ } -% \RightLabel{ $ \Rightarrow \mathcal{E} $} -% \BinaryInfC{ $ B $ } - -% \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } -% \RightLabel{ $ \land 2 \mathcal{E} $ } -% \UnaryInfC{ $ (B \Rightarrow C) $ } - -% \RightLabel{ $ \Rightarrow \mathcal{E} $} -% \BinaryInfC{ $ C $ } -% \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$} -% \UnaryInfC{ $ A \Rightarrow C $} -% \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$} -% \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $} -% \end{prooftree} - - -% Natural Deductionでは次のような証明木になる。 - - -% \begin{figure}[htpb] -% \begin{center} -% \scalebox{0.25}{\includegraphics{pic/modus-ponens.pdf}} -% \end{center} -% \caption{自然演繹での三段論法の証明} -% \label{fig:modus-ponens} -% \end{figure} - -% これにより自然演繹を使って三段論法が証明できた。 -% %%%%%%%%%%%%%%%%%%%%%% - - -% \section{Natural Deduction と 型付き $ \lambda $ 計算} - -% ここでは、 Natural Deduction と型付き$ \lambda $ 計算の対応を定義する。 -% 対応は以下の表\ref{table:curry-howard}のようになる。 - -% \begin{center} -% \begin{table}[h] -% \scalebox{0.5}{ -% \begin{tabular}{|c|c|} \hline -% Natural Deduction & 型付き $ \lambda $ 計算 \\ \hline \hline -% $ A $ & 型 A を持つ変数 x \\ \hline -% $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline -% $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline -% $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline -% $ A \land B $ & 型 A と型 B の直積型 を持つ変数 x \\ \hline -% $ \land \mathcal{I} $ & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline -% $ \land 1 \mathcal{E} $ & 直積型からの型Aを取り出す射影fst \\ \hline -% $ \land 2 \mathcal{E} $ & 直積型からの型Bを取り出す射影snd \\ \hline -% \end{tabular} -% } -% \caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)} -% \label{table:curry-howard} -% \end{table} -% \end{center} - -% この対応をもとに Agda で型付き $\lambda$ 計算による証明を示す。 -% % ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。 -% ここでも先程 Natural Deduction で証明した三段論法を例とする。 -% % この三段論法は自然演繹では\ref{fig:modus-ponens}のようになっていた。 - -% % \begin{figure}[htpb] -% % \begin{center} -% % \includegraphics{pic/modus-ponens.pdf} -% % \end{center} -% % \caption{自然演繹での三段論法の証明} -% % \label{fig:modus-ponens} -% % \end{figure} - -% %McCこの証明木に対応するAgdaによる証明はリスト\ref{agda-moduse-ponens}のようになる。 - -% \begin{lstlisting}[frame=lrbt,label=agda-moduse-ponens,caption={ Agda による -% 三段論法の定義と証明}] -% data _×_ (A B : Set) : Set where -% <_,_> : A → B → A × B - -% fst : {A B : Set} → A × B → A -% fst < a , _ > = a - -% snd : {A B : Set} → A × B → B -% snd < _ , b > = b - - -% f : {A B C : Set} → ((A → B) × (B → C)) → (A → C) -% f = λ p x → (snd p) ((fst p) x) -% \end{lstlisting} - -% 自然演繹での三段論法の証明は、1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ して導出していた。 - -% ここで $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。 -% よってこの証明は「一つの変数から fst と snd を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。 -% これをラムダ式で書くとリスト~\ref{agda-modus-ponens}のようになる。 -% 仮定 $ (A \rightarrow B) \times (B \rightarrow C) $ と仮定 A から A $ \rightarrow $ C を導いている。 - -% 仮定に相当する変数 p の型は$ (A \rightarrow B) \times (B \rightarrow C) $ であり、p からそれぞれの命題を取り出す操作が fst と snd に相当する。 -% fst p の型は $ (A \rightarrow B) $ であり、snd p の型は $ (B \rightarrow C) $ である。 -% もう一つの仮定xの型は A なので、fst p を関数適用することで B が導ける。 -% 得られた B を snd p に適用することで最終的に C が導ける。 - -% \lstinputlisting[label=agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda} - -% このように Agda でも自然演繹と同様に証明を記述できる。 - \section{Agda での CodeGear 、 DataGear 、 継続の表現} Agda と CbC を対応して CodeGear、 DataGear、 継続を Agda で表現する。 また、 Agda で継続を記述することで得た知見を示す。 @@ -732,6 +357,7 @@ DataGear はレコード型で表現できるため、 Agda のレコード型をそのまま利用して定義 していく。記述は~\ref{agda-ds}のようになる。 +% stack の DataGear の例を持ってくる \lstinputlisting[label=agda-ds, caption=Agda における DataGear の定義] {src/DataSegment.agda} @@ -764,16 +390,15 @@ CodeGear 型を受け取り、Input DataGear、 Output DataGear を返す。型になっている。 -\section{Agda での Stack、 Tree の実装} +\section{Agda での Stack、 Binary Tree の実装} ここでは Agda での Stack 、 Tree の実装を示す。 Stack の実装を以下のソースコード\ref{stack-impl}で示す。 実装は SingleLinkedStack という名前で定義されている。 -定義されている API は push を例に残りは省略する。残りのの実装は付録に示す。 %~\ +定義されている API は一部を書き、残りは省略する。 -\lstinputlisting[label=stack-impl, caption=Agdaにおける Stack の実装] {src/AgdaStackImpl.agda} - +\lstinputlisting[label=stack-impl, caption=Agdaにおける Stack の実装の一部] {src/AgdaStackImpl.agda} Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。 @@ -806,26 +431,22 @@ \section{Agda における Interface の実装} -%% 書くこと -% stack の Interface部分と redBlackTree の Interface部分。 -% interfaceとは?->cbcのとこに突っ込んでこっちは同様に〜で済ませたい - -Agda 側でも CbC 側と同様に interface を実装した。 +Agda で GearsOS のモジュール化の仕組みである interface を実装した。 +interface とは、実装と仕様を分ける記述でここでは Stack の実装を +SingleLinkedStack 、 Stack の仕様を Stack とする。 interface は record で列挙し、ソースコード~\ref{agda-interface}のように紐付けることができる。 -CbC とは異なり、 Agda では型を明記する必要があるため record 内に型を記述している。 +Agda では型を明記する必要があるため record 内に型を記述している。 -例として Agda で実装した Stack 上の interface (ソースコード\ref{agda-interface})を見る。 -Stack の実装は SingleLinkedStack(ソースコード\ref{agda-single-linked-stack}) として書かれている。それを Stack 側から -interface を通して呼び出している。 +例として Agda で実装した Stack 上の interface (ソースコード\ref{agda-interface}) +の一部を見る。 +Stack の実装は SingleLinkedStack(ソースコード\ref{agda-single-linked-stack}) として書かれている。それを Stack 側からinterface を通して呼び出している。 ここでの interface の型は Stack の record 内にある pushStack や popStack などで、 実際に使われる Stack の操作は StackMethods にある push や popである。この push や pop は SingleLinkedStack で実装されている。 -% \lstinputlisting[label=agda-single-linked-stack, caption=Agda における Stack -% の実装] {src/AgdaSingleLinkedStack.agda} - -\lstinputlisting[label=agda-interface, caption=Agda における Interface の定義] {src/AgdaInterface.agda} +\lstinputlisting[label=agda-interface, caption=Agda における Interface の定義の +一部] {src/AgdaInterface.agda} interface を通すことで、実際には Stack の push では stackImpl と何らかのデータ a を取 り、 stack を変更し、継続を返す型であったのが、 pushStack では 何らかのデータ a を取り stack を変更 @@ -844,7 +465,6 @@ % する可能性があったが、 pushStack では紐付けた Stack に push することになり \section{継続を使った Agda における Test , Debug} - Agda ではプログラムのコンパイルが通ると型の整合性が取れていることは保証できるが、必ず しも期待した動作をするとは限らない。そのため、本研究中に書いたプログラムが正しい動 作をしているかを確認するために行なった手法を幾つか示す。 @@ -871,7 +491,6 @@ と、 push した値が Stack 上から消えることなく push した順番に取り出せることが分 かる。 - また、継続を用いて記述することで関数の Test を書くことで計算途中のデータ内部をチェックするこ とができた。 @@ -934,13 +553,13 @@ る。 \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda} - + この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として 型に書かれている。 -この関数本体で返ってくる値は$ x \equiv x1 と y \equiv y1$ のため record でまと + この関数本体で返ってくる値は$ x \equiv x1$ と $y \equiv y1$ のため record でまと めて refl で推論が通る。 これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも のを受け取れることが証明できた。 @@ -948,39 +567,39 @@ % \lstinputlisting[label=agda-Test, caption=]{src/AgdaStackTest.agda} -\section{Agda による Interface 部分を含めた Binary Tree の部分的な証明と課題} -ここでは Binary Tree の性質の一部に対して証明を行う。 -Binary Tree の性質として挙げられるのは次のようなものである -% 上の２つはデータ構造として最低限守られるべき部分ではあるがとりあえず書いてる +% \section{Agda による Interface 部分を含めた Binary Tree の部分的な証明と課題} +% ここでは Binary Tree の性質の一部に対して証明を行う。 +% Binary Tree の性質として挙げられるのは次のようなものである +% % 上の２つはデータ構造として最低限守られるべき部分ではあるがとりあえず書いてる -\begin{itemize} - \item Tree に対して Node を Put することができる。 - \item Tree に Put された Node は Delete されるまでなくならない。 - \item Tree に 存在する Node とその子の関係は必ず「右の子 $>$ Node」かつ「Node $>$ 左の子」の関係になっている。 - \item どのような状態の Tree に値を put しても Node と子の関係は保たれる - \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。 -\end{itemize} +% \begin{itemize} +% \item Tree に対して Node を Put することができる。 +% \item Tree に Put された Node は Delete されるまでなくならない。 +% \item Tree に 存在する Node とその子の関係は必ず「右の子 $>$ Node」かつ「Node $>$ 左の子」の関係になっている。 +% \item どのような状態の Tree に値を put しても Node と子の関係は保たれる +% \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。 +% \end{itemize} -ここで証明する性質は +% ここで証明する性質は -${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。 +% ${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。 -\lstinputlisting[label=agda-tree-proof, caption=Tree Interface の証 -明]{src/AgdaTreeProof.agda} +% \lstinputlisting[label=agda-tree-proof, caption=Tree Interface の証 +% 明]{src/AgdaTreeProof.agda} -この Tree の証明では、不定状態の Tree を redBlackInSomeState で作成し、その状態の Tree -に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの -である。 +% この Tree の証明では、不定状態の Tree を redBlackInSomeState で作成し、その状態の Tree +% に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの +% である。 -しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した -Node が存在するのか、などの条件や、 Get した Node と Put した Node が合同なのか、 -key の値が等しい場合の eq は合同と同義であるのか等の様々な補題を証明する必要が -あった。今回この証明では Put した Node と Get した -Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合 -同であることを示すことが困難であった。 +% しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した +% Node が存在するのか、などの条件や、 Get した Node と Put した Node が合同なのか、 +% key の値が等しい場合の eq は合同と同義であるのか等の様々な補題を証明する必要が +% あった。今回この証明では Put した Node と Get した +% Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合 +% 同であることを示すことが困難であった。 -今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を -行おうと考えている。 +% 今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を +% 行おうと考えている。 \section{Hoare Logic} \label{hoare-logic} @@ -1003,7 +622,7 @@ 動きをすることを証明することができる。 この Hoare Logic の前状態、処理、後状態を CodeGear、 input/output の DataGear が表 -\ref{fig:cbc-hoare} のように表せるのではないか考えている。 +\ref{fig:cbc-hoare} のように表せると考えている。 \begin{figure}[htpb] \begin{center} @@ -1014,13 +633,35 @@ \end{figure} この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると -Pre Condition が CodeGear に入力として与えられる Input DataGear、Command が -CodeGear、 Post Condition を Output DataGear として当てはめることができると考えて -いる。 +Pre Condition は CodeGear に入力として与えられる Input DataGear として、 + Command は処理の単位である CodeGear、 Post Condition を Output DataGear として当てはめることができると考える。 + + ここでは binary tree での findNode、 replaceNode、 getRedBlackTree の流れを図 + \ref{fig:tree-hoare} で示す。 + + \begin{figure}[htpb] + \begin{center} + \scalebox{0.3}[0.3]{\includegraphics{pic/funcLoopinAutomata.pdf}} + \end{center} + \caption{binary tree での hoare logic の考え方} + \label{fig:tree-hoare} +\end{figure} + +% ここでは key に 1 の入った Node を put する際に内部で動く findNode について考え +% ている。 + +% findNode では put した key1 と同じ Node が存在するかをループしながら探していく。 +% このループ部分で invariant な変数を見つけ、それが findNode の逆の動きをする +% replaceNode で元に戻ることが分かればよい。 +% この場合辿った Node は1ループごとに Stack に積まれる。そのため、loop invariant +% は Tree と Stack で共に使っている Node の総数がまとめられた record 型の変数にな +% ると考えている。 + 今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ Agda に 当てはめ、幾つかの実装を証明していく。 + % Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。 % 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。 %%
--- a/Paper/src/AgdaInterface.agda Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/src/AgdaInterface.agda Thu Apr 19 20:28:12 2018 +0900 @@ -1,6 +1,3 @@ -open import Level renaming (suc to succ ; zero to Zero ) -module AgdaInterface where - data Maybe {n : Level } (a : Set n) : Set n where Nothing : Maybe a Just : a -> Maybe a @@ -9,10 +6,7 @@ field push : stackImpl -> a -> (stackImpl -> t) -> t pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t - pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t get : stackImpl -> (stackImpl -> Maybe a -> t) -> t - get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t - clear : stackImpl -> (stackImpl -> t) -> t open StackMethods record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where @@ -23,13 +17,6 @@ pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) popStack : (Stack a si -> Maybe a -> t) -> t popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t - pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) getStack : (Stack a si -> Maybe a -> t) -> t getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t - get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - clearStack : (Stack a si -> t) -> t - clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) - open Stack
--- a/Paper/src/AgdaInterface.agda.replaced Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/src/AgdaInterface.agda.replaced Thu Apr 19 20:28:12 2018 +0900 @@ -1,35 +1,22 @@ -open import Level renaming (suc to succ ; zero to Zero ) -module AgdaInterface where - data Maybe {n : Level } (a : Set n) : Set n where Nothing : Maybe a - Just : a @$\rightarrow$@ Maybe a + Just : a $\rightarrow$ Maybe a -record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where +record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.$\sqcup$ n) where field - push : stackImpl @$\rightarrow$@ a @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t - pop : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - pop2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - get : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - get2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - clear : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t + push : stackImpl $\rightarrow$ a $\rightarrow$ (stackImpl $\rightarrow$ t) $\rightarrow$ t + pop : stackImpl $\rightarrow$ (stackImpl $\rightarrow$ Maybe a $\rightarrow$ t) $\rightarrow$ t + get : stackImpl $\rightarrow$ (stackImpl $\rightarrow$ Maybe a $\rightarrow$ t) $\rightarrow$ t open StackMethods -record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.@$\sqcup$@ n) where +record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.$\sqcup$ n) where field stack : si stackMethods : StackMethods {n} {m} a {t} si - pushStack : a @$\rightarrow$@ (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t - pushStack d next = push (stackMethods ) (stack ) d (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } )) - popStack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - popStack next = pop (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - pop2Stack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - getStack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - getStack next = get (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - get2Stack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t - get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - clearStack : (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t - clearStack next = clear (stackMethods ) (stack ) (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } )) - + pushStack : a $\rightarrow$ (Stack a si $\rightarrow$ t) $\rightarrow$ t + pushStack d next = push (stackMethods ) (stack ) d (\s1 $\rightarrow$ next (record {stack = s1 ; stackMethods = stackMethods } )) + popStack : (Stack a si $\rightarrow$ Maybe a $\rightarrow$ t) $\rightarrow$ t + popStack next = pop (stackMethods ) (stack ) (\s1 d1 $\rightarrow$ next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) + getStack : (Stack a si $\rightarrow$ Maybe a $\rightarrow$ t) $\rightarrow$ t + getStack next = get (stackMethods ) (stack ) (\s1 d1 $\rightarrow$ next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) open Stack
--- a/Paper/src/AgdaStackImpl.agda Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/src/AgdaStackImpl.agda Thu Apr 19 20:28:12 2018 +0900 @@ -15,10 +15,7 @@ singleLinkedStackSpec = record { push = pushSingleLinkedStack ; pop = popSingleLinkedStack - ; pop2 = pop2SingleLinkedStack ; get = getSingleLinkedStack - ; get2 = get2SingleLinkedStack - ; clear = clearSingleLinkedStack } createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
--- a/Paper/src/AgdaStackImpl.agda.replaced Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/src/AgdaStackImpl.agda.replaced Thu Apr 19 20:28:12 2018 +0900 @@ -3,7 +3,7 @@ top : Maybe (Element a) open SingleLinkedStack -pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} $\rightarrow$ SingleLinkedStack Data $\rightarrow$ Data $\rightarrow$ (Code : SingleLinkedStack Data $\rightarrow$ t) $\rightarrow$ t +pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t pushSingleLinkedStack stack datum next = next stack1 where element = cons datum (top stack) @@ -11,7 +11,7 @@ -- Basic stack implementations are specifications of a Stack -singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} $\rightarrow$ StackMethods {n} {m} a {t} (SingleLinkedStack a) +singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a) singleLinkedStackSpec = record { push = pushSingleLinkedStack ; pop = popSingleLinkedStack @@ -21,7 +21,7 @@ ; clear = clearSingleLinkedStack } -createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} $\rightarrow$ Stack {n} {m} a {t} (SingleLinkedStack a) +createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a) createSingleLinkedStack = record { stack = emptySingleLinkedStack ; stackMethods = singleLinkedStackSpec
--- a/Paper/src/AgdaStackTest.agda Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/src/AgdaStackTest.agda Thu Apr 19 20:28:12 2018 +0900 @@ -1,18 +1,3 @@ -open import Level renaming (suc to succ ; zero to Zero ) -module AgdaStackTest where - -open import stack - -open import Relation.Binary.PropositionalEquality -open import Relation.Binary.Core -open import Data.Nat -open import Function - - -open SingleLinkedStack -open Stack - - -- after push 1 and 2, pop2 get 1 and 2 testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/AgdaTree.agda Thu Apr 19 20:28:12 2018 +0900 @@ -0,0 +1,22 @@ +record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where + field + putImpl : treeImpl -> a -> (treeImpl -> t) -> t + getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t +open TreeMethods + +record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where + field + tree : treeImpl + treeMethods : TreeMethods {n} {m} {a} {t} treeImpl + putTree : a -> (Tree treeImpl -> t) -> t + putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) + getTree : (Tree treeImpl -> Maybe a -> t) -> t + getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) +open Tree + +record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where + field + root : Maybe (Node a k) + nodeStack : SingleLinkedStack (Node a k) + compare : k -> k -> CompareResult {n} +open RedBlackTree
--- a/Paper/src/AgdaTreeImpl.agda Fri Apr 13 19:48:44 2018 +0900 +++ b/Paper/src/AgdaTreeImpl.agda Thu Apr 19 20:28:12 2018 +0900 @@ -30,4 +30,3 @@ ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)) --- 以下省略