changeset 9:50a27cc71ca7

fix final_pre.
author ryokka
date Tue, 20 Feb 2018 17:33:21 +0900
parents c8bfe73b2faf
children a01801c32db7
files final_main/chapter1.tex final_pre/finalPre.aux final_pre/finalPre.bbl final_pre/finalPre.blg final_pre/finalPre.dvi final_pre/finalPre.log final_pre/finalPre.pdf final_pre/finalPre.tex
diffstat 8 files changed, 7 insertions(+), 389 deletions(-) [+]
line wrap: on
line diff
--- 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}
 
--- 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}}
--- 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}
--- 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
Binary file final_pre/finalPre.dvi has changed
--- 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)
-
-<fig/codesegment.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).
Binary file final_pre/finalPre.pdf has changed
--- 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}