Mercurial > hg > Papers > 2022 > soto-sigos
changeset 6:9ec2d2ac1309
DONE 一度これで提出
line wrap: on
line diff
--- a/Paper/reference.bib Thu May 05 17:38:06 2022 +0900 +++ b/Paper/reference.bib Thu May 05 22:32:45 2022 +0900 @@ -1,22 +1,3 @@ -@inproceedings{agda, - author = {Norell, Ulf}, - title = {Dependently Typed Programming in Agda}, - booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation}, - series = {TLDI '09}, - year = {2009}, - isbn = {978-1-60558-420-1}, - location = {Savannah, GA, USA}, - pages = {1--2}, - numpages = {2}, - url = {http://doi.acm.org/10.1145/1481861.1481862}, - doi = {10.1145/1481861.1481862}, - acmid = {1481862}, - publisher = {ACM}, - address = {New York, NY, USA}, - keywords = {dependent types, programming}, -} - - @article{atton-ipsj, author="比嘉 健太 and 河野 真治", title="Verification Method of Programs Using Continuation based C", @@ -32,36 +13,6 @@ DOI="", } -@article{moggi-monad, - author = {Moggi, Eugenio}, - title = {Notions of Computation and Monads}, - journal = {Inf. Comput.}, - issue_date = {July 1991}, - volume = {93}, - number = {1}, - month = jul, - year = {1991}, - issn = {0890-5401}, - pages = {55--92}, - numpages = {38}, - url = {http://dx.doi.org/10.1016/0890-5401(91)90052-4}, - doi = {10.1016/0890-5401(91)90052-4}, - acmid = {116984}, - publisher = {Academic Press, Inc.}, - address = {Duluth, MN, USA}, -} - -@inproceedings{mitsuki-prosym, - author = "宮城光希 and 河野真治", - title = "Code Gear と Data Gear を持つ Gears OS の設計", - booktitle = "第59回プログラミング・シンポジウム予稿集", - year = "2018", - volume = "2018", - pages = "197--206", - month = "jan" -} - - @techreport{ryokka-sigos, author = "外間,政尊 and 河野,真治", title = "GearsOSのAgdaによる記述と検証", @@ -74,14 +25,6 @@ @misc{agda-wiki, title = {The Agda wiki}, howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}}, - note = {Accessed: 2018/12/17(Mon)}, -} - - -@misc{agda-documentation, - title = {Welcome to Agda’s documentation! — Agda latest documentation}, - howpublished = {\url{http://agda.readthedocs.io/en/latest/}}, - note = {Accessed: 2018/12/17(Mon)}, } @book{Stump:2016:VFP:2841316, @@ -91,113 +34,6 @@ isbn = {978-1-97000-127-3}, publisher = {Association for Computing Machinery and Morgan \&\#38; Claypool}, address = {New York, NY, USA}, -} - -@article{10.1145/363235.363259, -author = {Hoare, C. A. R.}, -title = {An Axiomatic Basis for Computer Programming}, -year = {1969}, -issue_date = {October 1969}, -publisher = {Association for Computing Machinery}, -address = {New York, NY, USA}, -volume = {12}, -number = {10}, -issn = {0001-0782}, -url = {https://doi.org/10.1145/363235.363259}, -doi = {10.1145/363235.363259}, -journal = {Commun. ACM}, -month = oct, -pages = {576–580}, -numpages = {5}, -keywords = {programming language design, theory of programming’ proofs of programs, machine-independent programming, program documentation, axiomatic method, formal language definition} -} - - -@misc{agda-alpa-old, - title = {Example - Hoare Logic}, - howpublished = {\url{http://ocvs.cfv.jp/Agda/readmehoare.html}}, - note = {Accessed: 2019/1/16(Wed)}, -} - -@misc{agda-alpa, - title = {Agda1}, - howpublished = {\url{https://sourceforge.net/projects/agda/}}, - note = {Accessed: 2020/2/9(Sun)}, -} - -@misc{agda2-hoare, - title = {Hoare Logic in Agda2}, - howpublished = {\url{https://github.com/IKEGAMIDaisuke/HoareLogic}}, - note = {Accessed: 2020/2/9(Sun)}, -} - -@misc{coq-old, - title = {Welcome! | The Coq Proof Assistant}, - howpublished = {\url{https://coq.inria.fr/}}, - note = {Accessed: 2020/2/9(Sun)}, -} - - -@misc{coq, - title = {Coq Source}, - howpublished = {\url{https://github.com/coq/coq}}, - note = {Accessed: 2020/2/9(Sun)}, -} - - -@misc{ats2, - title = {ATS-PL-SYS}, - howpublished = {\url{http://www.ats-lang.org/}}, - note = {Accessed: 2020/2/9(Sun)}, -} - -@misc{rust, - title = {Rust programming language}, - howpublished = {\url{https://www.rust-lang.org/}}, - note = {Accessed: 2020/2/9(Sun)}, -} - - -@article{Klein:2010:SFV:1743546.1743574, - author = {Klein, Gerwin and Andronick, June and Elphinstone, Kevin and Heiser, Gernot and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon}, - title = {seL4: Formal Verification of an Operating-system Kernel}, - journal = {Commun. ACM}, - issue_date = {June 2010}, - volume = {53}, - number = {6}, - month = jun, - year = {2010}, - issn = {0001-0782}, - pages = {107--115}, - numpages = {9}, - url = {http://doi.acm.org/10.1145/1743546.1743574}, - doi = {10.1145/1743546.1743574}, - acmid = {1743574}, - publisher = {ACM}, - address = {New York, NY, USA}, -} - -@inproceedings{Nelson:2017:HPV:3132747.3132748, - author = {Nelson, Luke and Sigurbjarnarson, Helgi and Zhang, Kaiyuan and Johnson, Dylan and Bornholt, James and Torlak, Emina and Wang, Xi}, - title = {Hyperkernel: Push-Button Verification of an OS Kernel}, - booktitle = {Proceedings of the 26th Symposium on Operating Systems Principles}, - series = {SOSP '17}, - year = {2017}, - isbn = {978-1-4503-5085-3}, - location = {Shanghai, China}, - pages = {252--269}, - numpages = {18}, - url = {http://doi.acm.org/10.1145/3132747.3132748}, - doi = {10.1145/3132747.3132748}, - acmid = {3132748}, - publisher = {ACM}, - address = {New York, NY, USA}, -} - -@misc{cr-ryukyu, - title = {whileTestPrim.agda - 並列信頼研 mercurial repository}, - howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestPrim.agda}}, - note = {Accessed: 2020/2/9(Sun)} } @mastersthesis{utah-master, @@ -221,24 +57,6 @@ year = "2018" } -@mastersthesis{mitsuki-master, - author = "宮城光希", - title = "継続を基本とした言語による OS のモジュール化", - school = "琉球大学 大学院理工学研究科 情報工学専攻", - year = "2019" -} - -@inproceedings{weko_82695_1, - author = "大城,信康 and 河野,真治", - title = "Continuation based C の GCC4.6 上の実装について", - booktitle = "第53回プログラミング・シンポジウム予稿集", - year = "2012", - volume = "2012", - number = "", - pages = "69--78", - month = "jan" -} - @article{kaito-lola, author = "Kaito, Tokumori and Shinji, Kono", title = "Implementing Continuation based language in LLVM and Clang", @@ -248,23 +66,3 @@ } - -@misc{cbc-llvm, - title = {cbc-llvm - 並列信頼研 mercurial repository}, - howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_llvm/}}, - note = {Accessed: 2020/2/9(Sun)} -} - -@misc{cbc-gcc, - title = {cbc-gcc - 並列信頼研 mercurial repository}, - howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}}, - note = {Accessed: 2020/2/9(Sun)} -} - - -@misc{loop-proof, - title = {loopSemInduct - 並列信頼研 mercurial repository}, - howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestGears.agda}}, - note = {Accessed: 2020/2/9(Sun)} -} -
--- a/Paper/soto-sigos.aux Thu May 05 17:38:06 2022 +0900 +++ b/Paper/soto-sigos.aux Thu May 05 22:32:45 2022 +0900 @@ -33,40 +33,19 @@ \@writefile{lol}{\contentsline {lstlisting}{\numberline {9}{\ignorespaces Gears Agdaでの DPP の step 実行}}{4}{}\protected@file@percent } \newlabel{agda-dpp-lfork}{{10}{4}} \@writefile{lol}{\contentsline {lstlisting}{\numberline {10}{\ignorespaces Gears Agdaでの DPP の左のフォークを取る記述}}{4}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {6}\hskip 1zw{DPPのモデル検査}}{5}{}\protected@file@percent } -\newlabel{agda-dpp-bruteforce}{{11}{5}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {11}{\ignorespaces Gears Agdaでの DPP の場合を網羅するコード}}{5}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{まとめと今後の課題}}{5}{}\protected@file@percent } \citation{*} \bibstyle{ipsjsort} \bibdata{reference} \bibcite{agda-wiki}{1} -\bibcite{agda-alpa}{2} -\bibcite{ats2}{3} -\bibcite{cbc-gcc}{4} -\bibcite{cbc-llvm}{5} -\bibcite{coq}{6} -\bibcite{agda-alpa-old}{7} -\bibcite{agda2-hoare}{8} -\bibcite{loop-proof}{9} -\bibcite{rust}{10} -\bibcite{coq-old}{11} -\bibcite{agda-documentation}{12} -\bibcite{cr-ryukyu}{13} -\bibcite{10.1145/363235.363259}{14} -\bibcite{kaito-lola}{15} -\bibcite{Klein:2010:SFV:1743546.1743574}{16} -\bibcite{moggi-monad}{17} -\bibcite{Nelson:2017:HPV:3132747.3132748}{18} -\bibcite{agda}{19} -\bibcite{Stump:2016:VFP:2841316}{20} -\bibcite{parusu-master}{21} -\bibcite{ryokka-sigos}{22} -\bibcite{mitsuki-master}{23} -\bibcite{mitsuki-prosym}{24} -\bibcite{atton-ipsj}{25} -\bibcite{weko_82695_1}{26} -\bibcite{utah-master}{27} -\bibcite{atton-master}{28} -\newlabel{ipsj@lastpage}{{}{6}} -\gdef \@abspage@last{6} +\bibcite{kaito-lola}{2} +\bibcite{Stump:2016:VFP:2841316}{3} +\bibcite{parusu-master}{4} +\bibcite{ryokka-sigos}{5} +\bibcite{atton-ipsj}{6} +\bibcite{utah-master}{7} +\bibcite{atton-master}{8} +\@writefile{toc}{\contentsline {section}{\numberline {6}\hskip 1zw{DPP のモデル検査}}{5}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{まとめと今後の課題}}{5}{}\protected@file@percent } +\newlabel{ipsj@lastpage}{{}{5}} +\gdef\svg@ink@ver@settings{{\m@ne }{inkscape}{\m@ne }} +\gdef \@abspage@last{5}
--- a/Paper/soto-sigos.bbl Thu May 05 17:38:06 2022 +0900 +++ b/Paper/soto-sigos.bbl Thu May 05 22:32:45 2022 +0900 @@ -1,95 +1,12 @@ -\begin{thebibliography}{10} +\begin{thebibliography}{1} \bibitem{agda-wiki} : The Agda wiki, \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. -\newblock Accessed: 2018/12/17(Mon). - -\bibitem{agda-alpa} -: Agda1, \url{https://sourceforge.net/projects/agda/}. -\newblock Accessed: 2020/2/9(Sun). - -\bibitem{ats2} -: ATS-PL-SYS, \url{http://www.ats-lang.org/}. -\newblock Accessed: 2020/2/9(Sun). - -\bibitem{cbc-gcc} -: cbc-gcc - 並列信頼研 mercurial - repository，\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}. -\newblock Accessed: 2020/2/9(Sun). - -\bibitem{cbc-llvm} -: cbc-llvm - 並列信頼研 mercurial - repository，\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_llvm/}. -\newblock Accessed: 2020/2/9(Sun). - -\bibitem{coq} -: Coq Source, \url{https://github.com/coq/coq}. -\newblock Accessed: 2020/2/9(Sun). - -\bibitem{agda-alpa-old} -: Example - Hoare Logic, \url{http://ocvs.cfv.jp/Agda/readmehoare.html}. -\newblock Accessed: 2019/1/16(Wed). - -\bibitem{agda2-hoare} -: Hoare Logic in Agda2, \url{https://github.com/IKEGAMIDaisuke/HoareLogic}. -\newblock Accessed: 2020/2/9(Sun). - -\bibitem{loop-proof} -: loopSemInduct - 並列信頼研 mercurial - repository，\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestGears.agda}. -\newblock Accessed: 2020/2/9(Sun). - -\bibitem{rust} -: Rust programming language, \url{https://www.rust-lang.org/}. -\newblock Accessed: 2020/2/9(Sun). - -\bibitem{coq-old} -: Welcome! | The Coq Proof Assistant, \url{https://coq.inria.fr/}. -\newblock Accessed: 2020/2/9(Sun). - -\bibitem{agda-documentation} -: Welcome to Agda’s documentation! ― Agda latest - documentation，\url{http://agda.readthedocs.io/en/latest/}. -\newblock Accessed: 2018/12/17(Mon). - -\bibitem{cr-ryukyu} -: whileTestPrim.agda - 並列信頼研 mercurial - repository，\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestPrim.agda}. -\newblock Accessed: 2020/2/9(Sun). - -\bibitem{10.1145/363235.363259} -Hoare, C. A.~R.: An Axiomatic Basis for Computer Programming, {\em Commun. - ACM}, Vol.~12, No.~10, p.\ 576^^e2^^80^^93580 (online), - \doi{10.1145/363235.363259} (1969). \bibitem{kaito-lola} Kaito, T. and Shinji, K.: Implementing Continuation based language in LLVM and Clang, {\em LOLA 2015, Kyoto} (2015). -\bibitem{Klein:2010:SFV:1743546.1743574} -Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., - Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H. - and Winwood, S.: seL4: Formal Verification of an Operating-system Kernel, - {\em Commun. ACM}, Vol.~53, No.~6, pp.\ 107--115 (online), - \doi{10.1145/1743546.1743574} (2010). - -\bibitem{moggi-monad} -Moggi, E.: Notions of Computation and Monads, {\em Inf. Comput.}, Vol.~93, - No.~1, pp.\ 55--92 (online), \doi{10.1016/0890-5401(91)90052-4} (1991). - -\bibitem{Nelson:2017:HPV:3132747.3132748} -Nelson, L., Sigurbjarnarson, H., Zhang, K., Johnson, D., Bornholt, J., Torlak, - E. and Wang, X.: Hyperkernel: Push-Button Verification of an OS Kernel, {\em - Proceedings of the 26th Symposium on Operating Systems Principles}, SOSP '17, - New York, NY, USA, ACM, pp.\ 252--269 (online), \doi{10.1145/3132747.3132748} - (2017). - -\bibitem{agda} -Norell, U.: Dependently Typed Programming in Agda, {\em Proceedings of the 4th - International Workshop on Types in Language Design and Implementation}, TLDI - '09, New York, NY, USA, ACM, pp.\ 1--2 (online), - \doi{10.1145/1481861.1481862} (2009). - \bibitem{Stump:2016:VFP:2841316} Stump, A.: {\em Verified Functional Programming in Agda}, Association for Computing Machinery and Morgan \&\#38; Claypool, New York, NY, USA (2016). @@ -102,25 +19,11 @@ 政尊外間，真治河野\：GearsOSのAgdaによる記述と検証，技術報告 5，琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科 (2018). -\bibitem{mitsuki-master} -宮城光希\：継続を基本とした言語による OS のモジュール化，修士論文，琉球大学 - 大学院理工学研究科 情報工学専攻 (2019). - -\bibitem{mitsuki-prosym} -宮城光希，河野真治\：Code Gear と Data Gear を持つ Gears OS - の設計，第59回プログラミング・シンポジウム予稿集，Vol.~2018, pp.\ 197--206 - (2018). - \bibitem{atton-ipsj} 比嘉健太，河野真治\：Verification Method of Programs Using Continuation based C, 情報処理学会論文誌プログラミング（PRO）， Vol.~10, No.~2, pp.\ 5--5 (online), \urle{https://ci.nii.ac.jp/naid/170000148438/en/} (2017). -\bibitem{weko_82695_1} -信康大城，真治河野\：Continuation based C の GCC4.6 - 上の実装について，第53回プログラミング・シンポジウム予稿集，Vol.~2012, pp.\ - 69--78 (2012). - \bibitem{utah-master} 徳森海斗\：LLVM Clang 上の Continuation based C コンパイラ の改良，修士論文，琉球大学 大学院理工学研究科 情報工学専攻 (2016).
--- a/Paper/soto-sigos.blg Thu May 05 17:38:06 2022 +0900 +++ b/Paper/soto-sigos.blg Thu May 05 22:32:45 2022 +0900 @@ -4,77 +4,49 @@ The style file: ipsjsort.bst Database file #1: reference.bib Warning--to sort, need author or key in agda-wiki -Warning--to sort, need author or key in agda-documentation -Warning--to sort, need author or key in agda-alpa-old -Warning--to sort, need author or key in agda-alpa -Warning--to sort, need author or key in agda2-hoare -Warning--to sort, need author or key in coq-old -Warning--to sort, need author or key in coq -Warning--to sort, need author or key in ats2 -Warning--to sort, need author or key in rust -Warning--to sort, need author or key in cr-ryukyu -Warning--to sort, need author or key in cbc-llvm -Warning--to sort, need author or key in cbc-gcc -Warning--to sort, need author or key in loop-proof Warning--Missing required argument author in agda-wiki -Warning--Missing required argument author in agda-alpa -Warning--Missing required argument author in ats2 -Warning--Missing required argument author in cbc-gcc -Warning--Missing required argument author in cbc-llvm -Warning--Missing required argument author in coq -Warning--Missing required argument author in agda-alpa-old -Warning--Missing required argument author in agda2-hoare -Warning--Missing required argument author in loop-proof -Warning--Missing required argument author in rust -Warning--Missing required argument author in coq-old -Warning--Missing required argument author in agda-documentation -Warning--Missing required argument author in cr-ryukyu Warning--there's no number and/or volumekaito-lola Warning--Missing required argument pages in kaito-lola -Warning--there's a series but neither volume nor number in Nelson:2017:HPV:3132747.3132748 -Warning--there's a series but neither volume nor number in agda -Warning--there's a volume but no series in mitsuki-prosym -Warning--there's a volume but no series in weko_82695_1 -You've used 28 entries, +You've used 8 entries, 2669 wiz_defined-function locations, - 754 strings with 8634 characters, -and the built_in function-call counts, 8082 in all, are: -= -- 713 -> -- 245 -< -- 8 -+ -- 106 -- -- 76 -* -- 532 -:= -- 1096 -add.period$ -- 41 -call.type$ -- 28 -change.case$ -- 94 + 652 strings with 5723 characters, +and the built_in function-call counts, 1968 in all, are: += -- 162 +> -- 72 +< -- 1 ++ -- 29 +- -- 20 +* -- 128 +:= -- 319 +add.period$ -- 8 +call.type$ -- 8 +change.case$ -- 26 chr.to.int$ -- 0 -cite$ -- 60 -duplicate$ -- 452 -empty$ -- 722 -format.name$ -- 102 -if$ -- 1867 +cite$ -- 12 +duplicate$ -- 109 +empty$ -- 174 +format.name$ -- 23 +if$ -- 432 int.to.chr$ -- 0 -int.to.str$ -- 28 -missing$ -- 10 -newline$ -- 100 -num.names$ -- 30 -pop$ -- 209 +int.to.str$ -- 8 +missing$ -- 3 +newline$ -- 27 +num.names$ -- 14 +pop$ -- 34 preamble$ -- 1 -purify$ -- 94 +purify$ -- 26 quote$ -- 0 -skip$ -- 372 +skip$ -- 96 stack$ -- 0 -substring$ -- 350 -swap$ -- 95 -text.length$ -- 20 +substring$ -- 53 +swap$ -- 7 +text.length$ -- 8 text.prefix$ -- 0 top$ -- 0 -type$ -- 110 -warning$ -- 32 -while$ -- 51 -width$ -- 30 -write$ -- 239 -is.kanji.str$ -- 169 -(There were 32 warnings) +type$ -- 30 +warning$ -- 4 +while$ -- 16 +width$ -- 9 +write$ -- 64 +is.kanji.str$ -- 45 +(There were 4 warnings)
--- a/Paper/soto-sigos.fdb_latexmk Thu May 05 17:38:06 2022 +0900 +++ b/Paper/soto-sigos.fdb_latexmk Thu May 05 22:32:45 2022 +0900 @@ -1,17 +1,18 @@ # Fdb version 3 -["bibtex soto-sigos"] 1651739057 "soto-sigos.aux" "soto-sigos.bbl" "soto-sigos" 1651739709 +["bibtex soto-sigos"] 1651754755 "soto-sigos.aux" "soto-sigos.bbl" "soto-sigos" 1651755492 "./ipsjsort.bst" 1541385384 25930 d27669b348c8e9a5c1cc93168b2b5e89 "" - "reference.bib" 1650721531 8174 141307c3535f6e6da421a5ffb91d3db0 "" - "soto-sigos.aux" 1651739709 4473 0ef7b506ff18fc5dee496af2cfee504c "latex" + "reference.bib" 1651750808 1954 450535f55d95a8a5d9e23cbab665da67 "" + "soto-sigos.aux" 1651755491 3788 a3a1a24c3dfa57ec20d5268a2cd1bf7c "latex" (generated) "soto-sigos.bbl" "soto-sigos.blg" -["dvipdf"] 1651739709 "soto-sigos.dvi" "soto-sigos.pdf" "soto-sigos" 1651739709 - "soto-sigos.dvi" 1651739709 67908 9ea91f7e3c11987d76a61d6680d451d3 "latex" +["dvipdf"] 1651755491 "soto-sigos.dvi" "soto-sigos.pdf" "soto-sigos" 1651755492 + "soto-sigos.dvi" 1651755491 59660 af25cc31678831b42d07032c653f6125 "latex" (generated) "soto-sigos.pdf" -["latex"] 1651739708 "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" "soto-sigos.dvi" "soto-sigos" 1651739709 - "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" 1651739708 5269 9fb5ed6f6ebe4ffdc43f6549ce2db125 "" +["latex"] 1651755491 "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" "soto-sigos.dvi" "soto-sigos" 1651755492 + "/dev/null" 0 -1 0 "" + "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" 1651755257 5146 1123a0eaf74dcc5e95f41207ee79342f "" "/usr/share/texmf-dist/fonts/map/fontname/texfonts.map" 1647844622 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm" 1647844622 2124 2601a75482e9426d33db523edf23570a "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm0700.tfm" 1647844622 3584 cf973739aac7ab6247f9150296af7954 "" @@ -83,6 +84,26 @@ "/usr/share/texmf-dist/fonts/tfm/public/lm/rm-lmr8.tfm" 1647844622 11864 309fd7f43e4a0ba39f6f7644d76e8edf "" "/usr/share/texmf-dist/fonts/tfm/public/lm/rm-lmr9.tfm" 1647844622 11884 c93929a6974dce79eabb778f219d7e18 "" "/usr/share/texmf-dist/fonts/tfm/public/txfonts/txsy.tfm" 1647844622 1268 1d124f224979493f8fd017a7597ea1cd "" + "/usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty" 1647807149 8622 63834878edeb14dd71d58d8f22bc3e06 "" + "/usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty" 1647844622 7734 b98cbb34c81f667027c1e3ebdbfce34b "" + "/usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty" 1647844622 492 1994775aa15b0d1289725a0b1bbc2d4c "" + "/usr/share/texmf-dist/tex/generic/iftex/iftex.sty" 1647844622 7237 bdd120a32c8fdb4b433cf9ca2e7cd98a "" + "/usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty" 1647844622 8356 7bbb2c2373aa810be568c29e333da8ed "" + "/usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty" 1647844622 17859 4409f8f50cd365c68e684407e5350b1b "" + "/usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty" 1647844622 20089 80423eac55aa175305d35b49e04fe23b "" + "/usr/share/texmf-dist/tex/generic/pgf/pgf.revision.tex" 1647844622 465 d68603f8b820ea4a08cce534944db581 "" + "/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg" 1647844622 926 2963ea0dcf6cc6c0a770b69ec46a477b "" + "/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-postscript.def" 1647844622 22211 6aad72fb819678b6a7e1bd0e01b78525 "" + "/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-dvips.def" 1647844622 23756 b375d6a2d12ea034485ca32b30950b7c "" + "/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex" 1647844622 61163 9b2eefc24e021323e0fc140e9826d016 "" + "/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex" 1647844622 1896 b8e0ca0ac371d74c0ca05583f6313c91 "" + "/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex" 1647844622 7778 53c8b5623d80238f6a20aa1df1868e63 "" + "/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex" 1647844622 37060 797782f0eb50075c9bc952374d9a659a "" + "/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.tex" 1647844622 37431 9abe862035de1b29c7a677f3205e3d9f "" + "/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex" 1647844622 4494 af17fb7efeafe423710479858e42fa7e "" + "/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.tex" 1647844622 7251 fb18c67117e09c64de82267e12cd8aa4 "" + "/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex" 1647844622 29274 e15c5b7157d21523bd9c9f1dfa146b8e "" + "/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def" 1647844622 6825 a2b0ea5b539dda0625e99dd15785ab59 "" "/usr/share/texmf-dist/tex/latex/amsfonts/amsfonts.sty" 1647844622 5949 3f3fd50a8cc94c3d4cbf4fc66cd3df1c "" "/usr/share/texmf-dist/tex/latex/amsfonts/amssymb.sty" 1647844622 13829 94730e64147574077f8ecfea9bb69af4 "" "/usr/share/texmf-dist/tex/latex/amsmath/amsbsy.sty" 1647844622 2222 da905dc1db75412efd2d8f67739f0596 "" @@ -110,6 +131,11 @@ "/usr/share/texmf-dist/tex/latex/graphics/keyval.sty" 1647844622 2671 4de6781a30211fe0ea4c672e4a2a8166 "" "/usr/share/texmf-dist/tex/latex/graphics/trig.sty" 1647844622 4009 187ea2dc3194cd5a76cd99a8d7a6c4d0 "" "/usr/share/texmf-dist/tex/latex/here/here.sty" 1647807325 439 d908692e0f19922874ccfe2bf35addc7 "" + "/usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty" 1647844622 3910 e04f6a6d983bdbdb024917b7ccc80262 "" + "/usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty" 1647844622 99856 6cbb9d59d820d727b2acbf2edddcf8c8 "" + "/usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty" 1647844622 11081 5538240709a5dbcdc97e4d1524f034a8 "" + "/usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty" 1647844622 3225 54deb0fdd4552a94c6525a4a8ff74efc "" + "/usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty" 1647844622 1954 94f3677c5f3a58b3854eb25278202694 "" "/usr/share/texmf-dist/tex/latex/l3backend/l3backend-dvips.def" 1647844622 35666 542d7d1651a3e3c984a42ed032a045c3 "" "/usr/share/texmf-dist/tex/latex/listings/listings.cfg" 1647844622 1830 e31effa752c61538383451ae21332364 "" "/usr/share/texmf-dist/tex/latex/listings/listings.sty" 1647844622 80964 64e57373f36316e4a09b517cbf1aba2e "" @@ -122,9 +148,16 @@ "/usr/share/texmf-dist/tex/latex/lm/ot1lmr.fd" 1647844622 1882 28c08db1407ebff35a658fd141753d16 "" "/usr/share/texmf-dist/tex/latex/lm/t1lmr.fd" 1647844622 1867 996fe743d88a01aca041ed22cc10e1bb "" "/usr/share/texmf-dist/tex/latex/lm/t1lmtt.fd" 1647844622 2682 555da1faa2e266801e4b221d01a42cb5 "" + "/usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty" 1647844622 443 8c872229db56122037e86bcda49e14f3 "" + "/usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty" 1647844622 325 f9f16d12354225b7dd52a3321f085955 "" "/usr/share/texmf-dist/tex/latex/psnfss/ot1ptm.fd" 1647844622 961 15056f4a61917ceed3a44e4ac11fcc52 "" + "/usr/share/texmf-dist/tex/latex/svg/svg.sty" 1647807149 43468 671ae75b3a15019004495eff4c0911e8 "" + "/usr/share/texmf-dist/tex/latex/tools/shellesc.sty" 1647844622 4118 0f286eca74ee36b7743ff20320e5479f "" + "/usr/share/texmf-dist/tex/latex/transparent/transparent.sty" 1647807149 4155 541de118e0abc42fce3317addc90afb0 "" + "/usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty" 1647807149 1380 971a51b00a14503ddf754cab24c3f209 "" "/usr/share/texmf-dist/tex/latex/txfonts/omstxsy.fd" 1647844622 329 6ac7e19535b9f1d64e4d8e3f77dc30a3 "" "/usr/share/texmf-dist/tex/latex/url/url.sty" 1647844622 12796 8edb7d69a20b857904dd0ea757c14ec9 "" + "/usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty" 1647844622 56029 3f7889dab51d620aa43177c391b7b190 "" "/usr/share/texmf-dist/tex/platex/japanese-otf/ajmacros.sty" 1647806829 31169 82da95c56dec9c45e5b9734751394461 "" "/usr/share/texmf-dist/tex/platex/japanese-otf/mlcid.sty" 1647806829 1209 8abf44b4af3260bbf90285291bba45c8 "" "/usr/share/texmf-dist/tex/platex/japanese-otf/mlutf.sty" 1647806829 5572 2718e332ffca67065c2d32dda76f558f "" @@ -135,16 +168,15 @@ "fig/cbc_codegear.pdf" 1651684831 30110 abae9d544b613e6b77036cde8327a20f "" "ipsj.cls" 1650809266 142123 ecf81ecc4679baed6ac44a1571336871 "" "ipsjtech.sty" 1541385384 6572 e6269869e3c126f2d200f352d590509a "" - "soto-sigos.aux" 1651739709 4473 0ef7b506ff18fc5dee496af2cfee504c "latex" - "soto-sigos.bbl" 1651739057 5285 fc93245f635fcc8bdb721d450a7e0e37 "bibtex soto-sigos" - "soto-sigos.tex" 1651739708 5269 9fb5ed6f6ebe4ffdc43f6549ce2db125 "" + "soto-sigos.aux" 1651755491 3788 a3a1a24c3dfa57ec20d5268a2cd1bf7c "latex" + "soto-sigos.bbl" 1651754755 1492 2b5d2ad68939782993b214beefd4c97b "bibtex soto-sigos" + "soto-sigos.tex" 1651755257 5146 1123a0eaf74dcc5e95f41207ee79342f "" "src/agda-dpp-impl.agda.replaced" 1651667549 2824 60454fbbf20d18849d1886385e94384b "" - "src/agda-dpp-modelcheck.agda.replaced" 1651672378 3179 60cc940175e150991d362fe173027e9b "" "src/agda/cbc-agda.agda.replaced" 1651647471 1143 ab39102eb0f69d3b9f8e4e985a7c1e37 "" - "tex/cbc.tex" 1651739682 2226 dc5c1d561f9ae2126a042ffb96b67360 "" - "tex/cbc_agda.tex" 1651739675 4619 23680a51e50a47a36d558165de0af034 "" - "tex/dpp_impl.tex" 1651739658 7074 a37d202fec1e5b5a34e9f7d0337bda56 "" - "tex/intro.tex" 1651739694 3474 25f20157d5beaa1ef82406eb9fdebc37 "" + "tex/cbc.tex" 1651755242 2253 b995cbd082eafbc6aa946f8e4f2d1282 "" + "tex/cbc_agda.tex" 1651754681 4613 af1478d06e60552962ce70ffd3e86a78 "" + "tex/dpp_impl.tex" 1651755490 7192 bfce887cfeb07dfd06b40449d6215e5a "" + "tex/intro.tex" 1651753637 3466 0307f5084892aaa4629f720086cf9f6e "" (generated) "soto-sigos.aux" "soto-sigos.dvi"
--- a/Paper/soto-sigos.fls Thu May 05 17:38:06 2022 +0900 +++ b/Paper/soto-sigos.fls Thu May 05 22:32:45 2022 +0900 @@ -342,6 +342,264 @@ INPUT /usr/share/texmf-dist/tex/latex/cite/cite.sty INPUT /usr/share/texmf-dist/tex/latex/cite/cite.sty INPUT /usr/share/texmf-dist/tex/latex/cite/cite.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/latex/svg/svg.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +INPUT /usr/share/texmf-dist/tex/latex/graphics/keyval.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +INPUT /usr/share/texmf-dist/tex/latex/graphics/graphicx.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +INPUT /usr/share/texmf-dist/tex/latex/tools/shellesc.sty +INPUT /usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +INPUT /usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /dev/null +INPUT /dev/null +INPUT /dev/null +INPUT ./soto-sigos.w18 +INPUT soto-sigos.w18 +INPUT soto-sigos.w18 +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +INPUT /usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg +INPUT /usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg +INPUT /usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg +INPUT /usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/latex/transparent/transparent.sty +INPUT /usr/share/texmf-dist/tex/generic/iftex/iftex.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty +INPUT /usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def +INPUT /usr/share/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/pgf.revision.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/pgf.revision.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-dvips.def +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-dvips.def +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-postscript.def +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex +INPUT /usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex INPUT /usr/share/texmf-dist/tex/latex/here/here.sty INPUT /usr/share/texmf-dist/tex/latex/here/here.sty INPUT /usr/share/texmf-dist/tex/latex/here/here.sty @@ -417,6 +675,7 @@ INPUT soto-sigos.aux INPUT soto-sigos.aux OUTPUT soto-sigos.aux +INPUT 'inkscape' -V INPUT /usr/share/texmf-dist/fonts/tfm/public/japanese-otf/nmlminr-v.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/japanese-otf/nmlminr-h.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/lm/ec-lmr9.tfm @@ -644,12 +903,6 @@ INPUT src/agda-dpp-impl.agda.replaced INPUT ./src/agda-dpp-impl.agda.replaced INPUT src/agda-dpp-impl.agda.replaced -INPUT ./src/agda-dpp-modelcheck.agda.replaced -INPUT src/agda-dpp-modelcheck.agda.replaced -INPUT ./src/agda-dpp-modelcheck.agda.replaced -INPUT src/agda-dpp-modelcheck.agda.replaced -INPUT ./src/agda-dpp-modelcheck.agda.replaced -INPUT src/agda-dpp-modelcheck.agda.replaced INPUT ./soto-sigos.bbl INPUT soto-sigos.bbl INPUT ./soto-sigos.bbl
--- a/Paper/soto-sigos.log Thu May 05 17:38:06 2022 +0900 +++ b/Paper/soto-sigos.log Thu May 05 22:32:45 2022 +0900 @@ -1,6 +1,6 @@ -This is e-pTeX, Version 3.141592653-p3.9.0-210218-2.6 (utf8.euc) (TeX Live 2021/Arch Linux) (preloaded format=platex 2022.4.23) 5 MAY 2022 17:35 +This is e-pTeX, Version 3.141592653-p3.9.0-210218-2.6 (utf8.euc) (TeX Live 2021/Arch Linux) (preloaded format=platex 2022.4.23) 5 MAY 2022 21:58 entering extended mode - restricted \write18 enabled. + \write18 enabled. file:line:error style messages enabled. %&-line parsing enabled. **/home/soto/lab/soto-sigos/Paper/soto-sigos.tex @@ -3235,13 +3235,133 @@ LaTeX Info: Redefining \cite on input line 302. LaTeX Info: Redefining \nocite on input line 332. Package: cite 2015/02/27 v 5.5 -) (/usr/share/texmf-dist/tex/latex/here/here.sty) (/usr/share/texmf-dist/tex/latex/float/float.sty +) (/usr/share/texmf-dist/tex/latex/svg/svg.sty +Package: svg 2020/11/26 v2.02k (include SVG pictures) + (/usr/share/texmf-dist/tex/generic/iftex/iftex.sty +Package: iftex 2022/02/03 v1.0f TeX engine tests +) (/usr/share/texmf-dist/tex/latex/koma-script/scrbase.sty +Package: scrbase 2021/11/13 v3.35 KOMA-Script package (KOMA-Script-independent basics and keyval usage) + (/usr/share/texmf-dist/tex/latex/koma-script/scrlfile.sty +Package: scrlfile 2021/11/13 v3.35 KOMA-Script package (file load hooks) + (/usr/share/texmf-dist/tex/latex/koma-script/scrlfile-hook.sty +Package: scrlfile-hook 2021/11/13 v3.35 KOMA-Script package (using LaTeX hooks) + (/usr/share/texmf-dist/tex/latex/koma-script/scrlogo.sty +Package: scrlogo 2021/11/13 v3.35 KOMA-Script package (logo) +))) +Applying: [2021/05/01] Usage of raw or classic option list on input line 252. +Already applied: [0000/00/00] Usage of raw or classic option list on input line 368. +) (/usr/share/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty +Package: pdftexcmds 2020-06-27 v0.33 Utility functions of pdfTeX for LuaTeX (HO) + (/usr/share/texmf-dist/tex/generic/infwarerr/infwarerr.sty +Package: infwarerr 2019/12/03 v1.5 Providing info/warning/error messages (HO) +) (/usr/share/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty +Package: ltxcmds 2020-05-10 v1.25 LaTeX kernel commands for general use (HO) +) +Package pdftexcmds Info: \pdf@primitive is available. +Package pdftexcmds Info: \pdf@ifprimitive is available. +Package pdftexcmds Info: \pdfdraftmode not found. +) (/usr/share/texmf-dist/tex/latex/trimspaces/trimspaces.sty +Package: trimspaces 2009/09/17 v1.1 Trim spaces around a token list +) (/usr/share/texmf-dist/tex/latex/tools/shellesc.sty +Package: shellesc 2019/11/08 v1.0c unified shell escape interface for LaTeX +Package shellesc Info: Unrestricted shell escape enabled on input line 75. +) (/usr/share/texmf-dist/tex/latex/ifplatform/ifplatform.sty +Package: ifplatform 2017/10/13 v0.4a Testing for the operating system + (/usr/share/texmf-dist/tex/generic/catchfile/catchfile.sty +Package: catchfile 2019/12/09 v1.8 Catch the contents of a file (HO) + (/usr/share/texmf-dist/tex/generic/etexcmds/etexcmds.sty +Package: etexcmds 2019/12/15 v1.7 Avoid name clashes with e-TeX commands (HO) +)) (/usr/share/texmf-dist/tex/generic/iftex/ifluatex.sty +Package: ifluatex 2019/10/25 v1.5 ifluatex legacy package. Use iftex instead. +) +runsystem(uname -s > "soto-sigos.w18")...executed. + + (./soto-sigos.w18) +runsystem(rm -- "soto-sigos.w18")...executed. + +) +\c@svg@param@lastpage=\count296 +\svg@box=\box89 +\c@svg@param@currpage=\count297 +) (/usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty +Package: xcolor 2021/10/31 v2.13 LaTeX color extensions (UK) + (/usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg +File: color.cfg 2016/01/02 v1.6 sample color configuration +) +Package xcolor Info: Driver file: dvips.def on input line 227. +LaTeX Info: Redefining \color on input line 711. +Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1352. +Package xcolor Info: Model `RGB' extended on input line 1368. +Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1370. +Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1371. +Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1372. +Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1373. +Package xcolor Info: Model `Gray' substituted by `gray' on input line 1374. +Package xcolor Info: Model `wave' substituted by `hsb' on input line 1375. +) (/usr/share/texmf-dist/tex/latex/transparent/transparent.sty +Package: transparent 2019/11/29 v1.4 Transparency via pdfTeX's color stack (HO) + + +Package transparent Warning: Loading aborted, because pdfTeX is not running in PDF mode. + +) (/usr/share/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty (/usr/share/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex +\pgfutil@everybye=\toks25 +\pgfutil@tempdima=\dimen187 +\pgfutil@tempdimb=\dimen188 + (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.tex)) (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def +\pgfutil@abb=\box90 +) (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex (/usr/share/texmf-dist/tex/generic/pgf/pgf.revision.tex) +Package: pgfrcs 2021/05/15 v3.1.9a (3.1.9a) +)) (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex +Package: pgfsys 2021/05/15 v3.1.9a (3.1.9a) + (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex +\pgfkeys@pathtoks=\toks26 +\pgfkeys@temptoks=\toks27 + (/usr/share/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.tex +\pgfkeys@tmptoks=\toks28 +)) +\pgf@x=\dimen189 +\pgf@y=\dimen190 +\pgf@xa=\dimen191 +\pgf@ya=\dimen192 +\pgf@xb=\dimen193 +\pgf@yb=\dimen194 +\pgf@xc=\dimen195 +\pgf@yc=\dimen196 +\pgf@xd=\dimen197 +\pgf@yd=\dimen198 +\w@pgf@writea=\write3 +\r@pgf@reada=\read2 +\c@pgf@counta=\count298 +\c@pgf@countb=\count299 +\c@pgf@countc=\count300 +\c@pgf@countd=\count301 +\t@pgf@toka=\toks29 +\t@pgf@tokb=\toks30 +\t@pgf@tokc=\toks31 +\pgf@sys@id@count=\count302 + (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg +File: pgf.cfg 2021/05/15 v3.1.9a (3.1.9a) +) +Driver file for pgf: pgfsys-dvips.def + (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-dvips.def +File: pgfsys-dvips.def 2021/05/15 v3.1.9a (3.1.9a) + (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-postscript.def +File: pgfsys-common-postscript.def 2021/05/15 v3.1.9a (3.1.9a) +\pgf@objectcount=\count303 +))) (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex +File: pgfsyssoftpath.code.tex 2021/05/15 v3.1.9a (3.1.9a) +\pgfsyssoftpath@smallbuffer@items=\count304 +\pgfsyssoftpath@bigbuffer@items=\count305 +) (/usr/share/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex +File: pgfsysprotocol.code.tex 2021/05/15 v3.1.9a (3.1.9a) +)) (/usr/share/texmf-dist/tex/latex/here/here.sty) (/usr/share/texmf-dist/tex/latex/float/float.sty Package: float 2001/11/08 v1.3d Float enhancements (AL) -\c@float@type=\count296 -\float@exts=\toks25 -\float@box=\box89 -\@float@everytoks=\toks26 -\@floatcapt=\box90 +\c@float@type=\count306 +\float@exts=\toks32 +\float@box=\box91 +\@float@everytoks=\toks33 +\@floatcapt=\box92 ) (/usr/share/texmf-dist/tex/latex/listings/lstlang1.sty File: lstlang1.sty 2020/03/24 1.8d listings language file ) (/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty @@ -3250,14 +3370,14 @@ Package: caption 2022/03/01 v3.6b Customizing captions (AR) (/usr/share/texmf-dist/tex/latex/caption/caption3.sty Package: caption3 2022/03/17 v2.3b caption3 kernel (AR) -\caption@tempdima=\dimen187 -\captionmargin=\dimen188 -\caption@leftmargin=\dimen189 -\caption@rightmargin=\dimen190 -\caption@width=\dimen191 -\caption@indent=\dimen192 -\caption@parindent=\dimen193 -\caption@hangindent=\dimen194 +\caption@tempdima=\dimen199 +\captionmargin=\dimen256 +\caption@leftmargin=\dimen257 +\caption@rightmargin=\dimen258 +\caption@width=\dimen259 +\caption@indent=\dimen260 +\caption@parindent=\dimen261 +\caption@hangindent=\dimen262 Package caption Info: Unknown document class (or package), (caption) standard defaults will be used. Package caption Info: \@makecaption = \long macro:#1#2->\footnotesize \vskip \abovecaptionskip \setbox \@tempboxa \hbox {\footnotesize {\bfseries #1}\hskip 1\zw \shortstack [l]{#2}}\@tempdima \ht \@tempboxa \advance \@tempdima \dp \@tempboxa \setbox \@tempboxb \hbox {\footnotesize {\bfseries #1}\hskip 1\zw }\ifdim \@tempdima > \baselineskip \ifdim \wd \@tempboxa > \capwidth \hfil \parbox [t]{\capwidth }{\hangindent \wd \@tempboxb {\bfseries #1}\hskip 1\zw #2}\vskip 4\@Q \else \hfil \parbox [t]{\wd \@tempboxa }{\hangindent \wd \@tempboxb {\bfseries #1}\hskip 1\zw #2}\par \prevdepth =0pt\vskip -1.5\h \fi \else \ifdim \wd \@tempboxa > \capwidth \hfil \parbox [t]{\capwidth }{\hangindent \wd \@tempboxb {\bfseries #1}\hskip 1\zw #2}\ifx \@captype \TABLE \ifDS@english \par \vskip .25mm\else \par \prevdepth =0pt\vskip -1.5mm\fi \else \par \prevdepth =0pt\vskip -1.5\h \fi \else \setbox \@tempboxb \hbox {#2}\hbox to\hsize {\hfil \box \@tempboxa \hfil }\ifDS@english \relax \else \vspace {-\belowcaptionskip }\fi \fi \fi \vspace {\belowcaptionskip }\par on input line 1176. @@ -3267,128 +3387,137 @@ (caption) standard defaults will be used. See the caption package documentation for explanation. -\c@caption@flags=\count297 -\c@continuedfloat=\count298 +\c@caption@flags=\count307 +\c@continuedfloat=\count308 Package caption Info: float package is loaded. Package caption Info: listings package is loaded. ) LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 9.24725pt on input line 54. +(Font) scaled to size 9.24725pt on input line 55. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 9.24725pt on input line 54. -LaTeX Font Info: Trying to load font information for T1+lmr on input line 54. +(Font) scaled to size 9.24725pt on input line 55. +LaTeX Font Info: Trying to load font information for T1+lmr on input line 55. (/usr/share/texmf-dist/tex/latex/lm/t1lmr.fd File: t1lmr.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) (/usr/share/texmf-dist/tex/latex/l3backend/l3backend-dvips.def File: l3backend-dvips.def 2022-02-07 L3 backend support: dvips -\l__pdf_internal_box=\box91 -\g__pdf_backend_object_int=\count299 -\l__pdf_backend_content_box=\box92 -\l__pdf_backend_model_box=\box93 -\g__pdf_backend_annotation_int=\count300 -\g__pdf_backend_link_int=\count301 -\g__pdf_backend_link_sf_int=\count302 +\l__pdf_internal_box=\box93 +\g__pdf_backend_object_int=\count309 +\l__pdf_backend_content_box=\box94 +\l__pdf_backend_model_box=\box95 +\g__pdf_backend_annotation_int=\count310 +\g__pdf_backend_link_int=\count311 +\g__pdf_backend_link_sf_int=\count312 ) (./soto-sigos.aux) \openout1 = `soto-sigos.aux'. -LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 54. -LaTeX Font Info: ... okay on input line 54. -LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 54. -LaTeX Font Info: ... okay on input line 54. -LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 54. -LaTeX Font Info: ... okay on input line 54. -LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 54. -LaTeX Font Info: ... okay on input line 54. -LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 54. -LaTeX Font Info: ... okay on input line 54. -LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 54. -LaTeX Font Info: ... okay on input line 54. -LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 54. -LaTeX Font Info: ... okay on input line 54. -LaTeX Font Info: Checking defaults for JY1/mc/m/n on input line 54. -LaTeX Font Info: ... okay on input line 54. -LaTeX Font Info: Checking defaults for JT1/mc/m/n on input line 54. -LaTeX Font Info: ... okay on input line 54. -\c@lstlisting=\count303 +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 55. +LaTeX Font Info: ... okay on input line 55. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 55. +LaTeX Font Info: ... okay on input line 55. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 55. +LaTeX Font Info: ... okay on input line 55. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 55. +LaTeX Font Info: ... okay on input line 55. +LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 55. +LaTeX Font Info: ... okay on input line 55. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 55. +LaTeX Font Info: ... okay on input line 55. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 55. +LaTeX Font Info: ... okay on input line 55. +LaTeX Font Info: Checking defaults for JY1/mc/m/n on input line 55. +LaTeX Font Info: ... okay on input line 55. +LaTeX Font Info: Checking defaults for JT1/mc/m/n on input line 55. +LaTeX Font Info: ... okay on input line 55. +\c@lstlisting=\count313 + (|'inkscape' -V ) + +Package svg Warning: No version of Inkscape was detected by invoking +(svg) `inkscape -V' +(svg) so the Inkscape export will fail quite sure as the +(svg) command is probably unknown to your OS. You could set +(svg) `inkscapeversion=<version>' manually but this is very +(svg) unlikely to work on input line 55. + Package caption Info: Begin \AtBeginDocument code. Package caption Info: End \AtBeginDocument code. LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 8.53593pt on input line 67. +(Font) scaled to size 8.53593pt on input line 68. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 8.53593pt on input line 67. +(Font) scaled to size 8.53593pt on input line 68. LaTeX Font Info: Font shape `JT1/hmc/bx/n' will be -(Font) scaled to size 8.53593pt on input line 67. +(Font) scaled to size 8.53593pt on input line 68. LaTeX Font Info: Font shape `JY1/hmc/bx/n' will be -(Font) scaled to size 8.53593pt on input line 67. +(Font) scaled to size 8.53593pt on input line 68. LaTeX Font Info: Font shape `JT1/gt/bx/n' in size <19.2207> not available -(Font) Font shape `JT1/gt/m/n' tried instead on input line 75. +(Font) Font shape `JT1/gt/m/n' tried instead on input line 76. LaTeX Font Info: Font shape `JY1/gt/bx/n' in size <19.2207> not available -(Font) Font shape `JY1/gt/m/n' tried instead on input line 75. -LaTeX Font Info: Calculating math sizes for size <9.61035> on input line 75. -LaTeX Font Info: Trying to load font information for OT1+lmr on input line 75. - (/usr/share/texmf-dist/tex/latex/lm/ot1lmr.fd +(Font) Font shape `JY1/gt/m/n' tried instead on input line 76. +LaTeX Font Info: Calculating math sizes for size <9.61035> on input line 76. +LaTeX Font Info: Trying to load font information for OT1+lmr on input line 76. +(/usr/share/texmf-dist/tex/latex/lm/ot1lmr.fd File: ot1lmr.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) -LaTeX Font Info: Trying to load font information for OML+lmm on input line 75. +LaTeX Font Info: Trying to load font information for OML+lmm on input line 76. (/usr/share/texmf-dist/tex/latex/lm/omllmm.fd File: omllmm.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) -LaTeX Font Info: Trying to load font information for OMS+lmsy on input line 75. +LaTeX Font Info: Trying to load font information for OMS+lmsy on input line 76. (/usr/share/texmf-dist/tex/latex/lm/omslmsy.fd File: omslmsy.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) -LaTeX Font Info: Trying to load font information for OMX+lmex on input line 75. +LaTeX Font Info: Trying to load font information for OMX+lmex on input line 76. (/usr/share/texmf-dist/tex/latex/lm/omxlmex.fd File: omxlmex.fd 2015/05/01 v1.6.1 Font defs for Latin Modern ) LaTeX Font Info: External font `lmex10' loaded for size -(Font) <9.61035> on input line 75. +(Font) <9.61035> on input line 76. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <6.7272> on input line 75. +(Font) <6.7272> on input line 76. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <4.80518> on input line 75. +(Font) <4.80518> on input line 76. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 6.47304pt on input line 75. +(Font) scaled to size 6.47304pt on input line 76. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 4.62363pt on input line 75. +(Font) scaled to size 4.62363pt on input line 76. LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 11.38124pt on input line 75. +(Font) scaled to size 11.38124pt on input line 76. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 11.38124pt on input line 75. -LaTeX Font Info: Calculating math sizes for size <11.82813> on input line 75. +(Font) scaled to size 11.38124pt on input line 76. +LaTeX Font Info: Calculating math sizes for size <11.82813> on input line 76. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <11.82813> on input line 75. +(Font) <11.82813> on input line 76. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <8.27965> on input line 75. +(Font) <8.27965> on input line 76. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <5.91406> on input line 75. +(Font) <5.91406> on input line 76. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 7.96683pt on input line 75. +(Font) scaled to size 7.96683pt on input line 76. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 5.69061pt on input line 75. +(Font) scaled to size 5.69061pt on input line 76. LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 7.96683pt on input line 75. +(Font) scaled to size 7.96683pt on input line 76. LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 7.11327pt on input line 75. +(Font) scaled to size 7.11327pt on input line 76. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 7.11327pt on input line 75. +(Font) scaled to size 7.11327pt on input line 76. LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 7.8246pt on input line 75. +(Font) scaled to size 7.8246pt on input line 76. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 7.8246pt on input line 75. -LaTeX Font Info: Calculating math sizes for size <8.13184> on input line 75. +(Font) scaled to size 7.8246pt on input line 76. +LaTeX Font Info: Calculating math sizes for size <8.13184> on input line 76. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <8.13184> on input line 75. +(Font) <8.13184> on input line 76. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <5.69225> on input line 75. +(Font) <5.69225> on input line 76. LaTeX Font Info: External font `lmex10' loaded for size -(Font) <4.06592> on input line 75. +(Font) <4.06592> on input line 76. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 5.47719pt on input line 75. +(Font) scaled to size 5.47719pt on input line 76. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 3.9123pt on input line 75. +(Font) scaled to size 3.9123pt on input line 76. LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 5.47719pt on input line 75. +(Font) scaled to size 5.47719pt on input line 76. (./tex/intro.tex LaTeX Font Info: Font shape `JT1/hmc/bx/n' will be (Font) scaled to size 11.38124pt on input line 1. @@ -3396,33 +3525,33 @@ (Font) scaled to size 11.38124pt on input line 1. ) (./tex/cbc.tex LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 7.53018pt on input line 7. +(Font) scaled to size 7.53018pt on input line 15. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 7.53018pt on input line 7. +(Font) scaled to size 7.53018pt on input line 15. LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 6.84561pt on input line 7. +(Font) scaled to size 6.84561pt on input line 15. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 6.84561pt on input line 7. +(Font) scaled to size 6.84561pt on input line 15. (I search kanjifont definition file: . . ) (I search font definition file: . . . . . . . ) -LaTeX Font Info: Trying to load font information for OMS+txsy on input line 7. +LaTeX Font Info: Trying to load font information for OMS+txsy on input line 15. (/usr/share/texmf-dist/tex/latex/txfonts/omstxsy.fd File: omstxsy.fd 2000/12/15 v3.1 ) -LaTeX Font Info: Trying to load font information for T1+txsy on input line 7. -LaTeX Font Info: No file T1txsy.fd. on input line 7. +LaTeX Font Info: Trying to load font information for T1+txsy on input line 15. +LaTeX Font Info: No file T1txsy.fd. on input line 15. LaTeX Font Warning: Font shape `T1/txsy/m/n' undefined -(Font) using `T1/cmr/m/n' instead on input line 7. - -LaTeX Font Info: Trying to load font information for OT1+ptm on input line 7. +(Font) using `T1/cmr/m/n' instead on input line 15. + +LaTeX Font Info: Trying to load font information for OT1+ptm on input line 15. (/usr/share/texmf-dist/tex/latex/psnfss/ot1ptm.fd File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm. ) LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 8.8993pt on input line 7. +(Font) scaled to size 8.8993pt on input line 15. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 8.8993pt on input line 7. +(Font) scaled to size 8.8993pt on input line 15. [1 @@ -3443,9 +3572,9 @@ consecutive: ) [2] LaTeX Font Info: Font shape `JT1/hmc/bx/n' will be -(Font) scaled to size 9.24725pt on input line 61. +(Font) scaled to size 9.24725pt on input line 54. LaTeX Font Info: Font shape `JY1/hmc/bx/n' will be -(Font) scaled to size 9.24725pt on input line 61. +(Font) scaled to size 9.24725pt on input line 54. ) (./tex/dpp_impl.tex File: fig/Dining.pdf Graphic file (type pdf) <fig/Dining.pdf> @@ -3461,7 +3590,7 @@ consecutive: ) (./src/agda-dpp-impl.agda.replaced consecutive: -[4])) (./src/agda-dpp-modelcheck.agda.replaced) [5] (./soto-sigos.bbl +) [4]) (./soto-sigos.bbl LaTeX Font Info: Calculating math sizes for size <8.8711> on input line 1. LaTeX Font Info: External font `lmex10' loaded for size (Font) <8.8711> on input line 1. @@ -3473,136 +3602,26 @@ (Font) scaled to size 5.97511pt on input line 1. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be (Font) scaled to size 4.26796pt on input line 1. - -Underfull \hbox (badness 10000) in paragraph at lines 12--14 -[]\T1/lmr/m/n/8.8711 : ATS-PL-SYS, $\T1/lmtt/m/n/8.8711 http : / / www . ats-[]lang . org/$\T1/lmr/m/n/8.8711 . - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 16--19 -\T1/lmtt/m/n/8.8711 / / www . cr . ie . u-[]ryukyu . ac . jp / hg / CbC / CbC _ gcc/$\T1/lmr/m/n/8.8711 . - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 21--24 -\T1/lmtt/m/n/8.8711 / / www . cr . ie . u-[]ryukyu . ac . jp / hg / CbC / CbC _ llvm/$\T1/lmr/m/n/8.8711 . - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 26--28 -[]\T1/lmr/m/n/8.8711 : Coq Source, $\T1/lmtt/m/n/8.8711 https : / / github . com / coq / coq$\T1/lmr/m/n/8.8711 . - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 30--32 -\T1/lmtt/m/n/8.8711 readmehoare . html$\T1/lmr/m/n/8.8711 . plus.33emminus.07emAccessed: - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 34--36 -[]\T1/lmr/m/n/8.8711 : Hoare Logic in Agda2, $\T1/lmtt/m/n/8.8711 https : / / - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 34--36 -\T1/lmtt/m/n/8.8711 github . com / IKEGAMIDaisuke / HoareLogic$\T1/lmr/m/n/8.8711 . - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 38--41 -\T1/lmtt/m/n/8.8711 http : / / www . cr . ie . u-[]ryukyu . ac . jp / hg / Members / - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 38--41 -\T1/lmtt/m/n/8.8711 ryokka / HoareLogic / file / tip / whileTestGears . - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 43--45 -[]\T1/lmr/m/n/8.8711 : Rust pro-gram-ming lan-guage, $\T1/lmtt/m/n/8.8711 https : / / www . - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 43--45 -\T1/lmtt/m/n/8.8711 rust-[]lang . org/$\T1/lmr/m/n/8.8711 . plus.33emminus.07emAccessed: - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 47--49 -\T1/lmtt/m/n/8.8711 / / coq . inria . fr/$\T1/lmr/m/n/8.8711 . plus.33emminus.07emAccessed: - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 51--54 -\T1/lmr/m/n/8.8711 lat-est doc-u-men-ta-tion\JY1/hmc/m/n/8.8711 ， $\T1/lmtt/m/n/8.8711 http : / / agda . readthedocs . - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 51--54 -\T1/lmtt/m/n/8.8711 io / en / latest/$\T1/lmr/m/n/8.8711 . plus.33emminus.07emAccessed: - [] - - -Underfull \hbox (badness 4353) in paragraph at lines 56--59 -[]\T1/lmr/m/n/8.8711 : whileTest-Prim.agda - \JY1/hmc/m/n/8.8711 並列信頼研 \T1/lmr/m/n/8.8711 mer-cu-rial - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 56--59 -\T1/lmr/m/n/8.8711 repos-i-tory\JY1/hmc/m/n/8.8711 ， $\T1/lmtt/m/n/8.8711 http : / / www . cr . ie . u-[]ryukyu . ac . - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 56--59 -\T1/lmtt/m/n/8.8711 jp / hg / Members / ryokka / HoareLogic / file / tip / - [] - LaTeX Font Info: Font shape `JT1/hgt/m/n' will be -(Font) scaled to size 8.53593pt on input line 61. +(Font) scaled to size 8.53593pt on input line 8. LaTeX Font Info: Font shape `JY1/hgt/m/n' will be -(Font) scaled to size 8.53593pt on input line 61. -LaTeX Font Info: Kanji font shape `JY1/hgt/m/it' undefined -(Font) No change on input line 61. -LaTeX Font Info: Kanji font shape `JY1/hgt/m/it' undefined -(Font) No change on input line 67. -LaTeX Font Info: Kanji font shape `JY1/hgt/m/it' undefined -(Font) No change on input line 73. -LaTeX Font Info: Kanji font shape `JY1/hgt/m/it' undefined -(Font) No change on input line 77. -LaTeX Font Info: Kanji font shape `JY1/hgt/m/it' undefined -(Font) No change on input line 82. -LaTeX Font Info: Kanji font shape `JY1/hgt/m/it' undefined -(Font) No change on input line 88. +(Font) scaled to size 8.53593pt on input line 8. LaTeX Font Info: Kanji font shape `JY1/hgt/m/it' undefined -(Font) No change on input line 94. - -Underfull \hbox (badness 7362) in paragraph at lines 115--118 -[]\JY1/hmc/m/n/8.8711 比嘉健太 ， 河野真治 []\T1/lmr/m/n/8.8711 Verification Method of - [] - - -Underfull \hbox (badness 10000) in paragraph at lines 115--118 -\T1/lmr/m/n/8.8711 Pro-grams Us-ing Con-tin-u-a-tion based C, \JY1/hmc/m/n/8.8711 情 - [] - - -Underfull \hbox (badness 6625) in paragraph at lines 115--118 -\JY1/hmc/m/n/8.8711 報処理学会論文誌プログラミング （\T1/lmr/m/n/8.8711 PRO\JY1/hmc/m/n/8.8711 ） ， - [] - -) [6] (./soto-sigos.aux) +(Font) No change on input line 8. +LaTeX Font Info: Kanji font shape `JY1/hgt/m/it' undefined +(Font) No change on input line 11. +) [5] (./soto-sigos.aux) LaTeX Font Warning: Some font shapes were not available, defaults substituted. ) Here is how much of TeX's memory you used: - 10946 strings out of 478739 - 166780 string characters out of 5863952 - 1452538 words of memory out of 5000000 - 29184 multiletter control sequences out of 15000+600000 + 13846 strings out of 478739 + 227762 string characters out of 5863952 + 1307732 words of memory out of 5000000 + 31965 multiletter control sequences out of 15000+600000 583961 words of font info for 188 fonts, out of 8000000 for 9000 929 hyphenation exceptions out of 8191 - 55i,11n,63p,483b,1976s stack positions out of 5000i,500n,10000p,200000b,80000s - -Output written on soto-sigos.dvi (6 pages, 67908 bytes). + 94i,10n,92p,483b,1986s stack positions out of 5000i,500n,10000p,200000b,80000s + +Output written on soto-sigos.dvi (5 pages, 59660 bytes).
--- a/Paper/soto-sigos.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/soto-sigos.tex Thu May 05 22:32:45 2022 +0900 @@ -19,6 +19,7 @@ \usepackage[deluxe, multi]{otf} \usepackage{url} \usepackage{cite} +\usepackage{svg} %\documentclass[withpage, english]{ipsjprosym} %\usepackage{comment} \usepackage{here} @@ -54,7 +55,7 @@ \begin{document} % Title, Author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\title{GearsAgda上のモデル検査の形式化} +\title{Gears Agda 上のモデル検査の形式化} %\affiliate{IPSJ}{情報処理学会} \affiliate{IIRYUKYU}{琉球大学大学院理工学研究科工学専攻知能情報プログラム} @@ -65,11 +66,11 @@ %概要 \begin{abstract} - 当研究室では Continuation based C （CbC） という言語を用いて，拡張性と信頼性を両立するOSであるGearsOSを開発している． + 当研究室では Continuation based C （CbC） という言語を用いて，拡張性と信頼性を両立する OS である Gears OS を開発している． CbC とは， C言語から通常の関数呼び出しではなく，アセンブラでいうjmp命令により関数を遷移する継続を導入した C 言語の下位言語である． - すでにGearsOSはメタ計算によるモデル検査機構を持っている． - GearsOSのCodeGear/DataGearはGearsAgdaにより形式証明に向いた形に記述することができる． - モデル検査機構をGearsAgdaにより記述することでHoare Logic的な逐次実行型のプログラムの証明だけでなく，並行実行を含むプログラムの証明が可能になる． + すでに Gears OS はメタ計算によるモデル検査機構を持っている． + GearsOS の CodeGear/DataGear は Gears Agda により形式証明に向いた形に記述することができる． + モデル検査機構を Gears Agda により記述することで Hoare Logic 的な逐次実行型のプログラムの証明だけでなく，並行実行を含むプログラムの証明が可能になる． \end{abstract} \maketitle @@ -94,31 +95,25 @@ \input{tex/dpp_impl.tex}% Gears Agda の記法 loopのやつやる -\section{DPPのモデル検査} +\section{DPP のモデル検査} モデル検査の機能として，入力の網羅が挙げられる． -今回のDPPの入力の網羅として，哲学者が思考をつづけるのか，食事をはじめようとするのかと +今回の DPP の入力の網羅として，哲学者が思考をつづけるのか，食事をはじめようとするのかと 食事中に食事をそのままつづけるのか，思考をするために食事を止めようとするのかが分岐する． -そのため，next-codeがthinkingかeatingであるものに対して分岐を網羅する Code \ref{agda-dpp-bruteforce} -を定義した． - +そのため， next-code が thinking か eating であるものに対して分岐を網羅するコードを実装した． -\lstinputlisting[caption= Gears Agdaでの DPP の場合を網羅するコード, label=agda-dpp-bruteforce]{src/agda-dpp-modelcheck.agda.replaced} - -内部で行っていることとして，その Code Gear 内に存在している next-code が thinking もしくは eatingである場合に -そのプロセスのnext-codeをそのままにするか，それぞれ pickup-rfork か putdown-lfork にする． -そのため，その部分に対してbit全探索を行い，場合の網羅を行っている． +内部で行っていることとして，その Code Gear 内に存在している next-code が thinking もしくは eating である場合に +そのプロセスの next-code をそのままにするか，それぞれ pickup-rfork か putdown-lfork にする． +そのため，その部分に対して bit 全探索を行い，場合の網羅を行っている． % まとめ \section{まとめと今後の課題} -今回は Agda に CbC の継続の概念を追加した Gears Agda にて -DPPのモデル検査を行おうとした． -結果として，DPPの実装と入力の網羅までできた． +今回は Agda に CbC の継続の概念を追加した Gears Agda にて DPP のモデル検査を行おうとした． +結果として，DPP の実装と入力の網羅までできた． -これからプロセスがすべてほかのプロセスの終了待ちになった場合に -dead lock 状態になっていることを検知できるようにしたい． -加えて，assertの機能をつけて仕様から外れたことをしていないことを示したい． +今後はプロセスがすべてほかのプロセスの終了待ちになった場合に dead lock 状態になっていることを検知できるようにしたい． +加えて，assert の機能をつけて仕様通りの動作がされていることを検証したい． \nocite{*} \bibliographystyle{ipsjsort}
--- a/Paper/src/ModelChecking.agda Thu May 05 17:38:06 2022 +0900 +++ b/Paper/src/ModelChecking.agda Thu May 05 22:32:45 2022 +0900 @@ -125,7 +125,7 @@ bit-force-search zero f l env envl exit = exit envl bit-force-search (suc redu) f [] env envl exit = exit envl bit-force-search (suc redu) f (true ∷ bs) env envl exit = bit-force-search (suc redu) (f ++ (false ∷ [])) bs env envl exit -- 今回の対象をfalseにしてfに追加,bを次の対象にする - bit-force-search (suc redu) f (false ∷ bs) env envl exit = set-state redu (f ++ (true ∷ bs)) (f ++ (true ∷ bs)) [] (ph env) env envl exit where -- 今回の対象をtrueにし、fとbを結合してそのListを代入する。かつそれをbに入れfをinitしてloopさせる + bit-force-search (suc redu) f (false ∷ bs) env envl exit = set-state redu (f ++ (true ∷ bs)) (f ++ (true ∷ bs)) [] (ph env) env envl exit where -- 今回の対象をtrueにし，fとbを結合してそのListを代入する．かつそれをbに入れfをinitしてloopさせる set-state : {n : Level} {t : Set n} → ℕ → (origin state : List Bool ) → (f b : List Phi) → Env → (List Env) → (exit : List Env → t) → t -- 入れ替える必要のあるやつはphaseがThinkingのやつのみ set-state redu origin [] f b env envl exit = bit-force-search redu [] origin env (record env{ph = (f ++ b)} ∷ envl) exit -- Stateが先に尽きる set-state redu origin state@(s ∷ ss) f b env envl exit with b @@ -323,8 +323,8 @@ -- いきなりsearchしないで実行結果を持つ感じに -- stubを使うとCodeの引数がスマートになるのでやる --- 実行結果をListでもっているので、stepをじっこうしても変化がなかった場合をdeadlockとして検出したい --- 東恩納先輩とおなじように、waitに入れて評価する +-- 実行結果をListでもっているので，stepをじっこうしても変化がなかった場合をdeadlockとして検出したい +-- 東恩納先輩とおなじように，waitに入れて評価する -- 余裕があったらassertにLTLの話をいれる
--- a/Paper/src/agda/hoare-test.agda Thu May 05 17:38:06 2022 +0900 +++ b/Paper/src/agda/hoare-test.agda Thu May 05 22:32:45 2022 +0900 @@ -53,7 +53,7 @@ plus-mdg s-doing env = (var-init-x env ≡ var-init-x env) ∧ (var-init-y env ≡ var-init-y env) -- よくないmdg plus-mdg s-fin env = (var-init-x env ≡ var-init-x env) ∧ (var-init-y env ≡ var-init-y env) -- よくないmdg --- 実行のwrapperを作って、そこでmcgが適切に選ばれて接続をしたい。多分できる気がする。 +-- 実行のwrapperを作って，そこでmcgが適切に選ばれて接続をしたい．多分できる気がする． plus-init-mcg : {l : Level} {t : Set l} → (x y : ℕ) → ((env : Env ) → plus-mdg s-init env → t) → t plus-init-mcg x y next = next ( plus-init x y ( λ env → env ) ) record { proj1 = refl ; proj2 = refl } where
--- a/Paper/src/agda/hoare-test.agda.replaced Thu May 05 17:38:06 2022 +0900 +++ b/Paper/src/agda/hoare-test.agda.replaced Thu May 05 22:32:45 2022 +0900 @@ -53,7 +53,7 @@ plus-mdg s-doing env = (var-init-x env !$\equiv$! var-init-x env) !$\wedge$! (var-init-y env !$\equiv$! var-init-y env) -- よくないmdg plus-mdg s-fin env = (var-init-x env !$\equiv$! var-init-x env) !$\wedge$! (var-init-y env !$\equiv$! var-init-y env) -- よくないmdg --- 実行のwrapperを作って、そこでmcgが適切に選ばれて接続をしたい。多分できる気がする。 +-- 実行のwrapperを作って，そこでmcgが適切に選ばれて接続をしたい．多分できる気がする． plus-init-mcg : {l : Level} {t : Set l} !$\rightarrow$! (x y : !$\mathbb{N}$!) !$\rightarrow$! ((env : Env ) !$\rightarrow$! plus-mdg s-init env !$\rightarrow$! t) !$\rightarrow$! t plus-init-mcg x y next = next ( plus-init x y ( !$\lambda$! env !$\rightarrow$! env ) ) record { proj1 = refl ; proj2 = refl } where
--- a/Paper/src/agda/lambda.agda Thu May 05 17:38:06 2022 +0900 +++ b/Paper/src/agda/lambda.agda Thu May 05 22:32:45 2022 +0900 @@ -8,7 +8,7 @@ test = (ll+ 5) 7 --- +1をしたのち、もう一度+1をする関数を定義する場合 +-- +1をしたのち，もう一度+1をする関数を定義する場合 +1 : (x : ℕ )→ ℕ +1 x = suc x
--- a/Paper/src/agda/lambda.agda.replaced Thu May 05 17:38:06 2022 +0900 +++ b/Paper/src/agda/lambda.agda.replaced Thu May 05 22:32:45 2022 +0900 @@ -8,7 +8,7 @@ test = (ll+ 5) 7 --- +1をしたのち、もう一度+1をする関数を定義する場合 +-- +1をしたのち，もう一度+1をする関数を定義する場合 +1 : (x : !$\mathbb{N}$! )!$\rightarrow$! !$\mathbb{N}$! +1 x = suc x
--- a/Paper/src/agda/rbt_imple.agda Thu May 05 17:38:06 2022 +0900 +++ b/Paper/src/agda/rbt_imple.agda Thu May 05 22:32:45 2022 +0900 @@ -9,7 +9,7 @@ open import rbt_t ---このmutalの部分は別場所に書いてimportしたい。その方が綺麗に検証できそう +--このmutalの部分は別場所に書いてimportしたい．その方が綺麗に検証できそう mutual data right-List : Set where [] : right-List
--- a/Paper/src/agda/rbt_imple.agda.replaced Thu May 05 17:38:06 2022 +0900 +++ b/Paper/src/agda/rbt_imple.agda.replaced Thu May 05 22:32:45 2022 +0900 @@ -9,7 +9,7 @@ open import rbt_t ---このmutalの部分は別場所に書いてimportしたい。その方が綺麗に検証できそう +--このmutalの部分は別場所に書いてimportしたい．その方が綺麗に検証できそう mutual data right-List : Set where [] : right-List
--- a/Paper/src/agda/rbt_t.agda Thu May 05 17:38:06 2022 +0900 +++ b/Paper/src/agda/rbt_t.agda Thu May 05 22:32:45 2022 +0900 @@ -60,7 +60,7 @@ -- 右回転 --- 実行時splitへ、それ以外はmerge-treeへ +-- 実行時splitへ，それ以外はmerge-treeへ merge-rotate-right : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t merge-rotate-right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node merge-rotate-right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node @@ -90,7 +90,7 @@ = next node --- 左回転、exitはsplit_branchへ nextもsplit_branchへ +-- 左回転，exitはsplit_branchへ nextもsplit_branchへ merge-rotate-left : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t merge-rotate-left node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node merge-rotate-left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node @@ -216,9 +216,9 @@ merge env exit = merge-tree env (λ env → skew env exit ) exit -} --- skewはnextがrotate-right。exitはsplitとなる --- skewの中にrotate-rightが内包され、実行後は必ずsplitに遷移する --- それはskewのexitと等しいので同時に記述してやる。 +-- skewはnextがrotate-right．exitはsplitとなる +-- skewの中にrotate-rightが内包され，実行後は必ずsplitに遷移する +-- それはskewのexitと等しいので同時に記述してやる． skew' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t skew' env exit = skew-bt env (λ env → merge-rotate-left env exit exit ) exit
--- a/Paper/src/agda/rbt_t.agda.replaced Thu May 05 17:38:06 2022 +0900 +++ b/Paper/src/agda/rbt_t.agda.replaced Thu May 05 22:32:45 2022 +0900 @@ -60,7 +60,7 @@ -- 右回転 --- 実行時splitへ、それ以外はmerge-treeへ +-- 実行時splitへ，それ以外はmerge-treeへ merge-rotate-right : {le : Level} {t : Set le} !$\rightarrow$! Env !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t merge-rotate-right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node merge-rotate-right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node @@ -90,7 +90,7 @@ = next node --- 左回転、exitはsplit_branchへ nextもsplit_branchへ +-- 左回転，exitはsplit_branchへ nextもsplit_branchへ merge-rotate-left : {le : Level} {t : Set le} !$\rightarrow$! Env !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t merge-rotate-left node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node merge-rotate-left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node @@ -216,9 +216,9 @@ merge env exit = merge-tree env (!$\lambda$! env !$\rightarrow$! skew env exit ) exit -} --- skewはnextがrotate-right。exitはsplitとなる --- skewの中にrotate-rightが内包され、実行後は必ずsplitに遷移する --- それはskewのexitと等しいので同時に記述してやる。 +-- skewはnextがrotate-right．exitはsplitとなる +-- skewの中にrotate-rightが内包され，実行後は必ずsplitに遷移する +-- それはskewのexitと等しいので同時に記述してやる． skew!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t skew!$\prime$! env exit = skew-bt env (!$\lambda$! env !$\rightarrow$! merge-rotate-left env exit exit ) exit
--- a/Paper/src/go.go Thu May 05 17:38:06 2022 +0900 +++ b/Paper/src/go.go Thu May 05 22:32:45 2022 +0900 @@ -20,7 +20,7 @@ length := flag.Int("l", 1024, "length") //オプション,デフォルト値,ヘルプ split := flag.Int("s", 8, "task size") cpu := flag.Int("cpu", 1, "cpu") - flag.Parse() //コマンドラインを解析し、定義したオプションにセット + flag.Parse() //コマンドラインを解析し，定義したオプションにセット fmt.Println("length: ", *length); //list の長さ prefix := *length / *split //length / task size
--- a/Paper/tex/abstract.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/abstract.tex Thu May 05 22:32:45 2022 +0900 @@ -1,8 +1,8 @@ \renewcommand{\abstractname}{\normalsize 要 旨} \begin{abstract} - 当研究室にて Continuation based C\cite{cbc-gcc} (以下CbC) なるC言語の下位言語に当たる言語を開発している。 - 先行研究\cite{ryokka-master}にて Floyd-Hoare Logic\cite{hoare}(以下Hoare Logic)を用いてその検証を行なった。 - 本稿では、先行研究にて実施されなかった CbC における RedBlackTree の検証を Hoare Logic を用いて検証することを目指す。 + 当研究室にて Continuation based C\cite{cbc-gcc} (以下CbC) なるC言語の下位言語に当たる言語を開発している． + 先行研究\cite{ryokka-master}にて Floyd-Hoare Logic\cite{hoare}(以下Hoare Logic)を用いてその検証を行なった． + 本稿では，先行研究にて実施されなかった CbC における RedBlackTree の検証を Hoare Logic を用いて検証することを目指す． \end{abstract} \renewcommand{\abstractname}{\normalsize Abstract}
--- a/Paper/tex/abstract/abstract.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/abstract/abstract.tex Thu May 05 22:32:45 2022 +0900 @@ -1,7 +1,7 @@ \begin{abstract} - 当研究室にて Continuation based C (以下CbC) なるC言語の下位言語に当たる言語を開発している。 - 外間による先行研究にて Floyd-Hoare Logic(以下Hoare Logic)を用いてその検証を行なった。 - 本稿では、先行研究にて実施されなかった CbC における赤黒木の検証を Hoare Logic を用いて検証することを目指す。 + 当研究室にて Continuation based C (以下CbC) なるC言語の下位言語に当たる言語を開発している． + 外間による先行研究にて Floyd-Hoare Logic(以下Hoare Logic)を用いてその検証を行なった． + 本稿では，先行研究にて実施されなかった CbC における赤黒木の検証を Hoare Logic を用いて検証することを目指す． \\ \\ We are developing a language called Continuation based C (CbC), which is a Subordinate language of the C. M.Eng Hokama verified it by using Floyd-Hoare Logic (Hoare Logic) in a previous study.
--- a/Paper/tex/agda.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/agda.tex Thu May 05 22:32:45 2022 +0900 @@ -1,99 +1,99 @@ -Agda \cite{agda} は純粋関数型言語である。 -Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。 +Agda \cite{agda} は純粋関数型言語である． +Agda は依存型という型システムを持ち，型を第一級オブジェクトとして扱う． -Agda の記述ではインデントが意味を持ち、スペースの有無もチェックされる。 -コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。 -また、\verb/_/でそこに入りうるすべての値を示すことができ、 -\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。 +Agda の記述ではインデントが意味を持ち，スペースの有無もチェックされる． +コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される． +また，\verb/_/でそこに入りうるすべての値を示すことができ， +\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる． %% データについて -Agda では型をデータや関数に記述する必要がある。 -Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。 -このとき \verb/name/ に 空白があってはいけない。 -データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。 -\verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、 -値にコンストラクタとその型を列挙する。 +Agda では型をデータや関数に記述する必要がある． +Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する． +このとき \verb/name/ に 空白があってはいけない． +データ型は，代数的なデータ構造で，その定義には \verb/data/ キーワードを用いる． +\verb/data/ キーワードの後に \verb/data/ の名前と，型， \verb/where/ 句を書きインデントを深くし， +値にコンストラクタとその型を列挙する． -Code \ref{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。 +Code \ref{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である． \lstinputlisting[label=agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced} -\verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。 -\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており、 -\verb/suc/ を連ねることで自然数全体を表現することができる。 +\verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である． +\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており， +\verb/suc/ を連ねることで自然数全体を表現することができる． -$\mathbb{N}$ 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。 -\verb/Set/ は階層構造を持ち、型集合の集合の型を指定するには \verb/Set1/ と書く。 -%% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。 +$\mathbb{N}$ 自身の型は \verb/Set/ であり，これは Agda が組み込みで持つ「型集合の型」である． +\verb/Set/ は階層構造を持ち，型集合の集合の型を指定するには \verb/Set1/ と書く． +%% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる． -Agda には C 言語における構造体に相当するレコード型というデータも存在する、 -例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。Code \ref{agda-record}のようになる。 +Agda には C 言語における構造体に相当するレコード型というデータも存在する， +例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する．Code \ref{agda-record}のようになる． \lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/env.agda.replaced} -レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。 -複数の値を列挙するには \verb/;/ で区切る必要がある。 +レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する． +複数の値を列挙するには \verb/;/ で区切る必要がある． %% 関数について -Agda での関数は型の定義と、関数の定義をする必要がある。 -関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが、入力を受け取り出力返す型として記述される。$\rightarrow$ 、 または\verb/→/ を用いて \verb/input → output/ のように記述される。 -また、\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し、中間記法で関数を定義することもできる。 -関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。 +Agda での関数は型の定義と，関数の定義をする必要がある． +関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが，入力を受け取り出力返す型として記述される．$\rightarrow$ ， または\verb/→/ を用いて \verb/input → output/ のように記述される． +また，\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し，中間記法で関数を定義することもできる． +関数の定義は型の定義より下の行に，\verb/=/ を使い \verb/name input = output/ のように記述される． -例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。 -また、複数の引数を取る関数の型は \verb/A → A → B/ のように書ける。 -例として任意の自然数$\mathbb{N}$を受け取り、\verb/+1/した値を返す関数はCode \ref{agda-function}のように定義できる。 +例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる． +また，複数の引数を取る関数の型は \verb/A → A → B/ のように書ける． +例として任意の自然数$\mathbb{N}$を受け取り，\verb/+1/した値を返す関数はCode \ref{agda-function}のように定義できる． \lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced} -引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 -これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 -例として自然数$\mathbb{N}$の加算を関数で書くとCode \ref{agda-plus}のようになる。 +引数は変数名で受けることもでき，具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる． +これはパターンマッチと呼ばれ，コンストラクタで case 文を行なっているようなものである． +例として自然数$\mathbb{N}$の加算を関数で書くとCode \ref{agda-plus}のようになる． \lstinputlisting[label=agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced} %% \lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced} -パターンマッチでは全てのコンストラクタのパターンを含む必要がある。 -例えば、自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。 -なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。 -例えばCode \ref{agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。 +パターンマッチでは全てのコンストラクタのパターンを含む必要がある． +例えば，自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある． +なお，コンストラクタをいくつか指定した後に変数で受けることもでき，その変数では指定されたもの以外を受けることができる． +例えばCode \ref{agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る． \lstinputlisting[label=agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced} -Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、 -\verb/\arg1 arg2 → function/ または $\lambda$\verb/arg1 arg2 → function/ のように書くことができる。 -Code \ref{agda-function} で例とした \verb/+1/ をラムダ計算で書くとCode \ref{agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。 +Agda には$\lambda$計算が存在している．$\lambda$計算とは関数内で生成できる無名の関数であり， +\verb/\arg1 arg2 → function/ または $\lambda$\verb/arg1 arg2 → function/ のように書くことができる． +Code \ref{agda-function} で例とした \verb/+1/ をラムダ計算で書くとCode \ref{agda-lambda}の\verb/$\lambda$+1/ように書くことができる．この二つの関数は同一の動作をする． \lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced} -Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。 -スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 -例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリストCode \ref{agda-where} のように書ける。 -これは \verb/f'/ と同様の動作をする。 -\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 +Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる． +スコープは \verb/where/句が存在する関数内部のみであるため，名前空間が汚染させることも無い． +例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき， \verb/where/ を使うとリストCode \ref{agda-where} のように書ける． +これは \verb/f'/ と同様の動作をする． +\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し，改行の後インデントをして関数内部で利用する関数を定義する． \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} -また Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。 -\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。 -Code \ref{term} で書かれた、\verb/loop/ と \verb/stop/ は任意の自然数を受け取り、0になるまでループして0を返す関数である。 -\verb/loop/ では $\mathbb{N}$ の数を受け取り、 \verb/loop/ 自身を呼び出しながら 数を減らす関数 pred を呼んでいる。しかし、\verb/loop/の記述では関数が停止すると言えないため、定義するには\verb/{-# TERMINATING #-}/のタグが必要である。 -\verb/stop/ では自然数がパターンマッチで分けられ、\verb/zero/のときは \verb/zero/を返し、 \verb/suc n/ のときは \verb/suc/ を外した \verb/n/ で stop を実行するため停止する。 +また Agda では停止性の検出機能が存在し，プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る． +\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない． +Code \ref{term} で書かれた，\verb/loop/ と \verb/stop/ は任意の自然数を受け取り，0になるまでループして0を返す関数である． +\verb/loop/ では $\mathbb{N}$ の数を受け取り， \verb/loop/ 自身を呼び出しながら 数を減らす関数 pred を呼んでいる．しかし，\verb/loop/の記述では関数が停止すると言えないため，定義するには\verb/{-# TERMINATING #-}/のタグが必要である． +\verb/stop/ では自然数がパターンマッチで分けられ，\verb/zero/のときは \verb/zero/を返し， \verb/suc n/ のときは \verb/suc/ を外した \verb/n/ で stop を実行するため停止する． -\lstinputlisting[label=term, caption=停止しない関数 loop、停止する関数 stop] {src/termination.agda.replaced} +\lstinputlisting[label=term, caption=停止しない関数 loop，停止する関数 stop] {src/termination.agda.replaced} -このように再帰的な定義の関数が停止するときは、何らかの値が減少する必要がある。 +このように再帰的な定義の関数が停止するときは，何らかの値が減少する必要がある． \section{定理証明支援器としての Agda} -Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。 -証明の例として Code Code \ref{proof} を見る。 -ここでの \verb/+zero/ は右から \verb/zero/ を足しても ≡ の両辺は等しいことを証明している。 -これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。 +Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式， $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である． +証明の例として Code Code \ref{proof} を見る． +ここでの \verb/+zero/ は右から \verb/zero/ を足しても ≡ の両辺は等しいことを証明している． +これは，引数として受けている \verb/y/ が \verb/Nat/ なので， \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある． \lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced} -\verb/y = zero/ の時は $zero \equiv zero$ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。 +\verb/y = zero/ の時は $zero \equiv zero$ とできて，左右の項が等しいということを表す \verb/refl/ で証明することができる． \verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという -Code \ref{cong}の \verb/cong/ を使って、y の値を 1 減らしたのち、再帰的に \verb/+zero y/ -を用いて証明している。 +Code \ref{cong}の \verb/cong/ を使って，y の値を 1 減らしたのち，再帰的に \verb/+zero y/ +を用いて証明している． \lstinputlisting[caption=cong,label=cong]{src/cong.agda.replaced} %% \begin{lstlisting}[caption=等式変形の例,label=proof] @@ -105,16 +105,16 @@ %% -- cong f refl = refl %% \end{lstlisting} -また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。 -ここでは \verb/rewrite/ と ≡\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。 +また，他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している． +ここでは \verb/rewrite/ と ≡\verb/-Reasoning/ の構文を説明するとともに，等式を変形する構文の例として加算の交換則について示す． -\verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し、複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する。 -Code \ref{agda-term-post} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である。 -ここでは、\verb/+zero/ を利用し、 \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり、左右の項が等しいことを示す \verb/refl/ になっている。 +\verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し，複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する． +Code \ref{agda-term-post} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である． +ここでは，\verb/+zero/ を利用し， \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり，左右の項が等しいことを示す \verb/refl/ になっている． \lstinputlisting[caption=等式変形の例3/3,label=agda-term-post]{src/agda-term3.agda.replaced} -Code \ref{agda-term-post} では \verb/suc (y + x)/ $equiv$ \verb/y + (suc x)/ という等式に対して $equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $equiv$ \verb/suc (y + x)/の形にし、\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した。 -これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた。 +Code \ref{agda-term-post} では \verb/suc (y + x)/ $equiv$ \verb/y + (suc x)/ という等式に対して $equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $equiv$ \verb/suc (y + x)/の形にし，\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した． +これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた． -Agda ではこのような形で等式を変形しながら証明を行う事ができる。 +Agda ではこのような形で等式を変形しながら証明を行う事ができる．
--- a/Paper/tex/cbc.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/cbc.tex Thu May 05 22:32:45 2022 +0900 @@ -2,20 +2,17 @@ Continuation based C\cite{kaito-lola} （以下 CbC） は 関数呼び出しの際にjmp命令で遷移をし，環境を持たずに遷移する ことができるC言語である， -つまりC言語の下位言語にあたり，よりアセンブラに近い記述を行う． - -jmp命令であるため関数遷移をし，実行が終了しても -もとの関数に戻ることはない． -そのため次に遷移する Code Gear を指定する． -これは，関数型プログラミングでの末尾関数呼び出しに相当する． - -Code Gear に Deta Gear を与え，それをもとに処理を行い， -出力として Data Gear を返し，また次の Code Gearに遷移 -していく流れとなる． +すなわちC言語の下位言語にあたり，よりアセンブラに近い記述を行う． CbC では CodeGear を処理の単位， DataGear をデータの単位として記述するプログラミング言語である． +jmp命令で関数遷移するため関数遷移し実行が終了しても，もとの関数に戻ることはない． +そのため次に遷移する Code Gear を指定する． +これは，関数型プログラミングでの末尾関数呼び出しに相当する． +したがって，Code Gear に Deta Gear を与え，それをもとに処理を行い， +出力として Data Gear を返し，また次の Code Gearに遷移していく流れとなる． + 他のプログラミング言語とは違い， Code Gear が 暗黙の環境を持たず，受け取った Data Gear のみを もとに処理をすること，
--- a/Paper/tex/cbc_agda.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/cbc_agda.tex Thu May 05 22:32:45 2022 +0900 @@ -24,22 +24,17 @@ 最初に関数名のあとに:（コロン）の後ろに命題を記述し， そのあとに関数名のあとに引数を書き，=（イコール）の後ろに定義を記述しています． -Gears Agda での Code Gear の命題は必ず （Env $\rightarrow$ t） $\rightarrow$ t で -終了するようになっている．この （Env $\rightarrow$ t） は引数で受け取る型で Env を -受け取ってtを返すという意味になる．これが Code Gear を実行したあとの末尾関数呼び出しを -行う次の Code Gear となる． 最後にtを返すとなっているのは，これ自体が Code Gear であることを -示している． +Gears Agda での Code Gear の命題は必ず （Env $\rightarrow$ t） $\rightarrow$ t で終了するようになっている． +この （Env $\rightarrow$ t） は引数で受け取る型で Env を受け取ってtを返すという意味になる． +これが Code Gear を実行したあとの末尾関数呼び出しを行う次の Code Gear となる． +最後にtを返すとなっているのは，これ自体が Code Gear であることを示している． 受け取ったあとに別の関数に再度渡している． -これは後述するが，Agdaの繰り返し処理を行う際に停止性を -見失うために減少列を引数に取っている． - -内部の処理はreducerを減らしながらvarxを増やすことで -varyの値をvarxに与えていくことで足し算を定義している． - -基本的に繰り返し実行するコードを実装する場合には -実行時に減少し，その関数がいずれ停止することを示す -reducerを含めるようにしている． +これは後述するが，Agda の繰り返し処理を行う際に停止性を見失うために減少列を引数に取っている． +内部の処理は reducer を減らしながらvarxを増やし， +vary の値を varx に与えていくことで足し算を定義している． +基本的に繰り返し実行するコードを実装する場合には， +実行時に減少しその関数がいずれ停止することを示す reducer を含めるようにしている． reducerを含めなかった際の Code Gear を Code \ref{agda-not-cg}に示す． agdaではパターンマッチを行うことで場合分けを考えることができるが， @@ -50,12 +45,10 @@ Code \ref{agda-exec-cg} は受け取った引数で Data Gear を初期化して それを Code Gear に与えることで実行を行っている． - 今回の例では 引数から Data Gear を作成するのは 複雑ではないため，一度で Data Gear を作成してそれを Code Gear に渡している 引数から Data Gear を作成するのが複雑な場合は一度 入力から Data Gear を作成する Code Gear を用いる． - 加えて，実行なので命題の部分の最後が Env になっている． \subsection{agda による Meta Gears}
--- a/Paper/tex/continuation_agda.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/continuation_agda.tex Thu May 05 22:32:45 2022 +0900 @@ -1,9 +1,9 @@ \section{Code Gearに合わせた Agda} -検証を行うために、AgdaのコードもCbCに合わせて記述を行う必要がある。 -実際に以下がコードとなる。 +検証を行うために，AgdaのコードもCbCに合わせて記述を行う必要がある． +実際に以下がコードとなる． -CbCの特徴である、変数を継続して実行するために、必要な変数は Envc に格納する。 -コードに (next : Envc → t) と (exit : Envc → t) を引数に受け取っている。 -これで次の遷移先を引数として受け取る事で、実行を継続していることを示す。 +CbCの特徴である，変数を継続して実行するために，必要な変数は Envc に格納する． +コードに (next : Envc → t) と (exit : Envc → t) を引数に受け取っている． +これで次の遷移先を引数として受け取る事で，実行を継続していることを示す． = の後は next Envc もしくは exit Envc となっていることからも -実行を継続している事が分かる。 +実行を継続している事が分かる．
--- a/Paper/tex/dpp_impl.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/dpp_impl.tex Thu May 05 22:32:45 2022 +0900 @@ -1,9 +1,11 @@ \section{Dining Philosophers Problem} 今回はモデル検査を行う対象として Dining Philosophers Problem （以下DPP） を用いることとした． -DPPとは資源共有問題であり，モデル検査をする際に挙げられる代表的な問題 +DPP とは資源共有問題であり，モデル検査をする際に挙げられる代表的な問題 である． +DPPのストーリーを図 \ref{fig:DPP} に示している． + \begin{figure}[htpb] \begin{center} \scalebox{0.5}{\includegraphics{fig/Dining.pdf}} @@ -12,10 +14,10 @@ \label{fig:DPP} \end{figure} -問題のストーリーをまとめると以下のようになる． +問題の条件を以下に示す． \begin{itemize} - \item 哲学者がN人円卓についている（Nは2以上の自然数） + \item 哲学者が$N$人円卓についている（Nは2以上の自然数） \item 哲学者の目の前には食べ物が用意されている \item 哲学者の人数と同じだけのフォークがそれぞれ哲学者の間に置かれている \item 哲学者はしばらく思考したのち，しばらく食事する動作を繰り返しおこなう @@ -44,10 +46,12 @@ テーブルの上にフォークはすでにひとつも存在しない． すべての哲学者は左のフォークを取ろうとするが 誰も右のフォークを置くことがないため，すべての哲学者の動作がこの状態で止まる．（dead lock） - これが起こることを Gears Agda で検出したい． \subsection{Gears Agda によるDPPの実装} + +DPP の記述の主要部分を示し，説明する． + \lstinputlisting[caption= Gears Agdaでの DPP の 哲学者の状態 , label=agda-dpp-state, lastline=7]{src/agda-dpp-impl.agda.replaced} \lstinputlisting[caption= Gears Agdaでの DPP の プロセス , label=agda-dpp-process, firstline=9, lastline=16]{src/agda-dpp-impl.agda.replaced} @@ -59,9 +63,9 @@ Code \ref{agda-dpp-process}は 哲学者一人ずつの環境を持っている． -pidはその哲学者がどこに座っているかの識別子で， +pid はその哲学者がどこに座っているかの識別子で， right / left hand はフォークを手に持っているかを格納している． -next-codeは次に行う動作を格納している． +next-code は次に行う動作を格納している． Code \ref{agda-dpp-dg} が Data Gear になる． @@ -71,12 +75,12 @@ そのため実行時にListから一人ずつ取り出して実行をしていく． tableはテーブルに置いてあるフォークの状態のことで， -pidが1の人の右側にあるフォークが List の最初にあり， -pidが1の人の左側にあるフォーク，すなわちpidが2の人の右側にあるフォークが -その次のListに格納されていくようになっている． +pid が1の人の右側にあるフォークが List の最初にあり， +pid が1の人の左側にあるフォーク，すなわち pid が2の人の右側にあるフォークが +その次の List に格納されていくようになっている． また，自然数の List になっているが， その場所のフォークがテーブルの上にある場合は自然数の0が， -誰かが所持している場合はその人のpidが格納されるようになっている． +誰かが所持している場合はその人の pid が格納されるようになっている． \lstinputlisting[caption= Gears Agdaでの DPP の Data Gear のinit, label=agda-dpp-init, firstline=23, lastline=30]{src/agda-dpp-impl.agda.replaced} @@ -86,27 +90,27 @@ \lstinputlisting[caption= Gears Agdaでの DPP の step 実行, label=agda-dpp-step, firstline=31, lastline=37]{src/agda-dpp-impl.agda.replaced} -Agda では並列実行を行うことができない．そのためstep単位の実行を一つづつ行うことで +Agda では並列実行を行うことができない．そのため step 単位の実行を一つづつ行うことで 並列実行をしていることとする． この際に Env にある List Phi の中身を展開しながら一つづつ行動を処理していく． \lstinputlisting[caption=Gears Agdaでの DPP の左のフォークを取る記述, label=agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced} -Code \ref{agda-dpp-lfork}がstep実行をした際に哲学者が左側のフォークを取る記述になる． +Code \ref{agda-dpp-lfork}が step 実行をした際に哲学者が左側のフォークを取る記述になる． 左側のフォークを取る際には table の index は pid の次の値になっている． 図 \ref{fig:DPP} を見ると直感的に理解ができる． 最後の哲学者は一番最初のフォークを参照する必要がある． フォークの状態を確認し，値が0である場合はフォークがテーブルの上にあるので -それを自分のpidに書き換えleft-handをtrueに書き換えてフォークを手に持つ +それを自分の pid に書き換え left-hand を true に書き換えてフォークを手に持つ フォークの状態が0以外，すなわち他の哲学者がその場所のフォークを取得している場合は 状態を変化させずに処理を続ける． このように左のフォークを取る記述をした． 右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る． -比較するべきtableのListと哲学者のListは一致しているため，put\_lforkのように最後の哲学者が +比較するべき table の List と哲学者のListは一致しているため，put\_lfork のように最後の哲学者が 最初のフォークを参照することもない． 似たような形で哲学者がフォークを置く putdown-l/rfork を実装した．
--- a/Paper/tex/future.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/future.tex Thu May 05 22:32:45 2022 +0900 @@ -1,24 +1,24 @@ \chapter{まとめ} -本論文では、Agda による CbCの検証方法と Gears Agda による -Left Learning Red Black Tree の実装について述べた。 -したがって、Gears Agda で再起処理と再代入を含んだ -複雑なアルゴリズムも記述できる事が判明した。 +本論文では，Agda による CbCの検証方法と Gears Agda による +Left Learning Red Black Tree の実装について述べた． +したがって，Gears Agda で再起処理と再代入を含んだ +複雑なアルゴリズムも記述できる事が判明した． 今回の研究中に複雑なアルゴリズムを Gears Agda にて実装することで -得られた知見は、今後の研究で大いに役立つと考える。 +得られた知見は，今後の研究で大いに役立つと考える． -今後の課題として、検証を行う事が挙げられる。 -検証には、Meta Code Gear が Pre / Post Condition の条件を -満たしているのか比較を行い、Hoare Logicに当てはめる事。 -そして接続された条件の接続と健全性の証明を行う必要がある。 -しかし、Imple を用いた Hoare Logic による証明は、 -While Loop でも かなり長いコードになっていた。 +今後の課題として，検証を行う事が挙げられる． +検証には，Meta Code Gear が Pre / Post Condition の条件を +満たしているのか比較を行い，Hoare Logicに当てはめる事． +そして接続された条件の接続と健全性の証明を行う必要がある． +しかし，Imple を用いた Hoare Logic による証明は， +While Loop でも かなり長いコードになっていた． これで Left Learning Red Black Tree の検証を -行うのは難しいため、別の手法を模索することも念頭に入れる。 +行うのは難しいため，別の手法を模索することも念頭に入れる． -展望としては、Gears Agda コードから CbC コードの変換をしたい。 -Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが、 -CbC はC言語とアセンブラの中間に位置しているため、コーディングはさらに困難である。 -そのため、Gears Agdaのコードを CbC に変換できるようにしたい。 -これができるようになれば、CbC での記述も Agda での証明も容易になると考えている。 +展望としては，Gears Agda コードから CbC コードの変換をしたい． +Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが， +CbC はC言語とアセンブラの中間に位置しているため，コーディングはさらに困難である． +そのため，Gears Agdaのコードを CbC に変換できるようにしたい． +これができるようになれば，CbC での記述も Agda での証明も容易になると考えている．
--- a/Paper/tex/hoare.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/hoare.tex Thu May 05 22:32:45 2022 +0900 @@ -1,35 +1,35 @@ \section{Hoare Logic} -Hoare Logic\ref{hoare} とは C.A.R Hoare、 -R.W Floyd が考案したプログラムの検証の手法である。 -これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」 -というもので、CbCの実行を継続するという性質に非常に相性が良い。 -Hoare Logic を表記すると以下のようになる。 +Hoare Logic\ref{hoare} とは C.A.R Hoare， +R.W Floyd が考案したプログラムの検証の手法である． +これは，「プログラムの事前条件(P)が成立しているとき，コマンド(C)実行して停止すると事後条件(Q)が成り立つ」 +というもので，CbCの実行を継続するという性質に非常に相性が良い． +Hoare Logic を表記すると以下のようになる． $$ \{P\}\ C \ \{Q\} $$ -この3つ組は Hoare Triple と呼ばれる。 +この3つ組は Hoare Triple と呼ばれる． -Hoare Triple の事後条件を受け取り、 -異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。 +Hoare Triple の事後条件を受け取り， +異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく． -Hoare Logic の検証では、 -「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。 -これらを満たし、 -事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。 +Hoare Logic の検証では， +「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である． +これらを満たし， +事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる． \subsection{Hoare Logic による Code Gear の検証手法 } -\figref{hoare}が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる。 -input DataGear が Hoare Logic上の Pre Condition(事前条件)となり、 -output DataGear が Post Conditionとなる。 -各DataGear が Pre / Post Condition を満たしているかの検証は、 -各 Condition を Meta DataGear で定義し、 -条件を満たしているのかをMeta CodeGear で検証する。 +\figref{hoare}が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる． +input DataGear が Hoare Logic上の Pre Condition(事前条件)となり， +output DataGear が Post Conditionとなる． +各DataGear が Pre / Post Condition を満たしているかの検証は， +各 Condition を Meta DataGear で定義し， +条件を満たしているのかをMeta CodeGear で検証する． \begin{figure}[H] \begin{center} \includegraphics[height=2.4cm]{fig/hoare_cg_dg.pdf} \end{center} - \caption{CodeGear、DataGear での Hoare Logic} + \caption{CodeGear，DataGear での Hoare Logic} \label{hoare} \end{figure}
--- a/Paper/tex/intro.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/intro.tex Thu May 05 22:32:45 2022 +0900 @@ -3,41 +3,32 @@ 思い思いにプログラムを書くと，冗長なコードができてしまい， 実行時間も遅い場合がある． - この場合にコードに対してアルゴリズムを適応すると実行が最適化され 実行時間が減り，かつ第三者がコードを読んだ際にロジックが統一されているため理解が容易くなる． つまり，一般的に良いコードが作成できる． - しかし，世の中にはすでに大量のアルゴリズムが存在するため， これを一人のプログラマーが全て覚え，適応できる場面を思いつくというのは不可能に近い． その道に詳しい人が複数人いる場面というのも稀だと考えられる． - そのため，人が書いたコードに対してアルゴリズムを使用するコードに変換できるようにしたい． - この際，アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい． 一般的なプログラミング言語では，関数の遷移が自由であることから，関数遷移などで発生した 暗黙の環境が存在するためである． この問題を解決するため，Gears Agda を用いる． - Gears Agda とは当研究室で開発している Continuation based C （CbC） の概念を取り入れた記法で書かれた Agda のことで， 通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する． この際メインルーチンで使用していた変数などの環境はスタックされ，サブルーチンが終了した際にメインルーチンに戻り， スタックしていた変数をもとに戻す流れとなる． -CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ，スタックを持たず環境を保持しない． +CbC の場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ，スタックを持たず環境を保持しない． 更に遷移後にメインルーチンに戻ることもない． つまり関数の実行では暗黙な環境が存在せず，関数が受け取った引数のみを使用する． これにより限定的な実行条件を作成でき，検証がしやすくなる． 現在，アルゴリズムの適応可否は以下の方法を考えている． - あらかじめ，アルゴリズムの実装と検証をおこなったアルゴリズムSetsを用意しておく． - 書いたコードが事前に定義していたアルゴリズムの仕様を満たしているかを検証していき， 満たしているコードがあった場合にそのコードを事前に定義してあるアルゴリズムに入れ替える方針を考えている． - この際，実装が仕様を満たしているか検証する手法には，定理証明やモデル検査などが挙げられる． - アルゴリズムの入れ替え可否判定には Gears Agda でモデル検査を行い， アルゴリズムの仕様がコードに適応できるか検証するのが妥当だと考えている． 思い思いに書いたコードに対して定理証明を行うのはコストが高く，適応するものの内部動作が一致しない場合定理証明を行っても使えないためである．
--- a/Paper/tex/intro/intro.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/intro/intro.tex Thu May 05 22:32:45 2022 +0900 @@ -1,15 +1,15 @@ \section{研究目的} - OS やアプリケーションの信頼性を高めることは重要な課題である。 - 信頼性を高める為には仕様を満たしたプログラムが実装されていることを検証する必要がある。 - 具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。 + OS やアプリケーションの信頼性を高めることは重要な課題である． + 信頼性を高める為には仕様を満たしたプログラムが実装されていることを検証する必要がある． + 具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる． - 研究室で CbC という言語を開発している。 - CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。 - この言語の信用性を検証したい。 + 研究室で CbC という言語を開発している． + CbC とは，C言語からループ制御構造とサブルーチンコールを取り除き，継続を導入した C言語の下位言語である． + この言語の信用性を検証したい． - 仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。 - Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、 - に事後条件が成り立つことでコマンドの検証を行う。 + 仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている． + Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に， + に事後条件が成り立つことでコマンドの検証を行う． - CbC の実行を継続するという性質が Hoare Logic の事前条件と事後条件の定義から検証を行うことと非常に相性が良い。 - これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。 + CbC の実行を継続するという性質が Hoare Logic の事前条件と事後条件の定義から検証を行うことと非常に相性が良い． + これらのことから，本稿では Hoare Logic を用いて CbC を検証することを目指す．
--- a/Paper/tex/rbt_imple.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/rbt_imple.tex Thu May 05 22:32:45 2022 +0900 @@ -1,14 +1,14 @@ \chapter{Red Black Tree の実装} -Left Learning Red Black Tree の実装において、 +Left Learning Red Black Tree の実装において， 通常の言語であれば再起処理を用いて実装を行える部分を -継続にて実行可能なように変更する必要がある。 -本節では、この課題に対して Gears Agda での -Left Learning Red Black Tree の実装方法について述べる。 +継続にて実行可能なように変更する必要がある． +本節では，この課題に対して Gears Agda での +Left Learning Red Black Tree の実装方法について述べる． \section{Gears Agda での Red Black Tree の 記述} -Gears Agda にて Red Black Tree を実装する際の手順を、 -下\figref{rbt_imple}を参考に説明する。 +Gears Agda にて Red Black Tree を実装する際の手順を， +下\figref{rbt_imple}を参考に説明する． \begin{figure}[H] \begin{center} @@ -18,103 +18,103 @@ \label{rbt_imple} \end{figure} -41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説明する。 -まず Root node である 59 と比較した際に、41はそれより小さい。 -この際、left node に遷移するが、CbC では再起処理が行えないため、listに保持していく。 -順々に辿っていき、対象の場所に到達すると insert / delete を行う。 -その後はlistからnodeを取り出し、結合することで Left Leaning Red Black Tree の操作を行う。 +41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説明する． +まず Root node である 59 と比較した際に，41はそれより小さい． +この際，left node に遷移するが，CbC では再起処理が行えないため，listに保持していく． +順々に辿っていき，対象の場所に到達すると insert / delete を行う． +その後はlistからnodeを取り出し，結合することで Left Leaning Red Black Tree の操作を行う． \subsection{定義した Data Gear の記述} -Left Learning Red Black Tree の記述の際に、 Code Gear -に渡している Data Gear である Env の記述を \coderef{env_imple} に示す。 +Left Learning Red Black Tree の記述の際に， Code Gear +に渡している Data Gear である Env の記述を \coderef{env_imple} に示す． \lstinputlisting[label=env_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=13, lastline=39] {src/agda/rbt_t.agda} -箇条書きにてそれぞれについて解説を行う。 +箇条書きにてそれぞれについて解説を行う． \begin{itemize} -\item col: 色のことで、red と black の data 型で記述し、パターンマッチを行う。 -\item node: その名の通り node に格納されている値を保存する。 色と自然数が入る -\item tree: tree の構造 を保存する。ここで node と x / right tree を持つ +\item col: 色のことで，red と black の data 型で記述し，パターンマッチを行う． +\item node: その名の通り node に格納されている値を保存する． 色と自然数が入る +\item tree: tree の構造 を保存する．ここで node と x / right tree を持つ \item rbt: 上3つの要素を合わせて持つことで Left Learning Red Black Tree を定義する -\item Env: rbt 以外に追加や削除を行う対象となる値と、 rbtを保存できる List を持つ Data Gear +\item Env: rbt 以外に追加や削除を行う対象となる値と， rbtを保存できる List を持つ Data Gear \end{itemize} \subsection{目的の node まで辿る Gears Agda} -上記に示した手順通りにAgdaで記述すると下 \coderef{insert_imple}のようになる。 -例は insert を行う場合の記述となる。 +上記に示した手順通りにAgdaで記述すると下 \coderef{insert_imple}のようになる． +例は insert を行う場合の記述となる． \lstinputlisting[label=insert_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=157, lastline=166] {src/agda/rbt_t.agda} -ソースコードの解説をする。上から3行はコメントで、この関数で行っていることを doに、 -next / exit では4章で述べた次の関数遷移先を記載している。 +ソースコードの解説をする．上から3行はコメントで，この関数で行っていることを doに， +next / exit では4章で述べた次の関数遷移先を記載している． -5行目にて withを使用することで vart のパターンマッチを行っている。 -vart が bt-empty である場合に 6行目が動作する。 -bt-empty であれば node の一番下であるため、 -varn を tree の値として insert して exit に遷移する。 +5行目にて withを使用することで vart のパターンマッチを行っている． +vart が bt-empty である場合に 6行目が動作する． +bt-empty であれば node の一番下であるため， +varn を tree の値として insert して exit に遷移する． -7行目は vart が bt-empty ではないパターンの動作を記述している。 -ここでは insertを行う値である varn と 現在いる位置の tree の値と比較を行い、 -再度パターンマッチを行う。 +7行目は vart が bt-empty ではないパターンの動作を記述している． +ここでは insertを行う値である varn と 現在いる位置の tree の値と比較を行い， +再度パターンマッチを行う． -8行目は比較した結果、同値だった場合であり、そのままexitに遷移している。 +8行目は比較した結果，同値だった場合であり，そのままexitに遷移している． -9行目は入力の値 varn の方が小さい場合を指している。 -vart に left tree を入れ、varl には 現在の tree から left treeを除いた -treeを追加している。それを next に遷移させている。 +9行目は入力の値 varn の方が小さい場合を指している． +vart に left tree を入れ，varl には 現在の tree から left treeを除いた +treeを追加している．それを next に遷移させている． -10行目は入力の値 varn の方が大きい場合を指している。 -9行目とは逆に、vart に right tree を入れ、varl には 現在の tree から right treeを除いた -treeを追加している。それをまたnext に遷移させている。 +10行目は入力の値 varn の方が大きい場合を指している． +9行目とは逆に，vart に right tree を入れ，varl には 現在の tree から right treeを除いた +treeを追加している．それをまたnext に遷移させている． -以上の手順により、目的の node まで辿っている。 +以上の手順により，目的の node まで辿っている． \subsection{目的の node まで辿った後の Gears Agda} -目的の node にたどり着いた後、List に格納された tree と vart の結合を行う。 -Gears Agda でそれを記述すると\coderef{mearge_imple}のようになる。 +目的の node にたどり着いた後，List に格納された tree と vart の結合を行う． +Gears Agda でそれを記述すると\coderef{mearge_imple}のようになる． \lstinputlisting[label=mearge_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=145, lastline=155] {src/agda/rbt_t.agda} -ソースコードの解説をする。 -5行目にて with を使用して varl についてパターンマッチを行っている。 +ソースコードの解説をする． +5行目にて with を使用して varl についてパターンマッチを行っている． -6行目が varl に何も入っていない場合で、実行終了のため exitに遷移している。 +6行目が varl に何も入っていない場合で，実行終了のため exitに遷移している． -7行目は varl に何か入っていた場合で、ここでは varl に入っているものが -何であるのか8行目と合わせてパターンマッチを行っている。 -ここでは varl に入っていたものが bt-empty であった場合について記述されている。 -bt-emptyが入ってくることは実装上ありえないので、exitに遷移することで強制終了している。 +7行目は varl に何か入っていた場合で，ここでは varl に入っているものが +何であるのか8行目と合わせてパターンマッチを行っている． +ここでは varl に入っていたものが bt-empty であった場合について記述されている． +bt-emptyが入ってくることは実装上ありえないので，exitに遷移することで強制終了している． -8行目では varl に入っていたものが bt-empty ではなかった場合で、 -それをxtreeと命名している。 -ここで vart に入っている値と xtree に入っている値を比較を行い、 -さらにパターンマッチを行う。 +8行目では varl に入っていたものが bt-empty ではなかった場合で， +それをxtreeと命名している． +ここで vart に入っている値と xtree に入っている値を比較を行い， +さらにパターンマッチを行う． -9行目が入っている値と同じ値であった場合で、 -特に操作する必要がないので vart に xtree を入れ、 -varl を一つ進める。 +9行目が入っている値と同じ値であった場合で， +特に操作する必要がないので vart に xtree を入れ， +varl を一つ進める． -10行目は vartが大きい場合で、 -varnに xtree の値を入れ、 +10行目は vartが大きい場合で， +varnに xtree の値を入れ， xtree の right tree に 現在のvart を入れたものを vartにして -varlを一つ進めている。 +varlを一つ進めている． -11行目は vartが小さい場合で、 -10行目と逆のことをしている。 -varnに xtree の値を入れ、 +11行目は vartが小さい場合で， +10行目と逆のことをしている． +varnに xtree の値を入れ， xtree の left tree に 現在のvart を入れたものを vartにして -varlを一つ進めている。 +varlを一つ進めている． -以上の組み合わせを行い、 +以上の組み合わせを行い， Gears Agda にて 再起処理を使わず に Left Learning Red Black Tree の insert / delete を -記述した。 +記述した． -% 以上のように Tree の基本操作である insert, find, delete の実装を行った。 +% 以上のように Tree の基本操作である insert, find, delete の実装を行った．
--- a/Paper/tex/rbt_intro.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/rbt_intro.tex Thu May 05 22:32:45 2022 +0900 @@ -1,20 +1,20 @@ \chapter{Red Black Tree} -実装を行う Red Black Tree の説明を行う。 -Red Black Tree は 木構造の基本操作である Insert(挿入)、Delete(削除)、Search(検索)の -いずれに置いても最悪実行時間が $O(log \: n)$であり、データ構造のうちで最善のものの一つである。 -そのため、実用的なデータ構造として知られている。 +実装を行う Red Black Tree の説明を行う． +Red Black Tree は 木構造の基本操作である Insert(挿入)，Delete(削除)，Search(検索)の +いずれに置いても最悪実行時間が $O(log \: n)$であり，データ構造のうちで最善のものの一つである． +そのため，実用的なデータ構造として知られている． \section{Tree} -Tree (木構造)とは、非常に有用なデータ構造である。 -\figref{tree}の○の部分を node (節) と呼び、top node を root(根) と呼ぶ。 -特に、根を持つ木構造のことを強調して、Rooted Tree (根付き木) と呼ぶ事がある。 +Tree (木構造)とは，非常に有用なデータ構造である． +\figref{tree}の○の部分を node (節) と呼び，top node を root(根) と呼ぶ． +特に，根を持つ木構造のことを強調して，Rooted Tree (根付き木) と呼ぶ事がある． \section{Binary Tree} 各 node からすぐ下に辺で結ばれている node を -その node の child またはson (子あるいは子供)と呼ぶ。 -child 側から上の辺を parent (親) と呼ぶ。 -\figref{bt}のように、各 node が持つ child が高々2つである Tree を Binary Tree (2分木)と呼ぶ。 +その node の child またはson (子あるいは子供)と呼ぶ． +child 側から上の辺を parent (親) と呼ぶ． +\figref{bt}のように，各 node が持つ child が高々2つである Tree を Binary Tree (2分木)と呼ぶ． \begin{figure}[htbp] \begin{minipage}{0.5\hsize} @@ -34,7 +34,7 @@ \end{figure} \section{Binary Search Tree} -Rooted Binary Tree に対して、 以下の制約を持つものを、Binary Search Tree と呼ぶ。 +Rooted Binary Tree に対して， 以下の制約を持つものを，Binary Search Tree と呼ぶ． $左側の子孫にある要素 < 親 < 右側の子孫にある要素$ @@ -49,19 +49,19 @@ \end{figure} \section{RedBlackTree} -RedBlackTree (または赤黒木)とは平衡2分探索木の一つである。 -2分探索木の点にランクという概念を追加し、そのランクの違いを赤と黒の色で分け、 +RedBlackTree (または赤黒木)とは平衡2分探索木の一つである． +2分探索木の点にランクという概念を追加し，そのランクの違いを赤と黒の色で分け， 以下の定義に基づくように -木を構成した物である。図では省略しているが、値を持っている点の下に黒色の空の葉があり、 -それが外点となる。 +木を構成した物である．図では省略しているが，値を持っている点の下に黒色の空の葉があり， +それが外点となる． \begin{enumerate} - \item 各点は赤か黒の色である。 - \item 点が赤である場合の親となる点の色は黒である。 - \item 外点(葉。つまり一番下の点)は黒である。 - \item 任意の点から外点までの黒色の点はいずれも同数となる。 + \item 各点は赤か黒の色である． + \item 点が赤である場合の親となる点の色は黒である． + \item 外点(葉．つまり一番下の点)は黒である． + \item 任意の点から外点までの黒色の点はいずれも同数となる． \end{enumerate} -参考となる\figref{rbt}を以下に示す。上記の定義を満たしていることが分かる。 +参考となる\figref{rbt}を以下に示す．上記の定義を満たしていることが分かる． \begin{figure}[H] \begin{center} @@ -72,18 +72,18 @@ \end{figure} \section{Left Learning Red Black Tree} -Left Learing Red Black Tree とは Red Black Tree の変形である。 -Red Black Tree の 仕様を満たしながら、実装が容易である。 +Left Learing Red Black Tree とは Red Black Tree の変形である． +Red Black Tree の 仕様を満たしながら，実装が容易である． \figref{rbt}に入っていた値を Left Learning Red Black Tree に適応した場合を -\figref{llrbt}に示す。 +\figref{llrbt}に示す． Left Learning Red Black Tree では赤色の node は parent から見て -左の node にしか 現れない Red Black Tree となる。 -これにより、パターンマッチの分岐を減らす事ができ、実装が容易になる。 +左の node にしか 現れない Red Black Tree となる． +これにより，パターンマッチの分岐を減らす事ができ，実装が容易になる． -本来の Red Black Tree の実装は困難であるため、 +本来の Red Black Tree の実装は困難であるため， 本論では Red Black Tree の仕様を満たしている -Left Learning Red Black Tree を検証する。 +Left Learning Red Black Tree を検証する． \begin{figure}[H] \begin{center}
--- a/Paper/tex/rbt_verif.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/rbt_verif.tex Thu May 05 22:32:45 2022 +0900 @@ -1,62 +1,62 @@ \chapter{Left Learning Red Black Tree の検証} -本章では、Left Learning Red Black Tree の +本章では，Left Learning Red Black Tree の 検証方法について述べる \section{Meta Data Gearの記述} -検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と -比較することで Hoare Triple に当てはめることは第5章で前述した。 +検証するにあたり，Meta Deta Gear を作成し Pre / Post Condition と +比較することで Hoare Triple に当てはめることは第5章で前述した． \subsection{大小関係を検証する Meta Data Gear} -Red Black Tree は Binary Search Tree の 定義を持っているので、 -parent から見て left node には parent の値より小さい値が、 -right node には大きい値が入る。これを検証する必要がある。 +Red Black Tree は Binary Search Tree の 定義を持っているので， +parent から見て left node には parent の値より小さい値が， +right node には大きい値が入る．これを検証する必要がある． -大小関係を検証するにあたり、Fresh List を用いた検証手法が考えられた。 -Fresh Listの記述を\coderef{fresh}に示す。 -% ソースコードを載せる。 +大小関係を検証するにあたり，Fresh List を用いた検証手法が考えられた． +Fresh Listの記述を\coderef{fresh}に示す． +% ソースコードを載せる． \lstinputlisting[label=fresh, caption=Fresh List の定義, firstline=47,lastline=49] {src/agda/_fresh.agda} -これを用いて Frash List への定数の insert を\coderef{fresh-test}に示す。 +これを用いて Frash List への定数の insert を\coderef{fresh-test}に示す． \lstinputlisting[label=fresh-test, caption=Fresh List への定数のinsert, firstline=10,lastline=15] {src/agda/fresh_test.agda} -Fresh Listは一つの値に対して、それより後の値との大小関係の証明が入っている。 -そのため、正確性が増すが、関数内でFresh List への insert は困難であったため、 +Fresh Listは一つの値に対して，それより後の値との大小関係の証明が入っている． +そのため，正確性が増すが，関数内でFresh List への insert は困難であったため， 証明付き Data 構造を持った List を \coderef{list_v} -のように定義した。 +のように定義した． \lstinputlisting[label=list_v, caption=証明付き Data 構造を持った List,firstline=12,lastline=30] {src/agda/rbt_varif.agda} -証明付き Data 構造を持った List の定義は right-List で行っている。 -List の Top と比較した際に、 -Topの値より大きい値でなければ insert できない。 -加えて insert できた値が Top より大きい事を示す証明も持つ事ができる。 +証明付き Data 構造を持った List の定義は right-List で行っている． +List の Top と比較した際に， +Topの値より大きい値でなければ insert できない． +加えて insert できた値が Top より大きい事を示す証明も持つ事ができる． -mutual は 以下の記述全てに対して掛かっている。 -これは right-List の定義の中で、top-r を呼び出しており、 -top-r は定義の部分で right-List を使用している。 -したがって相互呼び出しとなっている。 -Agdaは 逐次処理であるため、プログラムの上に宣言してある関数や型しか使用できない。 -mutual を掛けることで、プログラムの下で宣言している関数や型を使用する事ができる。 +mutual は 以下の記述全てに対して掛かっている． +これは right-List の定義の中で，top-r を呼び出しており， +top-r は定義の部分で right-List を使用している． +したがって相互呼び出しとなっている． +Agdaは 逐次処理であるため，プログラムの上に宣言してある関数や型しか使用できない． +mutual を掛けることで，プログラムの下で宣言している関数や型を使用する事ができる． -right-List の定義は、何も入っていない場合は right-List で停止するようにしている。 -List に一つしか値が入っていない場合は、証明付き Data 構造を持つ必要がない。 -そのため特記して記述している。 -List に他の値が入っている場合は、top とその次の値との比較を証明を持っている。 +right-List の定義は，何も入っていない場合は right-List で停止するようにしている． +List に一つしか値が入っていない場合は，証明付き Data 構造を持つ必要がない． +そのため特記して記述している． +List に他の値が入っている場合は，top とその次の値との比較を証明を持っている． -top-r は Listに入っている Top の値を持ってくる関数を記述している。 -insert-r は right-List に 値を insert するための関数で、 -right-List の top と入れる引数を比較し、 +top-r は Listに入っている Top の値を持ってくる関数を記述している． +insert-r は right-List に 値を insert するための関数で， +right-List の top と入れる引数を比較し， inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を -持った List となっている。 +持った List となっている． -これを Left Learning Red Black Tree の 仕様を満たすように、 -全てに対して行う。 -その後、条件が接続されているのかを検証したのち、健全性について示す事で -Hoare Logic による検証ができる。 +これを Left Learning Red Black Tree の 仕様を満たすように， +全てに対して行う． +その後，条件が接続されているのかを検証したのち，健全性について示す事で +Hoare Logic による検証ができる． %\subsection{Black node の数え上げ} -%他にも、Left Learning Red Brack Tree の black node の数え上げを記述した。 +%他にも，Left Learning Red Brack Tree の black node の数え上げを記述した． %\subsection{Meta Data Gear の作成}
--- a/Paper/tex/spec.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/spec.tex Thu May 05 22:32:45 2022 +0900 @@ -1,31 +1,31 @@ \section{検証手法} -本章では検証する際の手法を説明する。 -CodeGear の引数となる DataGear が事前条件となり、 -それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。 -その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。 -これらを用いて Hoare Logic によりプログラムの検証を行いたい。 +本章では検証する際の手法を説明する． +CodeGear の引数となる DataGear が事前条件となり， +それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する． +その後，さらに事後条件となる DetaGear も Meta Gears にて検証する． +これらを用いて Hoare Logic によりプログラムの検証を行いたい． \subsection{CbC記法で書くagda} -CbCプログラムの検証をするに当たり、AgdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。 -\coderef{agda-cg}が例となるコードである。 +CbCプログラムの検証をするに当たり，AgdaコードもCbC記法で記述を行う．つまり継続渡しを用いて記述する必要がある． +\coderef{agda-cg}が例となるコードである． \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda} -前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。 -これがAgdaで表現された CodeGear となる。 +前述した加算を行うコードと比較すると，不定の型 (t) により継続を行なっている部分が見える． +これがAgdaで表現された CodeGear となる． \subsection{agda による Meta Gears} -通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。 -今回はその Meta Gears をAgdaによる検証の為に用いる。 +通常の Meta Gears はノーマルレベルの CodeGear， DataGear では扱えないメタレベルの計算を扱う単位である． +今回はその Meta Gears をAgdaによる検証の為に用いる． \begin{itemize} \item Meta DataGear \mbox{}\\ - Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。 - これを用いることで、仕様となる制約条件を記述することができる。 + Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる． + これを用いることで，仕様となる制約条件を記述することができる． \item Meta CodeGear\mbox{}\\ Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear - である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 - す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである + である．Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 + す CodeGear である．故に，Meta CodeGear は Agda で記述した CodeGear の検証そのものである \end{itemize}
--- a/Paper/tex/spec/spec.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/spec/spec.tex Thu May 05 22:32:45 2022 +0900 @@ -1,24 +1,24 @@ \section{検証手法} - 手法は模索中であり、先行研究と同じ手法を取ろうとしている。本章では先行研究で述べられている検証手法について説明する。 + 手法は模索中であり，先行研究と同じ手法を取ろうとしている．本章では先行研究で述べられている検証手法について説明する． \subsection{CbC記法で書くagda} - CbCプログラムの検証をするに当たり、agdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。 - 以下が例となるコードである。 - 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。 - これがAgdaで表現された CodeGear となる。 + CbCプログラムの検証をするに当たり，agdaコードもCbC記法で記述を行う．つまり継続渡しを用いて記述する必要がある． + 以下が例となるコードである． + 前述した加算を行うコードと比較すると，不定の型 (t) により継続を行なっている部分が見える． + これがAgdaで表現された CodeGear となる． \subsection{agda による Meta Gears} - 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。 - Meta DataGear はメタ計算で使われる DataGear で、実行するメタ計算によって異なる。 - 今回はその Meta Gears をagdaによる検証の為に用いる。 - 検証での Meta Gears は DataGear が持つ同値関係や、 - 大小関係などの関係を表す DataGear がそれに当たると考えられる。 - Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。 - 以下が While Program での制約条件をまとめたものになる。 - Agdaにおける Meta DataGear のコードを載せる。 + 通常の Meta Gears はノーマルレベルの CodeGear， DataGear では扱えないメタレベルの計算を扱う単位である． + Meta DataGear はメタ計算で使われる DataGear で，実行するメタ計算によって異なる． + 今回はその Meta Gears をagdaによる検証の為に用いる． + 検証での Meta Gears は DataGear が持つ同値関係や， + 大小関係などの関係を表す DataGear がそれに当たると考えられる． + Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる． + 以下が While Program での制約条件をまとめたものになる． + Agdaにおける Meta DataGear のコードを載せる． \lstinputlisting[label=pg:sample]{./src/agda-mdg.agda} - whileTestState で Meta DataGear を識別するためのデータを分け、 - whileTestStatePでそれぞれの Meta DataGear を返している。 + whileTestState で Meta DataGear を識別するためのデータを分け， + whileTestStatePでそれぞれの Meta DataGear を返している． ここでは = の後ろの (vari env ≡ 0) (varn env ≡ - c10 env)/ などのデータを Meta DataGear として扱う。 + c10 env)/ などのデータを Meta DataGear として扱う． aa
--- a/Paper/tex/thanks.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/thanks.tex Thu May 05 22:32:45 2022 +0900 @@ -1,12 +1,12 @@ \chapter*{謝辞} -本研究の水光、本論文の作成にあたり、御多忙にも関わらず終始懇切丁寧なる御指導と御教授 -を賜わりました、河野真治准教授に心より感謝致します。そして、 共に研究を行い暖か +本研究の水光，本論文の作成にあたり，御多忙にも関わらず終始懇切丁寧なる御指導と御教授 +を賜わりました，河野真治准教授に心より感謝致します．そして， 共に研究を行い暖か な気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致しま -す。また、全員最終学年であるにもかかわらず、本コースのシステム更新に関わったシス -テム管理チームに感謝いたします。 -最後に、 有意義な時間を共に過ごした理工学研究科情報工学専攻の学友、 -並びに物心両面で支えてくれた家族に深く感謝致します。 +す．また，全員最終学年であるにもかかわらず，本コースのシステム更新に関わったシス +テム管理チームに感謝いたします． +最後に， 有意義な時間を共に過ごした理工学研究科情報工学専攻の学友， +並びに物心両面で支えてくれた家族に深く感謝致します． \thispagestyle{empty}
--- a/Paper/tex/tree_desc.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/tree_desc.tex Thu May 05 22:32:45 2022 +0900 @@ -1,13 +1,13 @@ \section{Gears Agda における木構造の設計} -本研究では、Gears Agda にて Red Black Tree の検証を行うにあたり、 -Agda が変数に対して再代入を許していないことが問題になってくる。 +本研究では，Gears Agda にて Red Black Tree の検証を行うにあたり， +Agda が変数に対して再代入を許していないことが問題になってくる． -そのため下図 \ref{rbt-stack} のように、木構造の root から leaf に 辿る際に見ているnodeから -下の tree をそのまま stack に持つようにする。 +そのため下図 \ref{rbt-stack} のように，木構造の root から leaf に 辿る際に見ているnodeから +下の tree をそのまま stack に持つようにする． -そして insert や delete を行った後に stack から tree を取り出し、 -元の木構造を再構築 していきながら rootへ戻る。 +そして insert や delete を行った後に stack から tree を取り出し， +元の木構造を再構築 していきながら rootへ戻る． \begin{figure}[H] \begin{center} @@ -18,91 +18,91 @@ \end{figure} -このようにして Gears Agda にて Red Black Tree を実装していく。 +このようにして Gears Agda にて Red Black Tree を実装していく． \section{Gears Agda における Binary Tree の実装} -Red Black Tree を実装しそれを検証する前段階として、 -実装が簡単な Binary Tree の実装から行う。 +Red Black Tree を実装しそれを検証する前段階として， +実装が簡単な Binary Tree の実装から行う． -まず Binary Tree と 遷移させる Data Gear となる Env の定義は Code \ref{bt_env} のようになる。 +まず Binary Tree と 遷移させる Data Gear となる Env の定義は Code \ref{bt_env} のようになる． \lstinputlisting[label=bt_env, caption=Binary Tree の Data Gear] {src/bt_impl/bt_env.agda.replaced} -bt は、木での順序としての意味を持つ key とその中身 value はどのような型でも入れられるように -「A : Set n」となっている。 -そして left, right には bt A を持つようにし、木構造を構築している。 +bt は，木での順序としての意味を持つ key とその中身 value はどのような型でも入れられるように +「A : Set n」となっている． +そして left, right には bt A を持つようにし，木構造を構築している． -Env では、 find, insert, delete の対象となる値を保存し、 Code Gear に与えられるようにするために -varn, varv を持っている。 -加えて変更を加える bt を持つ vart と、章Nで前述した木構造を持っておくための List である -varl を Env に設定している。 +Env では， find, insert, delete の対象となる値を保存し， Code Gear に与えられるようにするために +varn, varv を持っている． +加えて変更を加える bt を持つ vart と，章Nで前述した木構造を持っておくための List である +varl を Env に設定している． 7章で述べた Gears Agda での木構造を保ったまま root から目的のnodeまで辿る Code Gear が -Code \ref{bt_find_impl} になる。 +Code \ref{bt_find_impl} になる． \lstinputlisting[label=bt_find_impl, caption=root から目的のnodeまで辿る Code Gear] {src/bt_impl/find.agda.replaced} -まず、関数の実装が始まってすぐに Env の vartを指定したものと引数をそのまま find-c の関数に遷移している。 -ここで展開しているのは Env の vart で、そのまま Env から展開した vart をパターンマッチすると -Agda が追えなくなってしまい、\{-$\#$ TERMINATING $\#$-\} を使用することになってしまう。 +まず，関数の実装が始まってすぐに Env の vartを指定したものと引数をそのまま find-c の関数に遷移している． +ここで展開しているのは Env の vart で，そのまま Env から展開した vart をパターンマッチすると +Agda が追えなくなってしまい，\{-$\#$ TERMINATING $\#$-\} を使用することになってしまう． -そのため関数を新たに定義し、展開したものを受け取り、パターンマッチすることで +そのため関数を新たに定義し，展開したものを受け取り，パターンマッチすることで \{-$\#$ TERMINATING $\#$-\} を使用せずに loopを定義できるようになる -木を stack に入れるのは単純で、操作の対象の key となる varn と -node のkeyを比較を行う。 -そこからは本来の木構造と同じで、操作の対象の key が小さいなら -left の tree を次の node として遷移する。 -大きいなら right の tree を次の node として遷移していく。 +木を stack に入れるのは単純で，操作の対象の key となる varn と +node のkeyを比較を行う． +そこからは本来の木構造と同じで，操作の対象の key が小さいなら +left の tree を次の node として遷移する． +大きいなら right の tree を次の node として遷移していく． -操作の対象となる node に辿り着き、操作を行った後、 -Stack に持っている tree から再構築を行う。 +操作の対象となる node に辿り着き，操作を行った後， +Stack に持っている tree から再構築を行う． そのコードが Code \ref{bt_replace_impl} となる \lstinputlisting[label=bt_replace_impl, caption=Stack から tree を再構築する Code Gear] {src/bt_impl/replace.agda.replaced} -これも Code \ref{bt_find_impl} と同じように構成されており、 -varn と node の key を比較し、 vart を List から持ってきた node の どこに加えるかを決めるようになっている。 +これも Code \ref{bt_find_impl} と同じように構成されており， +varn と node の key を比較し， vart を List から持ってきた node の どこに加えるかを決めるようになっている． -以上の流れを繋げることで、 Binary Tree の insert と find を実装できた。 -delete は insert の値を消すようにすると実装ができる。 +以上の流れを繋げることで， Binary Tree の insert と find を実装できた． +delete は insert の値を消すようにすると実装ができる． \section{Gears Agda における Binary Tree の検証} -検証も前述した While Loop の 検証と同じようにしていく。 -しかし、 Binary Tree の不変条件は2つ以上あるため、これを関数定義の際に全て書くと -煩雑になってしまうため、事前に記述して関数化しておく。 -それが Code \ref{bt_invariant} になる。 +検証も前述した While Loop の 検証と同じようにしていく． +しかし， Binary Tree の不変条件は2つ以上あるため，これを関数定義の際に全て書くと +煩雑になってしまうため，事前に記述して関数化しておく． +それが Code \ref{bt_invariant} になる． \lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/invariant.agda.replaced} -この不変条件は、 treeInvariant が tree の 左にある node の key が小さく、 -右にある node の方が大きいことを条件としている。 +この不変条件は， treeInvariant が tree の 左にある node の key が小さく， +右にある node の方が大きいことを条件としている． -stackInvariant は Stack にある tree が、次に取り出す Tree の一部であることを -条件としている。 +stackInvariant は Stack にある tree が，次に取り出す Tree の一部であることを +条件としている． -これを先ほど実装した Code Gear に対して加えることで検証していく。 -先ほど実装した Code \ref{bt_find_impl} に対して加えると Code ref のようになる。 +これを先ほど実装した Code Gear に対して加えることで検証していく． +先ほど実装した Code \ref{bt_find_impl} に対して加えると Code ref のようになる． \lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/find.agda.replaced} 現時点では条件を満たしていることの証明まで行っていないが -コード中の {!!} に記述を行い、前述した While Loop と同じように中身を記述することで検証を行える。 +コード中の {!!} に記述を行い，前述した While Loop と同じように中身を記述することで検証を行える． \section{まとめと今後の課題} -本論文では、Gears Agda にて Hoare Logic を用いて While Loop の検証を行えた。 -これはプログラムが Code Gear という単位で分かれているため、 -一つ一つの Code Gear に対して検証を行いながら実装を行っていくことも可能である。 -そのため、従来の検証手法よりもスコープが小さく、簡単に検証と実装を行えると考える。 +本論文では，Gears Agda にて Hoare Logic を用いて While Loop の検証を行えた． +これはプログラムが Code Gear という単位で分かれているため， +一つ一つの Code Gear に対して検証を行いながら実装を行っていくことも可能である． +そのため，従来の検証手法よりもスコープが小さく，簡単に検証と実装を行えると考える． -今後の課題として、Gears Agda による Red Black Tree の実装と検証を行う必要がある。 -While Loop と同じように検証を行えると考えているが、研究目的である -「ループが存在し、かつ再代入がプログラムに含まれるデータ構造」を -Gaers Agda を実装することが難しく、それをさらに検証しなければならない。 +今後の課題として，Gears Agda による Red Black Tree の実装と検証を行う必要がある． +While Loop と同じように検証を行えると考えているが，研究目的である +「ループが存在し，かつ再代入がプログラムに含まれるデータ構造」を +Gaers Agda を実装することが難しく，それをさらに検証しなければならない．
--- a/Paper/tex/while_loop.tex Thu May 05 17:38:06 2022 +0900 +++ b/Paper/tex/while_loop.tex Thu May 05 22:32:45 2022 +0900 @@ -1,68 +1,68 @@ \section{Gears Agda にて Hoare Logic を用いた検証の例} -ここでは Gears Agda にて Hoare Logic を用いた検証の例として、 - While Loop プログラムを実装・検証する。 +ここでは Gears Agda にて Hoare Logic を用いた検証の例として， + While Loop プログラムを実装・検証する． \subsection{While Loop の実装} -まずは前述した Gears Agda の記述形式に基づいて While Loop を実装する。 -実装はまず、 Code \ref{while-loop-dg} のように Code Gear に遷移させる Data Gear の定義から行う。 +まずは前述した Gears Agda の記述形式に基づいて While Loop を実装する． +実装はまず， Code \ref{while-loop-dg} のように Code Gear に遷移させる Data Gear の定義から行う． \lstinputlisting[label=while-loop-dg, caption=Data Gearの定義] {src/while_loop_impl/while_loop_dg.agda.replaced} -そのため最初の Code Gear は引数を受け取り、Envを作成する Code Gear となる Code \ref{while_init_cg}。 +そのため最初の Code Gear は引数を受け取り，Envを作成する Code Gear となる Code \ref{while_init_cg}． \lstinputlisting[label=while_init_cg, caption=Data Gear の定義を行う Code Gear] {src/while_loop_impl/init_cg.agda.replaced} -次に、目的である While Loop の実装を行う。ソースコードは Code \ref{while-loop} のようになる。 +次に，目的である While Loop の実装を行う．ソースコードは Code \ref{while-loop} のようになる． \lstinputlisting[label=while-loop, caption=Loop の部分を担う Code Gears] {src/while_loop_impl/while_loop.agda.replaced} -また Agda では停止性の検出機能が存在し、 -プログラム中 に停止しない記述が存在するとコンパイル時にエラーが出る。 +また Agda では停止性の検出機能が存在し， +プログラム中 に停止しない記述が存在するとコンパイル時にエラーが出る． その場合は関数定義の直前に \{-$\#$ TERMINATING $\#$-\} のタグを付けると 停止しないプログラムをコンパイルすることができる -これまでの Code Gear を繋げることで、 While Loop を行う Code を実装することができる。 +これまでの Code Gear を繋げることで， While Loop を行う Code を実装することができる． \lstinputlisting[label=while-loop, caption=While Loop を行う Code Gear] {src/while_loop_impl/while_loop_c.agda.replaced} \subsection{While Loop の検証} -Gears Agda にて行なった While Loop の実装コードを元に、 +Gears Agda にて行なった While Loop の実装コードを元に， 5章にて述べた Pre / Post Condition を記述していくことで -Hoare Logic を用いた検証を行う。 +Hoare Logic を用いた検証を行う． -検証を行う Code Gear も Gears Agda による単純な実装と同じく Data Gear の定義から行う。Code \ref{while_verif_init_cg} がそれに当たる。 +検証を行う Code Gear も Gears Agda による単純な実装と同じく Data Gear の定義から行う．Code \ref{while_verif_init_cg} がそれに当たる． \lstinputlisting[label=while_verif_init_cg, caption=While Loop を行う Code Gear] {src/while_loop_verif/init_cg.agda.replaced} -今回は検証を行いたいため 5.1 で述べたように、実装に加えて Pre / Post Condition を持つ必要がある。 -init時の Pre Condition のみ特殊で Agda での関数定義の際に記述し、 -「Data Gear に正しく初期値が設定される」という条件を使用する。これが +今回は検証を行いたいため 5.1 で述べたように，実装に加えて Pre / Post Condition を持つ必要がある． +init時の Pre Condition のみ特殊で Agda での関数定義の際に記述し， +「Data Gear に正しく初期値が設定される」という条件を使用する．これが ((vari env) $\equiv$ 0) $\wedge$ ((varn env) $\equiv$ c10) -に当たる。 -そしてinit時以外の、Pre Condition と Post Condition には実行開始から実行終了までの間で不変の条件を記述する。 -今回は While Loop の不変条件として、 +に当たる． +そしてinit時以外の，Pre Condition と Post Condition には実行開始から実行終了までの間で不変の条件を記述する． +今回は While Loop の不変条件として， $今回loopさせたい回数(c10) = 残りのloopする回数(vern) + 今回loopした回数(vari)$ -を設定した。これがinit時の Post Condition となる。 +を設定した．これがinit時の Post Condition となる． -また、init時の Pre Condition と同じ値で -Post Condition を設定しなければならない。 -init時の Pre Condition を Post Condition に変換する Code \ref{conversion} を記載する。 +また，init時の Pre Condition と同じ値で +Post Condition を設定しなければならない． +init時の Pre Condition を Post Condition に変換する Code \ref{conversion} を記載する． \lstinputlisting[label=conversion, caption=init時の Pre Condition を Post Condition に変換する Code Gear] {src/while_loop_verif/conversion.agda.replaced} -ここで変換されて作成された Post Condition はプログラム実行中の不変条件となるため、 -この後の Pre / Post Condition は停止するまでこれを用いる。 +ここで変換されて作成された Post Condition はプログラム実行中の不変条件となるため， +この後の Pre / Post Condition は停止するまでこれを用いる． -以下の Code \ref{loop_verif_cg} は停止性の検証を行っていないが、 Wile Loop の Loop 部分の検証を行う Code Gear となる。 +以下の Code \ref{loop_verif_cg} は停止性の検証を行っていないが， Wile Loop の Loop 部分の検証を行う Code Gear となる． \lstinputlisting[label=loop_verif_cg, caption=停止性以外の Loop の検証も行う Code Gear] {src/while_loop_verif/while_loop.agda.replaced} -Loop が停止することを示していないため、関数定義の直前に \{-\# TERMINATING \#-\} が記述されている。 -こちらも Loop の実装以外に、Pre / Post Condition を満たしているか検証を行い、次の Code Gear に渡している。 +Loop が停止することを示していないため，関数定義の直前に \{-\# TERMINATING \#-\} が記述されている． +こちらも Loop の実装以外に，Pre / Post Condition を満たしているか検証を行い，次の Code Gear に渡している． -ここまでで定義した Pre / Post Consition が付いている Code Gear を繋げることで、 -停止性以外の While Loop の検証を行う Code Gear を実装できる。 +ここまでで定義した Pre / Post Consition が付いている Code Gear を繋げることで， +停止性以外の While Loop の検証を行う Code Gear を実装できる． \lstinputlisting[label=loop_verif_cg, caption=停止性以外の While Loop の検証を行う Code Gear] {src/while_loop_verif/verif_term.agda.replaced} @@ -70,14 +70,14 @@ \lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う Loop 部分の Code Gear] {src/while_loop_verif/verif_loop.agda.replaced} -停止することを Agda が理解できるように記述すると良い。 -そのため引数に減少していく変数 reduce を追加し、 -loop するとデクリメントするように実装する。 +停止することを Agda が理解できるように記述すると良い． +そのため引数に減少していく変数 reduce を追加し， +loop するとデクリメントするように実装する． loop には先ほど実装した loop の部分を担う Code Gear が次の関数遷移先を引数に受け取れるようにした -whileLoopSeg を使用する。 +whileLoopSeg を使用する． -そしてこれらを繋げて While Loop の検証を行うことができる Code ref を実装できた。 +そしてこれらを繋げて While Loop の検証を行うことができる Code ref を実装できた． \lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う While Loop の Code Gear] {src/while_loop_verif/verif.agda.replaced}