--- a/Paper/paper.log	Thu May 05 21:09:30 2022 +0900
+++ b/Paper/paper.log	Thu May 05 21:15:02 2022 +0900
@@ -1,4 +1,4 @@
-This is e-pTeX, Version 3.141592653-p3.9.0-210218-2.6 (utf8.euc) (TeX Live 2021) (preloaded format=platex 2021.11.27)  5 MAY 2022 21:08
+This is e-pTeX, Version 3.141592653-p3.9.0-210218-2.6 (utf8.euc) (TeX Live 2021) (preloaded format=platex 2021.11.27)  5 MAY 2022 21:14
 entering extended mode
  restricted \write18 enabled.
  %&-line parsing enabled.
@@ -3261,4 +3261,4 @@
  929 hyphenation exceptions out of 8191
  68i,10n,74p,294b,1326s stack positions out of 5000i,500n,10000p,200000b,80000s
 
-Output written on paper.dvi (6 pages, 52556 bytes).
+Output written on paper.dvi (6 pages, 52608 bytes).

Binary file Paper/paper.pdf has changed

Binary file Paper/paper.synctex.gz has changed

--- a/Paper/paper.tex	Thu May 05 21:09:30 2022 +0900
+++ b/Paper/paper.tex	Thu May 05 21:15:02 2022 +0900
@@ -67,7 +67,7 @@
 
 \begin{abstract}
 アプリケーションの信頼性を保証するために，アプリケーションが動作するOSの信頼性を高める必要がある．
-当研究室では，Continuation Based C(CbC)を用い，定理証明やモデル検査による信頼性の保証を目的としたGearsOSを開発している．
+当研究室では，CbC（Continuation Based C）を用い，定理証明やモデル検査による信頼性の保証を目的としたGearsOSを開発している．
 CbCは当研究室で開発しているノーマルレベル，メタレベルの処理を切り分けることができるC言語の下位言語である．
 GearsOSで未実装の機能であるファイルシステムをinodeの仕組みを用いて実装を行う．
 
@@ -102,7 +102,7 @@
 
 当研究室では，信頼性の保証を目的としたGearsOSを開発している．
 GearsOSは，OSの信頼性を定理証明やモデル検査を行うことで保証することを目指している\cite{modelcheck}．
-同じく，当研究室で開発しているプログラム言語であるCbC(Continuation based C)で記述されており，
+同じく，当研究室で開発しているプログラム言語であるCbC（Continuation based C）で記述されており，
 ノーマルレベルとメタレベルを簡単に切り分けることを可能としている．
 そのようにして，CbCでメタレベルの処理を切り出したものに対して，定理証明やモデル検査を行うことで信頼性を保証する．
 
@@ -121,7 +121,7 @@
 
 \section{Continuation based C}
 
-Continuation based C(CbC)\cite{cbcllvm,cbc}は，当研究室で開発しているCの下位言語である．
+Continuation based C（CbC）\cite{cbcllvm,cbc}は，当研究室で開発しているCの下位言語である．
 CbCでは関数の代わりにCodeGearという単位でプログラミングを行う．
 CodeGearは\emph{\_\_code}という記述で宣言することができる．
 また，データの単位にはDataGearと呼ばれる変数データを用いる．
@@ -152,7 +152,7 @@
 GearsOS\cite{gears,gearsos,cr}は当研究室で開発している，信頼性と拡張性の両立を目的としたOSである．
 GearsOSにはGearという概念があり，実行の単位をCodeGear，データの単位をDataGearと呼ぶ．
 軽量継続を基本とし，stackを持たない代わりに全てをContext経由で実行する．
-同様にGearの概念を持つCbC(Continuation based C)で記述されており，ノーマルレベルとメタレベルの処理を切り分けることが容易である．
+同様にGearの概念を持つContinuation based C（CbC）で記述されており，ノーマルレベルとメタレベルの処理を切り分けることが容易である．
 また，GearsOSは現在開発途上であり，OSとして動作するために今後実装しなければならない機能がいくつか残っている．
 
 ContextはGearsOS上全てのCodeGear，DataGearの参照を持ち，CodeGearとDataGearの接続に用いられる．
@@ -164,7 +164,7 @@
 
 図\ref{fig:context}はContextを参照する流れを表したものである．
 まずCodeGearがOutputDataGearへデータをoutputする．
-stubCodeGearはInputDataGear(前のCodeGearのOutputDataGear)とOutputDataGearをContextから参照し，次のCodeGearへgotoを行う．
+stubCodeGearはInputDataGear（前のCodeGearのOutputDataGear）とOutputDataGearをContextから参照し，次のCodeGearへgotoを行う．
 CodeGearでの処理後，OutputDataGearへデータをoutputする．
 
 Contextはいくつかの種類に分けることができる．
@@ -229,10 +229,10 @@
 
 ディレクトリ構造は2つのFileSystemTreeで実装する．
 1つ目はinode numberとfileのポインタのペアを持つ木である．
-それは，inode numberをkey，inodeをvalueとして持つためinode numberからinodeを検索するために用いる(以下，inode treeとする)．
+それは，inode numberをkey，inodeをvalueとして持つためinode numberからinodeを検索するために用いる（以下，inode treeとする）．
 2つ目はfilenameとinode numberのペアを持つ木である．
 それは，filenameをkey, inode numberをvalueとして持つため，filenameからinode numberを検索するために用いる．
-また，inodeをfilenameで検索するためのindex treeであるといえる(以下，index treeとする)．
+また，inodeをfilenameで検索するためのindex treeであるといえる（以下，index treeとする）．
 
 図\ref{fig:inode}はindex treeを用いたinodeの検索の流れを表す．
 まずindex treeからkeyがfilenameのnodeをgetする．