Mercurial > hg > Papers > 2019 > ryokka-sigss
changeset 5:493983f2c9db
fix abstruct and more
line wrap: on
line diff
--- a/Paper/Makefile Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/Makefile Tue Dec 18 00:12:40 2018 +0900 @@ -3,7 +3,7 @@ TARGET=tecrep LATEX=platex -#BIBTEX=pbibtex +BIBTEX=pbibtex DVIPDF=dvipdfmx -p a4 #You need setting "-l" option if You think You get a landscape PDF #DVIPDF_OPT=-l @@ -15,7 +15,7 @@ .tex.dvi: $(LATEX) $< - #$(BIBTEX) $(TARGET) + $(BIBTEX) $(TARGET) $(LATEX) $< $(LATEX) $<
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/escape_agda.rb Tue Dec 18 00:12:40 2018 +0900 @@ -0,0 +1,28 @@ +#!/usr/bin/env ruby + +Suffix = '.agda.replaced' +EscapeChar = '@' +FileName = ARGV.first + +ReplaceTable = { + '->' => 'rightarrow', + '⊔' => 'sqcup', + '∷' => 'text{::}', + '∙' => 'circ', + '≡' => 'equiv', + '×' => 'times', + '⟨' => 'langle', + '⟩' => 'rangle', + '₁' => 'text{1}', + 'ℕ' => 'mathbb{N}', + '∎' => 'blacksquare', + 'λ' => 'lambda' +} + +code = File.read(FileName) +ReplaceTable.each do |k, v| + escaped_str = EscapeChar + "$\\#{v}$" + EscapeChar + code = code.gsub(k, escaped_str) +end + +File.write(FileName.sub(/.agda$/, Suffix), code)
--- a/Paper/pic/MetaGear.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/MetaGear.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./MetaGear.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/MetaGear.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 792 532 %%HiResBoundingBox: 0.000000 0.000000 792.000000 532.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/cbc-hoare.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/cbc-hoare.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./cbc-hoare.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/cbc-hoare.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 580 175 %%HiResBoundingBox: 0.000000 0.000000 580.000000 175.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/cbc-subtype.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/cbc-subtype.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./cbc-subtype.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/cbc-subtype.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 1084 281 %%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/cbc_goto.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/cbc_goto.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./cbc_goto.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/cbc_goto.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 393 201 %%HiResBoundingBox: 0.000000 0.000000 393.000000 201.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/codeGear_dataGear.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/codeGear_dataGear.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./codeGear_dataGear.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/codeGear_dataGear.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 535 427 %%HiResBoundingBox: 0.000000 0.000000 535.000000 427.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/codeGear_dataGear_dependency.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/codeGear_dataGear_dependency.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./codeGear_dataGear_dependency.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/codeGear_dataGear_dependency.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 535 247 %%HiResBoundingBox: 0.000000 0.000000 535.000000 247.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/codesegment.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/codesegment.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./codesegment.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/codesegment.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 305 85 %%HiResBoundingBox: 0.000000 0.000000 305.000000 85.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/codesegment2.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/codesegment2.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./codesegment2.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/codesegment2.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 393 201 %%HiResBoundingBox: 0.000000 0.000000 393.000000 201.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/csds.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/csds.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./csds.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/csds.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 580 76 %%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/factorial.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/factorial.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./factorial.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/factorial.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 296 220 %%HiResBoundingBox: 0.000000 0.000000 296.000000 220.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/funcLoop.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/funcLoop.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./funcLoop.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/funcLoop.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 647 168 %%HiResBoundingBox: 0.000000 0.000000 647.000000 168.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/funcLoopinAutomata.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/funcLoopinAutomata.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./funcLoopinAutomata.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/funcLoopinAutomata.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 489 473 %%HiResBoundingBox: 0.000000 0.000000 489.000000 473.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/gears-meta.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/gears-meta.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./gears-meta.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/gears-meta.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 653 243 %%HiResBoundingBox: 0.000000 0.000000 653.000000 243.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/gears_structure.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/gears_structure.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./gears_structure.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/gears_structure.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 713 418 %%HiResBoundingBox: 0.000000 0.000000 713.000000 418.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/gearsos.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/gearsos.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./gearsos.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/gearsos.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 1174 1004 %%HiResBoundingBox: 0.000000 0.000000 1174.000000 1004.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/generate_context.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/generate_context.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./generate_context.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/generate_context.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 508 408 %%HiResBoundingBox: 0.000000 0.000000 508.000000 408.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/generate_context2.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/generate_context2.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./generate_context2.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/generate_context2.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 706 355 %%HiResBoundingBox: 0.000000 0.000000 706.000000 355.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/generate_context3.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/generate_context3.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./generate_context3.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/generate_context3.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 706 274 %%HiResBoundingBox: 0.000000 0.000000 706.000000 274.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/goto.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/goto.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./goto.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/goto.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 305 85 %%HiResBoundingBox: 0.000000 0.000000 305.000000 85.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/hoare-logic.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/hoare-logic.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./hoare-logic.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/hoare-logic.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 580 76 %%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/meta-hierarchy.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/meta-hierarchy.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./meta-hierarchy.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/meta-hierarchy.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 832 283 %%HiResBoundingBox: 0.000000 0.000000 832.000000 283.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/meta.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/meta.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./meta.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/meta.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 958 148 %%HiResBoundingBox: 0.000000 0.000000 958.000000 148.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/metaCS.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/metaCS.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./metaCS.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/metaCS.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 31 511 515 732 %%HiResBoundingBox: 30.601520 511.100000 515.413800 732.012800 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/meta_cg_dg.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/meta_cg_dg.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./meta_cg_dg.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/meta_cg_dg.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 2 302 608 522 %%HiResBoundingBox: 2.019531 302.382800 608.000000 522.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/meta_gear.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/meta_gear.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./meta_gear.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/meta_gear.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 788 229 %%HiResBoundingBox: 0.000000 0.000000 788.000000 229.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/metameta.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/metameta.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./metameta.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/metameta.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 472 184 %%HiResBoundingBox: 0.000000 0.000000 472.000000 184.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/modus-ponens.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/modus-ponens.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./modus-ponens.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/modus-ponens.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 96 684 500 799 %%HiResBoundingBox: 96.082030 683.554700 499.886700 799.296900 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/non-destructive-rbtree.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/non-destructive-rbtree.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./non-destructive-rbtree.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/non-destructive-rbtree.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 559 248 %%HiResBoundingBox: 0.000000 0.000000 559.000000 248.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/persistent_date_tree.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/persistent_date_tree.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./persistent_date_tree.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/persistent_date_tree.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 773 374 %%HiResBoundingBox: 0.000000 0.000000 773.000000 374.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/persistent_date_tree_2.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/persistent_date_tree_2.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./persistent_date_tree_2.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/persistent_date_tree_2.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 736 271 %%HiResBoundingBox: 0.000000 0.000000 736.000000 271.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/put.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/put.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./put.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/put.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 868 130 %%HiResBoundingBox: 0.000000 0.000000 868.000000 130.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/rbtree.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/rbtree.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./rbtree.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/rbtree.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 562 274 %%HiResBoundingBox: 0.000000 0.000000 562.000000 274.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/ryukyu.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/ryukyu.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./ryukyu.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/ryukyu.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 595 842 %%HiResBoundingBox: 0.000000 0.000000 595.000000 842.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/subtype-arg.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/subtype-arg.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./subtype-arg.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/subtype-arg.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 1084 281 %%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/subtype-return.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/subtype-return.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./subtype-return.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/subtype-return.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 1084 281 %%HiResBoundingBox: 0.000000 0.000000 1084.000000 281.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/taskManager.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/taskManager.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./taskManager.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/taskManager.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 1021 459 %%HiResBoundingBox: 0.000000 0.000000 1021.000000 459.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/twice_640.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/twice_640.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./twice_640.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/twice_640.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 360 216 %%HiResBoundingBox: 0.000000 0.000000 360.000000 216.000000 %%PDFVersion: 1.4 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/verification.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/verification.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./verification.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/verification.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 478 204 %%HiResBoundingBox: 0.000000 0.000000 478.000000 204.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/pic/worker.xbb Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/pic/worker.xbb Tue Dec 18 00:12:40 2018 +0900 @@ -1,8 +1,8 @@ -%%Title: ./worker.pdf -%%Creator: extractbb 20180217 +%%Title: ./pic/worker.pdf +%%Creator: extractbb 20140317 %%BoundingBox: 0 0 901 644 %%HiResBoundingBox: 0.000000 0.000000 901.000000 644.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Dec 12 18:19:49 2018 +%%CreationDate: Mon Dec 17 19:16:38 2018
--- a/Paper/tecrep.tex Mon Dec 17 16:08:50 2018 +0900 +++ b/Paper/tecrep.tex Tue Dec 18 00:12:40 2018 +0900 @@ -11,7 +11,7 @@ %\usepackage[fleqn]{amsmath} %\usepackage{amssymb} \usepackage{url} - +\usepackage{cite} \usepackage{listings} \lstset{ frame=single, @@ -20,7 +20,7 @@ commentstyle={\ttfamily}, identifierstyle={\ttfamily}, keywordstyle={\ttfamily}, - basicstyle={\ttfamily}, + basicstyle=\small, breaklines=true, xleftmargin=0zw, xrightmargin=0zw, @@ -37,6 +37,8 @@ extendedchars=true, escapechar={@} } + +% basicstyle={\ttfamily}, \renewcommand{\lstlistingname}{Code} \usepackage{caption} \captionsetup[lstlisting]{font={small,tt}} @@ -71,7 +73,7 @@ \end{jabstract} \begin{jkeyword} プログラミング言語, - CbC, Gears OS, Agda + CbC, Gears OS, Agda, 検証 %% あと他…？ \end{jkeyword} %% \begin{eabstract} @@ -82,28 +84,151 @@ %% \end{ekeyword} \maketitle \section{まえがき} -% とりあえずabstをそのまま -Gears OS は継続を主とするプログラミング言語 CbC で記 -述されている。 -OS やアプリケーションの信頼性を上げるには仕様を満 -たしていることを確認する必要がある。 -現在 GearsOS の仕様の確認には定理証明系である Agda を -用いている。 -CbC では関数呼び出しを用いず goto 文により遷移する -。 -これは Agda 上では継続渡しの記述を用いた関数として +OS やアプリケーションの信頼性は重要である。 +信頼性を上げるには仕様を満たしていることを検証する必要がある。 +プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が存在している。 +HoareLogic は事前条件が成り立っているときにある +関数を実行して、それが停止する際に事後条件を満た +すことを確認することで、検証を行う。 +HoareLogic はシンプルなアプローチだが通常のプログラミング言語で使用することができず、 +広まっているとはいえない。 + +当研究室では信頼性の高い OS として GearsOS を開発している。 +現在 GearsOS ではCodeGear、DataGearという単位を用いてプログラムを記述する手法を用いており、 +仕様の確認には定理証明系である Agda を用いている。 + +CodeGearは Agda 上では継続渡しの記述を用いた関数として 記述する。 -また、継続にはある関数を実行するための事前条件や +また、継続にある関数を実行するための事前条件や 事後条件などをもたせることが可能である。 -Floyd–Hoare logic (以下 Hoare Logic) は事前条件が成り立っているときにある -関数を実行して、それが停止する際に事後条件を満た -すことを確認することで、検証を行うアイディアである。 -これは継続を用いた Agda 上では事前条件とその証明をを継続で関数 -に渡し、関数からさらに継続した先で事後条件とその証明が成り -立つという形で記述できる。 -本研究では GearsOS の仕様確認に Hoare Logic をベースと -した証明を導入し、今まで行っていた証明との比較を -行う。 + +そのため Hoare Logic と CodeGear、DataGear という単位を用いたプログラミング手法 +記述と相性が良く、既存の言語とは異なり HoareLogic を使ったプログラミングができると考えている。 + +本研究では Agda 上での HoareLogic の記述を使い、簡単なwhile Loop のプログラムを作成し、証明を行った。 +また、GearsOS の仕様確認のために CodeGear、DataGear という単位を用いた記述で Hoare Logic をベースと +したwhile Loop プログラムを記述、その証明を行なった。 + + +\section{現状} +現在の OS やアプリケーションの検証では、実装と別に検証用の言語で記述された実装と証明を持つのが一般的である。 +kernel 検証\cite{Klein:2010:SFV:1743546.1743574},\cite{Nelson:2017:HPV:3132747.3132748}の例では C で記述された Kernel に対して。 +また、別のアプローチとしては ATS や Rust などの低レベル記述向けの関数型言語を実装に用いる手法が存在している。 + +証明支援向けのプログラミング言語としては Agda、 Coq などが存在しているが、これらの言語は実行速度が期待できるものではない。 + +この現状から、証明の記述とプログラムの記述が別になっていることがネックになっているのではないかと考えている + +\section{Agda} +Adga \cite{agda} とは証明支援系言語である。 +Agdaにおける型指定は : を用いて行う。例えば、 変数 x が型 A を持つ、ということを表すには x : A と記述する。 +データ型は、代数的なデータ構造で、その定義には data キーワードを用いる。 +data キーワードの後に data の名前と、型、 where 句を書きインデントを深 くした後、 +値にコンストラクタとその型を列挙する。 Code \ref{agda-data} はこの data 型の例である。 +Comm では Skip、Abort、PComm などのコンストラクタを持ち、: の後に型が書かれている。 + +\begin{lstlisting}[caption=data の例,label=agda-data] +data Comm : Set where + Skip : Comm + Abort : Comm + PComm : PrimComm -> Comm + Seq : Comm -> Comm -> Comm + If : Cond -> Comm -> Comm -> Comm + While : Cond -> Comm -> Comm +\end{lstlisting} + +Agda には C における構造体に相当するレコード型というデータも存在する、 +record キーワード後の内部に field キーワードを記述し、その下に Name = value の形で値を列挙していく。 +複数の値を列挙する際は ; で区切る必要がある。 + Code \ref{agda-record} はレコード型の例であり、Env では varn と vari の二つの field を持ち、 +それぞれの型が Agda 上で自然数を表す Nat になっている。 + +\begin{lstlisting}[caption=record の例,label=agda-record] +record Env : Set where + field + varn : ℕ + vari : ℕ +\end{lstlisting} + +関数の定義は、関数名と型を記述した後に関数の本体を = の後に記述する。関数の型には → 、または-> を用いる。 +例えば引数が型 A で返り値が型 B の関数は A -> B のように書ける。また、複数の引数を取る関数の型は A -> A -> B のように書ける。この時の型は A -> (A -> B) のように考えられる。 +ここでは Code \ref{agda-function}を例にとる。これは引き算の演算子で、Agda の Nat を二つ引数に受けて Nat を返す +関数である。 + +\begin{lstlisting}[caption=関数の例,label=agda-function] +_-_ : ℕ → ℕ → ℕ +x - zero = x +zero - _ = zero +(suc x) - (suc y) = x - y +\end{lstlisting} + +Agda での証明では型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明が完成する。 +証明の例として Code \ref{proof} を見る。 +ここでの $+zero$ は右から zero を足しても $\equiv$ の両辺は等しいことを証明している。 +これは、引数として受けている y が Nat なので、 zero の時と suc y の二つの場合を証明する必要がある。 + +$y = zero$ の時は両辺が zero とできて、左右の項が等しいということを表す refl で証明することができる。 +$y = suc y$ の時は x == y の時 fx == fy が成り立つという cong を使って、y の値を 1 減らしたのちに再帰的に $+zero y$ +を用いて証明している。 +\begin{lstlisting}[caption=等式変形の例,label=proof] ++zero : { y : ℕ } → y + zero ≡ y ++zero {zero} = refl ++zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) +\end{lstlisting} + +また、他にも $\lambda$ 項部分で等式を変形する構文が存在している。 + Code \ref{agda-term-pre}、 \ref{agda-term-post} は等式変形の例である。 +始めに等式変形を始めたいところで $let open \equiv-Reasoning in begin$と記述する。 +Agda 上では分からないところを ? と置いておくことができるので、残りを ? としておく。 +$--$ は Agda 上ではコメントである。 + +\begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre] +stmt2Cond : {c10 : ℕ} → Cond +stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) + +lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ +10}) +lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + ? -- ?0 + ≡⟨ ? ⟩ -- ?1 + ? -- ?2 + ∎ ) + +-- ?0 : Bool +-- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) ≡ true +-- ?2 : Bool +\end{lstlisting} + +この状態で Compile すると ? 部分に入る型を Agda が示してくれるため、始めに変形する等式を ?0 に +記述し、?1 の中に $x == y$ のような変形規則を入れることで等式を変形して証明することができる。 + +ここでは \ref{agda-term-mid} の Bool 値 x を受け取って $x \wedge true$ の時必ず x であるという証明 $\wedge$true と 値と Env を受け取って Bool 値を返す stmt1Cond を使って等式変形を行う。 +\begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid] +∧true : { x : Bool } → x ∧ true ≡ x +∧true {x} with x +∧true {x} | false = refl +∧true {x} | true = refl + +stmt1Cond : {c10 : ℕ} → Cond +stmt1Cond {c10} env = Equal (varn env) c10 +\end{lstlisting} + +最終的な証明は\ref{agda-term-post} のようになる。 + +\begin{lstlisting}[caption=等式変形の例3/3,label=agda-term-post] +lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ +10}) +lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + (Equal (varn env) c10 ) ∧ true + ≡⟨ ∧true ⟩ + Equal (varn env) c10 + ≡⟨ cond ⟩ + true + ∎ ) +\end{lstlisting} + \section{GearsOS} Gears OS は信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に開発している OSである。 @@ -111,16 +236,15 @@ Gears OS は処理の単位を Code Gear、データの単位を Data Gear と呼ばれる単位でプログラムを構成する。 信頼性や拡張性はメタ計算として、通常の計算とは区別して記述する。 - \section{CodeGearとDataGear} - Gears OS ではプログラムとデータの単位として CodeGear、 DataGear を用いる。 Gear は並列実行の単位、データ分割、 Gear 間の接続等になる。 -CodeGear はプログラムの処理そのもので、図\ref{fig:cgdg}で示しているように任意の数の +CodeGear はプログラムの処理そのもので、図 Code \ref{fig:cgdg}で示しているように任意の数の Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。 CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し -た後に元のコードに戻らず、次の CodeGear へ継続を行う。これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。 +た後に元のコードに戻らず、次の CodeGear へ継続を行う。 +これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。 Gear では処理やデータ構造が CodeGear、 DataGear に閉じている。したがって、 DataGear は Agda のデータ構造(data と record)で表現できる。 @@ -128,88 +252,59 @@ \begin{figure}[htpb] \begin{center} - \scalebox{0.3}{\includegraphics{pic/codeGear_dataGear.pdf}} + \scalebox{0.25}{\includegraphics{pic/meta_cg_dg.pdf}} \end{center} \caption{CodeGear と DataGear の関係} \label{fig:cgdg} \end{figure} また Gears OS 自体もこの Code Gear、Data Gear を用いた CbC(Continuation based C) で実装される。 -そのため、Gears OS の実装は Code Gear、Data Gear を用いたプログラミングスタイルの指標となる。 - -\section{Agda} - +そのため、Gears OS の実装は Gears を用いたプログラミングスタイルの指標となる。 \section{CbC と Agda} %% CbC の CodeGear, DataGear を用いたプログラミングスタイルと Agda での対応 -ここでは CodeGear、DataGear を用いたプログラムを検証するため、 +ここでは Gears を用いたプログラムを検証するため、 Agda 上での CodeGear、 DataGear の対応をみていく。 - CodeGear は Agda では継続渡しで書かれた関数と等価である。 継続は不定の型 (\verb+t+) を返す関数で表される。 CodeGear 自体も同じ型 \verb+t+ を返す関数となる。 -例えば、 Stack への push を行う関数 pushStack は以下のような型を持つ。 + Code \ref{agda-gc}は Agda で書いた CodeGear の型の例である。 -\begin{lstlisting}[caption=pushStack の型,label=push-stack] - pushStack : a -> (Stack a si -> t) -> t +\begin{lstlisting}[caption= whileTest の型,label=agda-cg] +whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) → (Code : Env -> t) -> t +whileTest c10 next = next (record {varn = c10 ; vari = 0} ) \end{lstlisting} -\verb+pushStack+ が関数名で、コロンの後ろに型を記述する。 -最初の引数は Stack に格納される型\verb+a+ を持つ。 -二つ目の引数は継続であり、\verb+Stack a si+ (\verb+si+という実装を持つ\verb+a+を格納するStack)を受け取り不定の型\verb+t+を返す関数である。 -この CodeGear 自体は不定の型\verb+t+を返す。 GearsOS で CodeGear の性質を証明するには、 Agda で記述された CodeGear と -DataGear に対してメタ計算として証明を行う。証明すべき性質は、不定の型を持つ継続 -\verb+t+ に記述することができる。例えば、 Stack にある値\verb+x+をpushして、pop -すると \verb+ x'+ が取れてくる。\verb+Just x+ と\verb+Just x'+ は等しい必要があ -る。これは Agda では \verb+(Just x ≡ x')+ と記述される。 -ここで Just とは Agda の以下のデータ構造である。 +DataGear に対して証明を行う。証明すべき性質は、不定の型を持つ継続 +\verb+t+ に記述することができる。 +例えば、 Code \ref{gears-proof} では $(vari e) ≡ 10 $ が証明したい命題で、whileTest +から、whileLoop の CodeGear に継続した後、この命題が正しければよい。 +この証明は proof1 の型に対応する$\lambda$項を与えると証明が完了したことになる。 +ここで与えている refl は x==x で、命題が正しいことが証明できている。 % \begin{verbatim} -\begin{lstlisting}[caption=data型の例:Maybe,label=maybe] -data Maybe {n : Level } (a : Set n) : Set n where - Nothing : Maybe a - Just : a -> Maybe a +\begin{lstlisting}[caption=Agda での証明の例,label=gears-proof] +proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) +proof1 = refl \end{lstlisting} % \end{verbatim} -これは DataGear に相当し、\verb+Nothing+ と \verb+Just+ の二つの状態を保つ。 -pop した時に、 Stack が空であれば\verb+Nothing+ を返し、そうでなければ\verb+Just+ のついた返り値を返す。 - -この性質を Agda で表すと、以下のような型になる。 -Agda では証明すべき論理式は型で表される。 -継続部分に直接証明すべき性質を型として記述できる。 -Agda ではこの型に対応する$\lambda$項を与えると証明が完了したことになる。 - -\begin{lstlisting}[caption=pushとpop,label=push-pop] -push->pop : {l : Level} {D : Set l} (x : D ) - (s : SingleLinkedStack D) -> - pushStack (stackInSomeState s) - x (\s -> popStack s - ( \s3 x1 -> (Just x ≡ x1))) -\end{lstlisting} - -このように、CodeGear を Agda で記述し、継続部分に証明すべき性質を Agda で記述する。 +%% \section{HoareLogic} +%% %% HoareLogic の説明と Commands、 Rules の説明。公理としてのものなのですべて説明。 -%% GearsOS での記述は interface によってモジュール化される。 -%% よって、このモジュール化もAgda により記述する必要がある。 -%% CbC で記述された任意の CodeGear と Meta CodeGear が Agda にそのまま変換されるわけではないが、変換可能なように記述されると仮定する。 - -\section{HoareLogic} -%% HoareLogic の説明と Commands、 Rules の説明。公理としてのものなのですべて説明。 +%% HoareLogic とは C.A.R Hoare、 R.W Floyd らによるプログラムの検証のアイディアである。 +%% これはプログラムの部分的な正当性を検証するアイディアで、 +%% 事前条件(Pre-Condition) P が成り立つとき、コマンド C を実行した後に +%% 事後条件(Post-Condition) Q が成り立つ。 +%% これを ${P} C {Q}$ のように表し、コマンドをつなげてプログラム全体を記述することで、 +%% プログラム内のすべての部分について検証を行うことができる。 +%% %% これは、プログラムを Skip、 Abort、 Seq、 PComm、 If、 While の6つの規則で記述することで -HoareLogic とは C.A.R Hoare、 R.W Floyd らによるプログラムの検証のアイディアである。 -これはプログラムの部分的な正当性を検証するアイディアで、 -事前条件(Pre-Condition) P が成り立つとき、コマンド C を実行した後に -事後条件(Post-Condition) Q が成り立つ。 -これを ${P} C {Q}$ のように表し、コマンドをつなげてプログラム全体を記述することで、 -プログラム内のすべての部分について検証を行うことができる。 -%% これは、プログラムを Skip、 Abort、 Seq、 PComm、 If、 While の6つの規則で記述することで - -HoareLogic ではプログラムを Assign、 Sequential Composition、 If、 While というコマンドで -記述する。 +%% HoareLogic ではプログラムを Assign、 Sequential Composition、 If、 While というコマンドで +%% 記述する。 %% Skip は動作をしないコマンドで事前条件や事後条件に変化を与えない。 %% About は途中で処理を中断するコマンドで Skip と同様、条件に変化を与えることはない。 @@ -219,8 +314,10 @@ \section{AgdaでのHoareLogic} -本章では、Agda 上での HoareLogic についての記述と検証を行う。 -今回は、\ref{agda-while} のような while Loop に対しての検証を行うこととする。 + +% Agda 上での HoareLogic についての記述と検証を行う。 + +今回は、 Code \ref{agda-while} のような while Loop に対しての検証を行う。 \begin{lstlisting}[caption=while Loop,label=agda-while] n = 10; @@ -233,20 +330,34 @@ } \end{lstlisting} -\ref{agda-while}では最初期の事前条件は何もなく、プログラムが停止するときの条件として、 $i==10 ∧ n == 0$ が成り立つ。 -また、 $n = 10$、 $i = 0$、 といった代入に事前条件と、事後条件をつけ、 while文 にループの普遍条件をつけることになる。 + Code \ref{agda-while}では最初期の事前条件は何もなく、プログラムが停止するときの条件として、 $i==10 ∧ n == 0$ が成り立つ。 +また、 $n = 10$、 $i = 0$、 といった代入に事前条件と、事後条件をつけ、 while 文にループの普遍条件をつけることになる。 -\ref{agda-hoare} は Agda上での HoareLogic の構築子である。 +現在 Agda 上での HoareLogic は初期の Agda で実装されたもの \cite{agda-alpa}とそれを現在のAgdaに対応させたもの \cite{agda2-hoare}が存在している。 + +今回は現在のAgdaに対応させたもの \cite{agda2-hoare}の Command と証明のためのルールを使って HoareLogic を実装した。 + Code \ref{agda-hoare} は Agda上での HoareLogic の構築子である。 +ここでの Comm は Agda2 に対応した Command の定義をそのまま使っている。 -$Env$ は\ref{agda-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。 +% Code \ref{agda-alfa} \cite{agda2-hoare} +$Env$ は Code \ref{agda-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。 + PrimComm は Primitive Command で、 n、i といった変数に 代入するときに使用される関数である。 -Cond は Condition で、 変数を受け取って Bool値を返す関数となっている。 + +Cond は HoareLogic の Condition で、 Env を受け取って Bool 値を返す関数となっている。 + + Agda のデータで定義されている Comm は HoareLogic での Command を表す。 + Skip は何も変更しない Command で、 Abort はプログラムを中断する Command である。 -PComm は PrimComm を受けて Command を返す型で定義されていて、 変数を代入するときに使われる。 -Seq は Sequence Composition で Command を2つ受けて Command を返す型で定義されている。これは、ある Command から Command に移り、その結果を次の Command に渡す型になっている。 -If は Cond と Comm を2つ受け取り、 Cond の中身によって Comm を変える Command である。 +PComm は PrimComm を受けて Command を返す型で定義されており、 変数を代入するときに使われる。 + +Seq は Sequence で Command を2つ受けて Command を返す型で定義されている。 +これは、ある Command から Command に移り、その結果を次の Command に渡す型になっている。 + +If は Cond と Comm を2つ受け取り、 Cond が true か false かで 実行する Comm を変える Command である。 + While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。 \begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare] @@ -273,10 +384,10 @@ Agda 上の HoareLogic で使われるプログラムは Comm 型の関数となる。 プログラムの処理を Seq でつないでいき、最終的な状態にたどり着くと値を返して止まる。 -%% \ref{agda-hoare-simpl} は 変数 $i$、 $n$ に代入を行うプログラムである。 +%% Code \ref{agda-hoare-simpl} は 変数 $i$、 $n$ に代入を行うプログラムである。 %% これは Seq で PComm を2つ繋げた形になる。 -\ref{agda-hoare-prog}は\ref{agda-while}で書いた While Loop を HoareLogic での Comm で記述したものである。 -ここでの $\$$は $()$の対応を合わせる Agda の糖衣で、行頭から行末までを $()$で囲っていることと同義である。 + Code \ref{agda-hoare-prog}は Code \ref{agda-while}で書いた While Loop を HoareLogic での Comm で記述したものである。 +ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。 \begin{lstlisting}[caption= HoareLogic のプログラム ,label=agda-hoare-prog] program : Comm @@ -286,11 +397,11 @@ $ While (λ env → lt zero (varn env ) ) (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) $ PComm (λ env → record env {varn = ((varn env) - 1)} )) - \end{lstlisting} -しかし、 この Comm は Command をならべているだけである。 -そのため、この Command を Agda 上で実行するため、 \ref{agda-hoare-interpret} のような interpreter を記述した。 +この Comm は Command をならべているだけである。 +この Comm を Agda 上で実行するため、 Code \ref{agda-hoare-interpret} のような interpreter を記述した。 + \begin{lstlisting}[caption=Agda での HoareLogic interpreter ,label=agda-hoare-interpret] {-# TERMINATING #-} interpret : Env → Comm → Env @@ -306,19 +417,51 @@ ... | false = env \end{lstlisting} -\ref{agda-hoare-interpret}は 初期状態の Env と 実行する Command の並びを受けとって、実行後の Env を返すものとなっている。 + Code \ref{agda-hoare-interpret}は 初期状態の Env と 実行する Command の並びを受けとって、実行後の Env を返すものとなっている。 \begin{lstlisting}[caption=Agda での HoareLogic の実行 ,label=agda-hoare-run] test : Env -test = interpret ( record { vari = 0 ; varn = 0 } ) programt +test = interpret ( record { vari = 0 ; varn = 0 } ) program \end{lstlisting} -\ref{agda-hoare-run}のように interpret に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価してやると$record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。 + + Code \ref{agda-hoare-run}のように interpret に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価してやると$record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。 次に先程書いたプログラムの証明について記述する。 -\ref{agda-hoare-rule} は Agda 上での HoareLogic での証明の構成である。 + Code \ref{agda-hoare-rule} は Agda 上での HoareLogic での証明の構成である。 HTProof では Condition と Command もう一つ Condition を受け取って、 Set を返す Agda のデータである。 -- これは Pre と Post の Condition を Command で変化させる +ここでの HTProof \cite{agda2-hoare} も Agda2 に移植されたものを使っている。 + +PrimRule は Code \ref{axiom-taut} の Axiom という関数を使い、事前条件が成り立っている時、 +実行後に事後条件が成り立つならば、 PComm で変数に値を代入できることを保証している。 + +SkipRule は Condition を受け取ってそのままの Condition を返すことを保証する。 + +AbortRule は PreContition を受け取って、Abort を実行して終わるルールである。 + +WeakeningRule は \ref{axiom-taut} の Tautology という関数を使って通常の逐次処理から、 +WhileRule のみに適応されるループ不変変数に移行する際のルールである。 + +SeqRule は3つの Condition と 2つの Command を受け取り、これらのプログラムの逐次的な実行を保証する。 + +IfRule は分岐に用いられ、3つの Condition と 2つの Command を受け取り、判定の Condition が成り立っているかいないかで実行する Command を変えるルールである。 +この時、どちらかの Command が実行されることを保証している。 + +WhileRule はループに用いられ、1つの Command と２つの Condition を受け取り、事前条件が成り立っている間、 Command を繰り返すことを保証している。 + +\begin{lstlisting}[caption=Axiom と Tautology,label=axiom-taut] +_⇒_ : Bool → Bool → Bool +false ⇒ _ = true +true ⇒ true = true +true ⇒ false = false + +Axiom : Cond -> PrimComm -> Cond -> Set +Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true + +Tautology : Cond -> Cond -> Set +Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true +\end{lstlisting} \begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare-rule] data HTProof : Cond -> Comm -> Cond -> Set where @@ -350,28 +493,45 @@ HTProof bInv (While b cm) (bInv /\ neg b) \end{lstlisting} -\ref{agda-hoare-rule}を使って先程の while Program を証明する。 -証明は \ref{agda-hoare-rule}の proof1 の様になる。 +Code \ref{agda-hoare-rule}を使って Code \ref{agda-while}の whileProgram を証明する。 -\begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while] + +\begin{lstlisting}[caption=whileProgram Condition, label=while-cond] initCond : Cond initCond env = true -stmt1Cond : Cond -stmt1Cond env = Equal (varn env) 10 +stmt1Cond : {c10 : ℕ} → Cond +stmt1Cond {c10} env = Equal (varn env) c10 + +init-case : {c10 : ℕ} → (env : Env) → (( λ e → true ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari \ += vari env }) ) ≡ true +init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl ) -stmt2Cond : Cond -stmt2Cond env = (Equal (varn env) 10) ∧ (Equal (vari env) 0) +init-type : {c10 : ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Co\ +nd {c10}) +init-type {c10} env = init-case env + +stmt2Cond : {c10 : ℕ} → Cond +stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) -whileInv : Cond -whileInv env = Equal ((varn env) + (vari env)) 10 +whileInv : {c10 : ℕ} → Cond +whileInv {c10} env = Equal ((varn env) + (vari env)) c10 + +whileInv' : {c10 : ℕ} → Cond +whileInv' {c10} env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env) -whileInv' : Cond -whileInv' env = Equal ((varn env) + (vari env)) 11 +termCond : {c10 : ℕ} → Cond +termCond {c10} env = Equal (vari env) c10 +\end{lstlisting} -termCond : Cond -termCond env = Equal (vari env) 10 - +証明は Code \ref{agda-hoare-while}の proof1 の様になる。 +proof1 では型で initCond、 Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、 +initCond から program を実行し termCond に行き着く HoareLogic の証明になっている。 + +lemma1 から lemma5 は Code \ref{agda-hoare-while-lemma} の通りで、 +lemma1 が + +\begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while] proof1 : HTProof initCond program termCond proof1 = SeqRule {λ e → true} ( PrimRule empty-case ) @@ -382,49 +542,228 @@ $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 \end{lstlisting} -proof1 は\ref{agda-hoare-prog}の program と似た形をとっている。 -Comannd に対応する証明規則があるため、証明はプログラムに対応する形になる。 +%% \begin{lstlisting}[caption=proof1 の lemma ,label=agda-hoare-while-lemma] +%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) +%% (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) +%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in +%% begin +%% (Equal (varn env) c10 ) ∧ true +%% ≡⟨ ∧true ⟩ +%% Equal (varn env) c10 +%% ≡⟨ cond ⟩ +%% true +%% ∎ ) -\begin{lstlisting}[caption=Gears 上での WhileLoop の検証,label=Gears-hoare-while] +%% lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10 +%% lemma21 eq = Equal→≡ (∧-pi1 eq) +%% lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0 +%% lemma22 eq = Equal→≡ (∧-pi2 eq) +%% lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10 +%% lemma23 {env} {c10} eq = let open ≡-Reasoning in +%% begin +%% varn env + vari env +%% ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩ +%% c10 + vari env +%% ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩ +%% c10 + 0 +%% ≡⟨ +-sym {c10} {0} ⟩ +%% 0 + c10 +%% ≡⟨⟩ +%% c10 +%% ∎ +%% lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv +%% lemma2 {c10} env = bool-case (stmt2Cond env) ( +%% λ eq → let open ≡-Reasoning in +%% begin +%% (stmt2Cond env) ⇒ (whileInv env) +%% ≡⟨⟩ +%% (stmt2Cond env) ⇒ ( Equal (varn env + vari env) c10 ) +%% ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩ +%% (stmt2Cond env) ⇒ (Equal c10 c10) +%% ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl ) ⟩ +%% (stmt2Cond {c10} env) ⇒ true +%% ≡⟨ ⇒t ⟩ +%% true +%% ∎ +%% ) ( +%% λ ne → let open ≡-Reasoning in +%% begin +%% (stmt2Cond env) ⇒ (whileInv env) +%% ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩ +%% false ⇒ (whileInv {c10} env) +%% ≡⟨ f⇒ {whileInv {c10} env} ⟩ +%% true +%% ∎ +%% ) +%% lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' +%% lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in +%% begin +%% whileInv' (record { varn = varn env ; vari = vari env + 1 }) +%% ≡⟨⟩ +%% Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) ) +%% ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond ) ⟩ +%% Equal (varn env + (vari env + 1)) (suc c10) ∧ true +%% ≡⟨ ∧true ⟩ +%% Equal (varn env + (vari env + 1)) (suc c10) +%% ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩ +%% Equal ((varn env + vari env) + 1) (suc c10) +%% ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩ +%% Equal (suc (varn env + vari env)) (suc c10) +%% ≡⟨ sym Equal+1 ⟩ +%% Equal ((varn env + vari env) ) c10 +%% ≡⟨ ∧-pi1 cond ⟩ +%% true +%% ∎ ) +%% lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true +%% lemma41 env {c10} c1 c2 = let open ≡-Reasoning in +%% begin +%% Equal ((varn env - 1) + vari env) c10 +%% ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-predℕ=n c2) ) ⟩ +%% Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10 +%% ≡⟨⟩ +%% Equal ((predℕ {varn env} c2 ) + vari env) c10 +%% ≡⟨ Equal+1 ⟩ +%% Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10) +%% ≡⟨ cong ( λ z → Equal (z + vari env ) (suc c10) ) (suc-predℕ=n c2 ) ⟩ +%% Equal (varn env + vari env) (suc c10) +%% ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩ +%% Equal (suc c10) (suc c10) +%% ≡⟨ ≡→Equal refl ⟩ +%% true +%% ∎ +%% lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv +%% lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in +%% begin +%% whileInv (record { varn = varn env - 1 ; vari = vari env }) +%% ≡⟨⟩ +%% Equal ((varn env - 1) + vari env) c10 +%% ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩ +%% true +%% ∎ +%% ) +%% lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero +%% lemma51 z cond with lt zero (varn z) | (suc zero) ≤? (varn z) +%% lemma51 z () | false | yes p +%% lemma51 z () | true | yes p +%% lemma51 z refl | _ | no ¬p with varn z +%% lemma51 z refl | _ | no ¬p | zero = refl +%% lemma51 z refl | _ | no ¬p | suc x = ⊥-elim ( ¬p (s≤s z≤n ) ) +%% lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond +%% lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in +%% begin +%% termCond env +%% ≡⟨⟩ +%% Equal (vari env) c10 +%% ≡⟨⟩ +%% Equal (zero + vari env) c10 +%% ≡⟨ cong ( λ z → Equal (z + vari env) c10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩ +%% Equal (varn env + vari env) c10 +%% ≡⟨ ∧-pi1 cond ⟩ +%% true +%% ∎ +%% ) +%% \end{lstlisting} +proof1 は Code \ref{Agda-hoare-prog}の program と似た形をとっている。 +HoareLogic では Comannd に対応する証明規則があるため、証明はプログラムに対応する形になる。 + +\section{Gears ベースの HoareLogic の証明} +次に Gears をベースにした HoareLogic の例を見ていく。 +Gears を用いた記述では、 Input の DataGear 、 CodeGear、 Output の DataGearという +並びでプログラムを記述していく。 +そのため、Input DataGear を PreCondition、 Command を CodeGear、 Output DataGear を PostCondition と +そのまま置き換えることができる。 + +こちらも通常の HoareLogic と同様に \ref{agda-while} のwhileプログラムと同様のものを記述する +Code \ref{Gears-hoare-while} は、 CodeGear、 DataGear を用いた Agda 上での while Program の記述であり、証明でもある。 + +\begin{lstlisting}[caption=Gears 上での WhileLoop の記述と検証,label=Gears-hoare-while] proofGears : {c10 : ℕ } → Set -proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) +proofGears {c10} = whileTest {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) +\end{lstlisting} +Code \ref{Gears-hoare-while} で使われている CodeGear を見ていく + +始めに Code \ref{gears-while} の whileTest では変数 i、n にそれぞれ 0 と 10 を代入している。 +whileTest は最初のCodeGear なので initCondition は true で、 +Code : の後ろに書かれた$(env : Env) -> ((vari env) ≡ 0) /\ ((varn env) ≡ c10)$ が PostCondition である。 +$\lambda$ 項の next には次のCodeGear が入り、継続される引数である env は whileTest の PostCondition であり、 +次の CodeGear の PreCondition にあたる。 +conversion1 は通常の Condition からループ不変条件に移行するためのもので前のCondition である $i == 0 and n == 10$ が +成り立っている時、$i + n == 10$ を返すCodeGear となっている。 +whileLoop では conversion1 のループ不変条件を受け取ってWhile の条件である$0 < n$ が成り立っている間、 $i++;n++$ +を行う。 +そして、ループを抜けた後の termCondition は $i == 10$ となる。 + +\begin{lstlisting}[caption=Gears whileProgram, label=gears-while] +whileTest : {l : Level} {t : Set l} -> {c10 : ℕ } → (Code : (env : Env) -> + ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t +whileTest {_} {_} {c10} next = next env proof2 + where + env : Env + env = record {vari = 0 ; varn = c10} + proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) + proof2 = record {pi1 = refl ; pi2 = refl} -proofGearsMeta : {c10 : ℕ } → whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1(λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) -proofGearsMeta {c10} = {!!} +conversion1 : {l : Level} {t : Set l } → (env : Env) -> {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c\ +10) + -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ c10) -> t) -> t +conversion1 env {c10} p1 next = next env proof4 + where + proof4 : varn env + vari env ≡ c10 + proof4 = let open ≡-Reasoning in + begin + varn env + vari env + ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ + c10 + vari env + ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ + c10 + 0 + ≡⟨ +-sym {c10} {0} ⟩ + c10 + ∎ + +{-# TERMINATING #-} +whileLoop : {l : Level} {t : Set l} -> (env : Env) -> {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) -> (Co\ +de : Env -> t) -> t +whileLoop env proof next with ( suc zero ≤? (varn env) ) +whileLoop env proof next | no p = next env +whileLoop env {c10} proof next | yes p = whileLoop env1 (proof3 p ) next + where + env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} + 1<0 : 1 ≤ zero → ⊥ + 1<0 () + proof3 : (suc zero ≤ (varn env)) → varn env1 + vari env1 ≡ c10 + proof3 (s≤s lt) with varn env + proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p) + proof3 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in + begin + n' + (vari env + 1) + ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩ + n' + (1 + vari env ) + ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩ + (n' + 1) + vari env + ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩ + (suc n' ) + vari env + ≡⟨⟩ + varn env + vari env + ≡⟨ proof ⟩ + c10 + ∎ \end{lstlisting} -\begin{thebibliography}{99} -%\bibitem{ohno} -%大野義夫編，\TeX\ 入門， -%共立出版，東京，1989. -%\bibitem{Seroul} -%R. Seroul and S. Levy, A Beginner's Book of \TeX, -%Springer-Verlag, New York, 1989. - -%\bibitem{nodera1} -%野寺隆志，楽々\LaTeX{}， -%共立出版，東京，1990. - -%\bibitem{itou} -%伊藤和人，\LaTeX\ トータルガイド， -%秀和システムトレーディング，1991. +\section{まとめと今後の課題} +本研究では Agda 上で HoareLogic のwhileを使った例題を作成し、 +証明を行なった。 -%\bibitem{nodera2} -%野寺隆志，今度こそ\AmSLaTeX{}， -%共立出版，東京，1991. - -\bibitem{ryokka-sigos} -外間政尊, 河野真治, GearsOSのAgdaによる記述と検証， -\\システムソフトウェアとオペレーティング・システム研究会, 2018. +また、 Gears を用いた HoareLogic を記述することができた。 +さらに、Gears を用いてHoareLocic 記述で、 +証明を引数として受け渡して記述し、証明とプログラムを一体化することができた。 -%% \bibtem{agda-alfa} -%% \url{http://ocvs.cfv.jp/Agda/} +今後の課題としては GearsOS の検証のために、 +RedBlackTree や SynchronizedQueue などのデータ構造の検証をHoareLogic ベースで行うことなどが挙げられる。 +%% 特に SynchronizedQueue の検証のために、 並列なプログラムを状態遷移に変換する。 -%% \bibtem{agda2-hoare} -%% \url{https://github.com/IKEGAMIDaisuke/HoareLogic} - - -\end{thebibliography} +\nocite{*} +\bibliography{tecrep}{} +\bibliographystyle{plain} \end{document}
--- a/ryokka-sigss.mm Mon Dec 17 16:08:50 2018 +0900 +++ b/ryokka-sigss.mm Tue Dec 18 00:12:40 2018 +0900 @@ -117,5 +117,61 @@ <node CREATED="1544952979891" ID="ID_1616071429" MODIFIED="1544952986481" TEXT="まとめ"/> </node> <node CREATED="1542710960435" ID="ID_167048397" MODIFIED="1542710984521" POSITION="right" TEXT="研究"/> +<node CREATED="1545030891993" ID="ID_424599902" MODIFIED="1545030897348" POSITION="left" TEXT="研究目的"> +<node CREATED="1545031695286" ID="ID_1807380852" MODIFIED="1545031828376" TEXT="OS やアプリケーションの信頼性をあげたい"/> +<node CREATED="1545031829304" ID="ID_848338957" MODIFIED="1545031877618" TEXT="プログラム自体のバグがないことが重要"/> +<node CREATED="1545031881555" ID="ID_1890176001" MODIFIED="1545031901586" TEXT="大半のバグは簡単なものである"/> +<node CREATED="1545031915332" ID="ID_1766422576" MODIFIED="1545031926012" TEXT="本来なら当たり前に見つかるエラーを簡単に見つけたい"/> +<node CREATED="1545031934733" ID="ID_819406039" MODIFIED="1545031952333" TEXT="プログラムの証明には HoareLogic が存在する"/> +<node CREATED="1545031953430" ID="ID_189897321" MODIFIED="1545031992503" TEXT="プログラミングの方法論自体に HoareLogic を組み込むアプローチ"/> +<node CREATED="1545031995576" ID="ID_455588060" MODIFIED="1545032022728" TEXT="そのためには既存のプログラミング言語ではダメなのかもしれない"/> +<node CREATED="1545032024743" ID="ID_862300550" MODIFIED="1545032052066" TEXT="HoareLogic が広まらない理由"> +<node CREATED="1545032068115" ID="ID_1062003354" MODIFIED="1545032100996" TEXT="既存の言語には HoareLogic を書く場所がない"/> +<node CREATED="1545032104901" ID="ID_298160802" MODIFIED="1545032113668" TEXT="不当に難しいと思われている"> +<node CREATED="1545032129477" ID="ID_952723861" MODIFIED="1545032134998" TEXT="格調高い"/> +</node> +</node> +<node CREATED="1545032140487" ID="ID_1131641415" MODIFIED="1545032158255" TEXT="簡単なエラーを見つけるための証明が難しいはずはない"/> +<node CREATED="1545032159792" ID="ID_1116096354" MODIFIED="1545032164071" TEXT="簡単なものから始める"/> +<node CREATED="1545032299337" ID="ID_1249663292" MODIFIED="1545032321657" TEXT="Gears は HoareLogic との相性が良いように設計されたプログラミング言語になっている"/> +<node CREATED="1545032436351" ID="ID_1535666009" MODIFIED="1545032467432" TEXT="WhileProgram と同じ形で Gears で証明ができる"/> +</node> +<node CREATED="1545030901019" ID="ID_901428450" MODIFIED="1545030905483" POSITION="left" TEXT="論文の流れ"> +<node CREATED="1545031348434" ID="ID_685170876" MODIFIED="1545031357009" TEXT="現状"> +<node CREATED="1545031359867" ID="ID_1180031106" MODIFIED="1545031386298" TEXT="kernel の検証例"> +<node CREATED="1545031393090" ID="ID_410307657" MODIFIED="1545031412419" TEXT="Cによる実装と関数型言語の記述と証明を行う"/> +</node> +<node CREATED="1545031418116" ID="ID_536836987" MODIFIED="1545031432052" TEXT="低レベル記述向けの関数型言語"> +<node CREATED="1545031433208" ID="ID_1290789880" MODIFIED="1545031441435" TEXT="ATS"/> +<node CREATED="1545031442323" ID="ID_894719933" MODIFIED="1545031444003" TEXT="Rust"/> +<node CREATED="1545031555795" ID="ID_813031602" MODIFIED="1545031611781" TEXT="証明を行うだけの型システムは持ってない"/> +</node> +<node CREATED="1545031472093" ID="ID_942826330" MODIFIED="1545031482407" TEXT="証明支援向けのプログラミング言語"> +<node CREATED="1545031484349" ID="ID_24675818" MODIFIED="1545031491533" TEXT="Agda"/> +<node CREATED="1545031492670" ID="ID_54745078" MODIFIED="1545031494677" TEXT="Coq"/> +<node CREATED="1545031496988" ID="ID_1790735065" MODIFIED="1545031505366" TEXT="Issabella"/> +<node CREATED="1545031511911" ID="ID_1140265385" MODIFIED="1545031517464" TEXT="実行には向かない"/> +</node> +<node CREATED="1545031663383" ID="ID_1834440802" MODIFIED="1545031679864" TEXT="証明の記述とプログラムの記述が別々なのが問題ではないか"/> +</node> +<node CREATED="1545031099382" ID="ID_1202631621" MODIFIED="1545031110989" TEXT="Agda の概要"> +<node CREATED="1545031122593" ID="ID_1888101637" MODIFIED="1545031128590" TEXT="等式変形"/> +<node CREATED="1545031131170" ID="ID_759945081" MODIFIED="1545031133318" TEXT="？"/> +</node> +<node CREATED="1545031223230" ID="ID_1271382711" MODIFIED="1545031233635" TEXT="Gears の概要"> +<node CREATED="1545031240448" ID="ID_1246355278" MODIFIED="1545031248659" TEXT="CbC の実装"/> +<node CREATED="1545031249811" ID="ID_1433130177" MODIFIED="1545031258084" TEXT="Agda による Gears の記述"/> +</node> +<node CREATED="1545031141237" ID="ID_906133157" MODIFIED="1545031146348" TEXT="While Progarm"/> +<node CREATED="1545031153481" ID="ID_434127663" MODIFIED="1545031168863" TEXT="WhileProgram の Agda による証明"/> +<node CREATED="1545031170853" ID="ID_1197992113" MODIFIED="1545031185689" TEXT="Gears による例題"/> +<node CREATED="1545031186560" ID="ID_1521714484" MODIFIED="1545031200105" TEXT="Gears における HoareLogic の証明"/> +</node> +<node CREATED="1545030910084" ID="ID_372949892" MODIFIED="1545030913012" POSITION="left" TEXT="結果"> +<node CREATED="1545030966535" ID="ID_1338356672" MODIFIED="1545030996904" TEXT="Agda で WhileProgram の HoareLogic による証明を作った"/> +<node CREATED="1545030999516" ID="ID_35075799" MODIFIED="1545031016585" TEXT="Gears での HoareLogic の記述をした"/> +<node CREATED="1545031027240" ID="ID_981326333" MODIFIED="1545031044786" TEXT="証明とプログラムの記述を一体化して記述できた"/> +<node CREATED="1545031065628" ID="ID_457628232" MODIFIED="1545031085235" TEXT="証明をメタ計算の引数の受け渡しとして記述できた"/> +</node> </node> </map>