# HG changeset patch # User ryokka # Date 1519115601 -32400 # Node ID 50a27cc71ca72ceb472e9cb5fc2e76afd117b2a0 # Parent c8bfe73b2faf5024d9c8f7d194cc1c6a26d23c48 fix final_pre. diff -r c8bfe73b2faf -r 50a27cc71ca7 final_main/chapter1.tex --- a/final_main/chapter1.tex Tue Feb 20 17:06:05 2018 +0900 +++ b/final_main/chapter1.tex Tue Feb 20 17:33:21 2018 +0900 @@ -1,4 +1,4 @@ -\chapter{A} +\chapter{ソフトウェアの信頼性の保証} \label{chap:introduction} \pagenumbering{arabic} diff -r c8bfe73b2faf -r 50a27cc71ca7 final_pre/finalPre.aux --- a/final_pre/finalPre.aux Tue Feb 20 17:06:05 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -\relax -\@writefile{toc}{\contentsline {section}{\numberline {1}ソフトウェアの信頼性の保証}{1}} -\@writefile{toc}{\contentsline {section}{\numberline {2}Countinuation based C (CbC)}{1}} -\newlabel{src:goto}{{1}{1}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}CbCコードの例}{1}} -\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces ソースコード1\relax の流れ}}{1}} -\newlabel{fig:code_simple}{{1}{1}} -\@writefile{toc}{\contentsline {section}{\numberline {3}CbC における Interface の定義}{1}} -\citation{agda} -\newlabel{src:interface}{{2}{2}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}CbCでのStack-Interfaceの実装}{2}} -\@writefile{toc}{\contentsline {section}{\numberline {4}Agda}{2}} -\newlabel{src:agda-css}{{3}{2}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {3}Agda における CodeSegment の定義}{2}} -\@writefile{toc}{\contentsline {section}{\numberline {5}Agda における Interface の定義、実装}{2}} -\newlabel{src:agda-interface}{{4}{2}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}Agda における Stack -Interface の定義の一部}{2}} -\newlabel{src:agda-single-linked-stack}{{5}{2}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}Agda における Stack -Interface の実装の一部}{2}} -\@writefile{toc}{\contentsline {section}{\numberline {6}Agda による Interface 部分を含めた Stack の部分的な証明}{2}} -\newlabel{src:agda-in-some-state}{{6}{2}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {6}抽象的なStackの定義とpush$->$push$->$pop2 の証明}{2}} -\citation{*} -\bibstyle{junsrt} -\bibdata{reference} -\bibcite{agda}{1} -\bibcite{Yasutaka:2016}{2} -\bibcite{Tatsuki:2016}{3} -\bibcite{kaito:2015}{4} -\bibcite{agda-documentation}{5} -\@writefile{toc}{\contentsline {section}{\numberline {7}まとめ}{3}} diff -r c8bfe73b2faf -r 50a27cc71ca7 final_pre/finalPre.bbl --- a/final_pre/finalPre.bbl Tue Feb 20 17:06:05 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ -\begin{thebibliography}{1} - -\bibitem{agda} -The agda wiki. -\newblock \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. -\newblock Accessed: 2017/10/24(Tue). - -\bibitem{Yasutaka:2016} -{比嘉 健太, 河野 真治}. -\newblock {メタ計算を用いた Continuation based C の検証手法}, 2016. - -\bibitem{Tatsuki:2016} -{伊波 立樹, 東恩納 琢偉, 河野 真治}. -\newblock {Code Gear 、Data Gear に基づく OS のプロトタイプ}, 2016. - -\bibitem{kaito:2015} -{徳森 海斗, 河野 真治}. -\newblock {LLVM Clang 上の Continuation based C コンパイラ の改良}, 2015. - -\bibitem{agda-documentation} -Welcome to agda’s documentation! ― agda 2.6.0 documentation. -\newblock \url{http://agda.readthedocs.io/en/latest/index.html}. -\newblock Accessed: 2017/10/24(Tue). - -\end{thebibliography} diff -r c8bfe73b2faf -r 50a27cc71ca7 final_pre/finalPre.blg --- a/final_pre/finalPre.blg Tue Feb 20 17:06:05 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -This is pBibTeX, Version 0.99d-j0.33 (utf8.euc) (TeX Live 2016) -Capacity: max_strings=35307, hash_size=35307, hash_prime=30011 -The top-level auxiliary file: finalPre.aux -The style file: junsrt.bst -Database file #1: reference.bib -You've used 5 entries, - 2270 wiz_defined-function locations, - 561 strings with 4743 characters, -and the built_in function-call counts, 806 in all, are: -= -- 44 -> -- 14 -< -- 0 -+ -- 8 -- -- 3 -* -- 5 -:= -- 87 -add.period$ -- 12 -call.type$ -- 5 -change.case$ -- 5 -chr.to.int$ -- 0 -cite$ -- 5 -duplicate$ -- 55 -empty$ -- 121 -format.name$ -- 6 -if$ -- 201 -int.to.chr$ -- 0 -int.to.str$ -- 5 -missing$ -- 0 -newline$ -- 25 -num.names$ -- 3 -pop$ -- 63 -preamble$ -- 1 -purify$ -- 0 -quote$ -- 0 -skip$ -- 47 -stack$ -- 0 -substring$ -- 0 -swap$ -- 5 -text.length$ -- 0 -text.prefix$ -- 0 -top$ -- 0 -type$ -- 0 -warning$ -- 0 -while$ -- 3 -width$ -- 6 -write$ -- 44 -is.kanji.str$ -- 33 diff -r c8bfe73b2faf -r 50a27cc71ca7 final_pre/finalPre.dvi Binary file final_pre/finalPre.dvi has changed diff -r c8bfe73b2faf -r 50a27cc71ca7 final_pre/finalPre.log --- a/final_pre/finalPre.log Tue Feb 20 17:06:05 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,281 +0,0 @@ -This is e-pTeX, Version 3.14159265-p3.7-160201-2.6 (utf8.euc) (TeX Live 2016) (preloaded format=platex 2017.4.13) 20 FEB 2018 17:04 -entering extended mode - restricted \write18 enabled. - %&-line parsing enabled. -**finalPre.tex -(./finalPre.tex -pLaTeX2e <2016/05/07> (based on LaTeX2e <2016/03/31>) -Babel <3.9r> and hyphenation patterns for 83 language(s) loaded. -(/usr/local/texlive/2016/texmf-dist/tex/platex/base/jarticle.cls -Document Class: jarticle 2006/06/27 v1.6 Standard pLaTeX class -\c@@paper=\count81 -(/usr/local/texlive/2016/texmf-dist/tex/platex/base/jsize10.clo -File: jsize10.clo 2006/06/27 v1.6 Standard pLaTeX file (size option) -) -\c@part=\count82 -\c@section=\count83 -\c@subsection=\count84 -\c@subsubsection=\count85 -\c@paragraph=\count86 -\c@subparagraph=\count87 -\c@figure=\count88 -\c@table=\count89 -\abovecaptionskip=\skip41 -\belowcaptionskip=\skip42 -\symmincho=\mathgroup4 -LaTeX Font Info: Overwriting symbol font `mincho' in version `bold' -(Font) JY1/mc/m/n --> JY1/gt/m/n on input line 593. -\toclineskip=\dimen118 -\@lnumwidth=\dimen119 -\bibindent=\dimen120 -\heisei=\count90 -) -(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphicx.sty -Package: graphicx 2014/10/28 v1.0g Enhanced LaTeX Graphics (DPC,SPQR) - -(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/keyval.sty -Package: keyval 2014/10/28 v1.15 key=value parser (DPC) -\KV@toks@=\toks15 -) -(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphics.sty -Package: graphics 2016/05/09 v1.0r Standard LaTeX Graphics (DPC,SPQR) - -(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/trig.sty -Package: trig 2016/01/03 v1.10 sin cos tan (DPC) -) -(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/graphics.cfg -File: graphics.cfg 2016/01/02 v1.10 sample graphics configuration -) -Package graphics Info: Driver file: dvipdfmx.def on input line 96. - -(/usr/local/texlive/2016/texmf-dist/tex/latex/dvipdfmx-def/dvipdfmx.def -File: dvipdfmx.def 2016/04/06 v4.08 LaTeX color/graphics driver for dvipdfmx (T -eX Live/ChoF) - -(/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/infwarerr.sty -Package: infwarerr 2016/05/16 v1.4 Providing info/warning/error messages (HO) -) -(/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ltxcmds.sty -Package: ltxcmds 2016/05/16 v1.23 LaTeX kernel commands for general use (HO) -))) -\Gin@req@height=\dimen121 -\Gin@req@width=\dimen122 -) -(./picins.sty Option `picins' Version 3.0 Sep. 1992, TH Darmstadt/HRZ -\@BILD=\box41 -\@TEXT=\box42 -\d@breite=\dimen123 -\d@hoehe=\dimen124 -\d@xoff=\dimen125 -\d@yoff=\dimen126 -\d@shad=\dimen127 -\d@dash=\dimen128 -\d@boxl=\dimen129 -\d@pichskip=\dimen130 -\d@tmp=\dimen131 -\d@tmpa=\dimen132 -\d@bskip=\dimen133 -\hsiz@=\dimen134 -\p@getot@l=\dimen135 -\c@breite=\count91 -\c@hoehe=\count92 -\c@xoff=\count93 -\c@yoff=\count94 -\c@pos=\count95 -\c@shad=\count96 -\c@dash=\count97 -\c@boxl=\count98 -\c@zeilen=\count99 -\@changemode=\count100 -\c@piccaption=\count101 -\c@piccaptionpos=\count102 -\c@picpos=\count103 -\c@whole=\count104 -\c@half=\count105 -\c@tmp=\count106 -\c@tmpa=\count107 -\c@tmpb=\count108 -\c@tmpc=\count109 -\c@tmpd=\count110 -\d@leftskip=\skip43 -\ptoti=\dimen136 -\ptotii=\dimen137 -\env@box=\box43 -\d@envdp=\dimen138 -\c@hsize=\count111 -\c@envdp=\count112 -\d@envb=\dimen139 -) -(./fancyhdr.sty -Package: fancyhdr 2017/06/30 v3.9a Extensive control of page headers and footer -s -\f@nch@headwidth=\skip44 -\f@nch@O@elh=\skip45 -\f@nch@O@erh=\skip46 -\f@nch@O@olh=\skip47 -\f@nch@O@orh=\skip48 -\f@nch@O@elf=\skip49 -\f@nch@O@erf=\skip50 -\f@nch@O@olf=\skip51 -\f@nch@O@orf=\skip52 -) -(/usr/local/texlive/2016/texmf-dist/tex/latex/abstract/abstract.sty -Package: abstract 2009/06/08 v1.2a configurable abstracts -\abstitleskip=\skip53 -\absleftindent=\skip54 -\absrightindent=\skip55 -\absparindent=\skip56 -\absparsep=\skip57 -) -(/usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty -\Urlmuskip=\muskip10 -Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc. -) (./bussproofs.sty -Proof Tree (bussproofs) style macros. Version 1.1. -\theLevel=\count113 -\myMaxLevel=\count114 -\myBoxA=\box44 -\myBoxB=\box45 -\myBoxC=\box46 -\myBoxD=\box47 -\myBoxLL=\box48 -\myBoxRL=\box49 -\thisAboveSkip=\dimen140 -\thisBelowSkip=\dimen141 -\newScoreStart=\dimen142 -\newScoreEnd=\dimen143 -\newCenter=\dimen144 -\displace=\dimen145 -\leftLowerAmt=\dimen146 -\rightLowerAmt=\dimen147 -\scoreHeight=\dimen148 -\scoreDepth=\dimen149 -\htLbox=\dimen150 -\htRbox=\dimen151 -\htRRbox=\dimen152 -\htRRRbox=\dimen153 -\htAbox=\dimen154 -\htCbox=\dimen155 -) (/usr/local/texlive/2016/texmf-dist/tex/latex/listings/listings.sty -\lst@mode=\count115 -\lst@gtempboxa=\box50 -\lst@token=\toks16 -\lst@length=\count116 -\lst@currlwidth=\dimen156 -\lst@column=\count117 -\lst@pos=\count118 -\lst@lostspace=\dimen157 -\lst@width=\dimen158 -\lst@newlines=\count119 -\lst@lineno=\count120 -\lst@maxwidth=\dimen159 - -(/usr/local/texlive/2016/texmf-dist/tex/latex/listings/lstmisc.sty -File: lstmisc.sty 2015/06/04 1.6 (Carsten Heinz) -\c@lstnumber=\count121 -\lst@skipnumbers=\count122 -\lst@framebox=\box51 -) -(/usr/local/texlive/2016/texmf-dist/tex/latex/listings/listings.cfg -File: listings.cfg 2015/06/04 1.6 listings configuration -)) -Package: listings 2015/06/04 1.6 (Carsten Heinz) - -(./jlisting.sty -Package: jlisting 2006/02/20 0.2 (Thor) -\lst@nextchar=\count123 -\lst@inputfile=\read1 -) (./dummy.tex) - -LaTeX Warning: Unused global option(s): - [9.5pt]. - -(./finalPre.aux) -\openout1 = `finalPre.aux'. - -LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 41. -LaTeX Font Info: ... okay on input line 41. -LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 41. -LaTeX Font Info: ... okay on input line 41. -LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 41. -LaTeX Font Info: ... okay on input line 41. -LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 41. -LaTeX Font Info: ... okay on input line 41. -LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 41. -LaTeX Font Info: ... okay on input line 41. -LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 41. -LaTeX Font Info: ... okay on input line 41. -LaTeX Font Info: Checking defaults for JY1/mc/m/n on input line 41. -LaTeX Font Info: ... okay on input line 41. -LaTeX Font Info: Checking defaults for JT1/mc/m/n on input line 41. -LaTeX Font Info: ... okay on input line 41. -\c@lstlisting=\count124 -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <12> on input line 99. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <8> on input line 99. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <6> on input line 99. -LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <9> not available -(Font) Font shape `JT1/gt/m/n' tried instead on input line 99. -LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <9> not available -(Font) Font shape `JY1/gt/m/n' tried instead on input line 99. -LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <14.4> not available -(Font) Font shape `JT1/gt/m/n' tried instead on input line 109. -LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <14.4> not available -(Font) Font shape `JY1/gt/m/n' tried instead on input line 109. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <7> on input line 137. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <5> on input line 137. -LaTeX Font Info: Try loading font information for OMS+cmr on input line 143. - - (/usr/local/texlive/2016/texmf-dist/tex/latex/base/omscmr.fd -File: omscmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions -) -LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <10> not available -(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 143. -File: fig/codesegment.pdf Graphic file (type pdf) - - - -LaTeX Warning: File `../pic/emblem-bitmap.pdf' not found on input line 164. - -File: ../pic/emblem-bitmap.pdf Graphic file (type pdf) -<../pic/emblem-bitmap.pdf> - -Package Fancyhdr Warning: \headheight is too small (0.0pt): - Make it at least 20.37784pt. - We now make it that large for the rest of the document. - This may cause the page layout to be inconsistent, however. - -[1 - - -] -LaTeX Font Info: Try loading font information for OML+cmr on input line 164. - - (/usr/local/texlive/2016/texmf-dist/tex/latex/base/omlcmr.fd -File: omlcmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions -) -LaTeX Font Info: Font shape `OML/cmr/m/n' in size <10> not available -(Font) Font shape `OML/cmm/m/it' tried instead on input line 164. - -Underfull \hbox (badness 10000) in paragraph at lines 224--224 -[]\JY1/mc/m/n/10 ソ ースコ ード \OT1/cmr/m/n/10 6: \JY1/mc/m/n/10 抽象的な \OT1 -/cmr/m/n/10 Stack \JY1/mc/m/n/10 の定義と - [] - -[2] (./finalPre.bbl) [3 - -] (./finalPre.aux) ) -Here is how much of TeX's memory you used: - 2664 strings out of 493693 - 35780 string characters out of 6149787 - 358088 words of memory out of 5000000 - 6201 multiletter control sequences out of 15000+600000 - 14789 words of font info for 58 fonts, out of 8000000 for 9000 - 929 hyphenation exceptions out of 8191 - 27i,15n,43p,299b,1499s stack positions out of 5000i,500n,10000p,200000b,80000s - -Output written on finalPre.dvi (3 pages, 25448 bytes). diff -r c8bfe73b2faf -r 50a27cc71ca7 final_pre/finalPre.pdf Binary file final_pre/finalPre.pdf has changed diff -r c8bfe73b2faf -r 50a27cc71ca7 final_pre/finalPre.tex --- a/final_pre/finalPre.tex Tue Feb 20 17:06:05 2018 +0900 +++ b/final_pre/finalPre.tex Tue Feb 20 17:33:21 2018 +0900 @@ -118,9 +118,10 @@ CbC では通常の計算とメタ計算を分けて記述している。 しかし、CodeGear で DataGear を扱う際、 Context と呼ばれる CodeGear、 DataGear の リスト等を持っている Meta DataGear を経由する。 -通常の CodeGear から Context を直接扱えるようにするのは信頼性を損なう。そのため、 CbC -では Context を通して、次の CodeGear に接続する MetaCodeGear である stub -CodeGear を定義している。 +通常の CodeGear から Meta DataGear である Context を直接扱えると、ユーザーがメタ +計算をノーマルレベルで自由に記述できてしまい、信頼性を損なう。そのため、 CbC +では Context を通して、次の CodeGear に接続する Meta CodeGear である stub + CodeGear を定義している。 CbC で実装していくにつれて特殊な stub CodeGear の記述が複雑になった。 そこで既存の実装をモジュールとして扱うために Interface という仕組みを導入した。 @@ -137,7 +138,8 @@ CodeGear は関数定義の先頭に $\_\_code$ をつけて定義する。 CodeGear は処理の単位でそれらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。 DataGear は CodeGear が扱うデータの単位であり、処理に必要なデータが全て入っている。次の CodeGear に処理を移す際は、 goto の後に CodeGear 名と DataGear を指定する。 -CbC ではこの継続処理がメタ計算として定義されており、 CodeGear に変更なく検証等を行うことができる。 +CbC ではこの継続処理がメタ計算として定義されており、通常計算である CodeGear を変 +更することなく検証や資源管理等の記述を行うことができる。 例として CbC の簡単な例(ソースコード\ref{src:goto})と、流れ\ref{fig:code_simple}を示す。 \lstinputlisting[label=src:goto, caption=CbCコードの例]{./src/goto.cbc}