Binary file Paper/master_paper.pdf has changed

--- a/Paper/tex/agda.tex	Thu Feb 02 20:52:51 2023 +0900
+++ b/Paper/tex/agda.tex	Thu Feb 02 21:20:08 2023 +0900
@@ -2,8 +2,8 @@
 Agda \cite{agda-wiki} \cite{Stump:2016:VFP:2841316} は純粋関数型言語である。
 Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。
 
-また、ともとの Agda には自然数などの普遍的な定義すら存在しない。
-その実装ができることも本章で取り扱っているが、般的には agda-standard-libralies \cite{agda-stdlib} を使用する。
+また、もともとの Agda には自然数などの普遍的な定義すら存在しない。
+その実装ができることも本章で取り扱っているが、一般的には agda-standard-libralies \cite{agda-stdlib} を使用する。
 
 本章ではAgdaの基本とAgdaによる定理証明の方法について述べる。
 
@@ -18,7 +18,7 @@
 Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。
 このとき \verb/name/ に 空白があってはいけない。
 データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
-\verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、
+\verb/data/ キーワードの後に \verb/data/ の名前と型を記述、 \verb/where/ 句を書きインデントを深くし、
 値にコンストラクタとその型を列挙する。
 
 \coderef{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)の例である。
@@ -40,14 +40,14 @@
 複数の値を列挙するには \verb/;/ で区切る必要がある。
 
 %% 関数について
-Agda での関数は型の定義と、関数の定義をする必要がある。
-関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが、入力を受け取り出力を返す型として記述される。または $\rightarrow$ を用いて \verb/input → output/ のように記述される。
-また、\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し、中間記法で関数を定義することもできる。
-関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。
+Agda での関数は型の定義と関数の定義をする必要がある。
+関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ と記述するが、入力を受け取り出力を返す型として記述される。または $\rightarrow$ を用いて \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/した値を返す関数は\coderef{agda-function}のように定義できる。
+例として任意の自然数$\mathbb{N}$を受け取り、それに1を加えた値を返す関数は\coderef{agda-function}のように定義できる。
 \lstinputlisting[label=code:agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced}
 
 

--- a/Paper/tex/cbc.tex	Thu Feb 02 20:52:51 2023 +0900
+++ b/Paper/tex/cbc.tex	Thu Feb 02 21:20:08 2023 +0900
@@ -15,36 +15,36 @@
 本章ではCbCの概要について説明する。
 
 \section{CodeGear / DataGear}
-CbCでは,検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いる。
+CbCでは、検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いる。
 
-CodeGear はプログラムの処理そのものであり,一般的なプログラム言語における関数と同じ役割である。
-DataGear は CodeGear で扱うデータの単位であり,処理に必要なデータである。
-CodeGear の入力となる DataGear を Input DataGear と呼び,出力は Output DataGear と呼ぶ。
+CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。
+DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。
+CodeGear の入力となる DataGear を Input DataGear と呼び、出力は Output DataGear と呼ぶ。
 
 CodeGear 間の移動は継続を用いて行われる。
-継続は関数呼び出しとは異なり,呼び出した後に元のコードに戻れず,次の CodeGear へ遷移を行う。
-これは,関数型プログラミングでは末尾再帰をしていることと同義である。
+継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻れず、次の CodeGear へ遷移を行う。
+これは、関数型プログラミングでは末尾再帰をしていることと同義である。
 
 
 \section{CbC と C言語の違い}
-同じ仕様でCbCとC言語で実装した際の違いを,実際のコードを元に比較する。
-比較するにあたり,再起処理が含まれるコードの例として,
+同じ仕様でCbCとC言語で実装した際の違いを、実際のコードを元に比較する。
+比較するにあたり、再起処理が含まれるコードの例として、
 フィボナッチ数列の n 番目を求めるコードを挙げる。
 C言語で記述したものが\coderef{fib_c}になり、CbCで記述したものが\coderef{fib_cbc}になる。
 CbCは実行を継続するため、return を行えない。そのためC言語での実装も return を書
-かず関数呼び出しを行い,最後にexitをして実行終了するように記述している。
+かず関数呼び出しを行い、最後にexitをして実行終了するように記述している。
 
 \lstinputlisting[label=code:fib_c, caption=C言語で記述した フィボナッチ数列の n 番目
 を求めるコード, firstline=5] {src/cbc/fib.c}
 \lstinputlisting[label=code:fib_cbc, caption=CbCで記述した フィボナッチ数列の n 番目
 を求めるコード, firstline=5] {src/cbc/fib.cbc}
 
-軽量実装になっているのか,上記のコードをアセンブラ変換した結果を見て確認する。
-全てを記載すると長くなるので,アセンブラ変換した際のfib関数のみを記載する。
+軽量実装になっているのか、上記のコードをアセンブラ変換した結果を見て確認する。
+全てを記載すると長くなるので、アセンブラ変換した際のfib関数のみを記載する。
 C言語で記述したコードをアセンブラ変換した結果が\coderef{c-ass}。
 CbCで記述したコードをアセンブラ変換した結果が\coderef{cbc-ass}になる。
 
-比較すると,fib 関数の内部で再度 fib 関数を呼び出す際,
+比較すると、fib 関数の内部で再度 fib 関数を呼び出す際、
 C言語で実装した\coderef{c-ass}の30行目では callq で fib 関数を呼び出している。
 対して CbC で実装した\coderef{cbc-ass}の32行目では、jmp により fib 関数に移動
 している。
@@ -57,7 +57,7 @@
 
 \section{Meta CodeGear / Meta DataGear}
 Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub
-CodeGear では Context と呼ばれる接続可能な CodeGear,DataGear のリストや,DataGear
+CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear
 のメモリ空間等を持った Meta DataGear を扱っている。
 
 また、プログラムを記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、資源管理等を記述しなければならない処理が存在する。

--- a/Paper/tex/conclusion.tex	Thu Feb 02 20:52:51 2023 +0900
+++ b/Paper/tex/conclusion.tex	Thu Feb 02 21:20:08 2023 +0900
@@ -1,22 +1,22 @@
 \chapter{まとめと今後の展望}
-本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた。そこで,定理証明については Invariant を用いて定理証明を行った。モデル検査については Gears Agda にて dead lock を検知できるようになった。
+本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた。そこで、定理証明については Invariant を用いて定理証明を行った。モデル検査については Gears Agda にて dead lock を検知できるようになった。
 
-実際に Invariant を用いることで,プログラムに与える入力とその出力に対して条件を与え,Hoare Logic による検証を行えるようになった。
-これにより,いままでより容易に Gears Agda にて検証が進められるようになった。
+実際に Invariant を用いることで、プログラムに与える入力とその出力に対して条件を与え、Hoare Logic による検証を行えるようになった。
+これにより、いままでより容易に Gears Agda にて検証が進められるようになった。
 
-また,先行研究での課題にて,CbCで開発,検証を行いたいと考えている Gears OS\cite{mitsuki-prosym}の並列動作の検証があった。これもモデル検査により,Gears Agda 内で並列動作に対する検証も行えるようになった。
+また、先行研究での課題にて、CbCで開発、検証を行いたいと考えている Gears OS\cite{mitsuki-prosym}の並列動作の検証があった。これもモデル検査により、Gears Agda 内で並列動作に対する検証も行えるようになった。
 
 
 \section{今後の課題}
-今後の課題としてモデル検査による検証,定理証明による検証,Gears Agda の今後の展望について述べる。
-モデル検査においては,有向グラフからなる有限オートマトンの遷移を全自動探索することと,live lockやLTTLも用いたアサーションなどの検証\cite{model}を行いたい。
-加えて,State List のデータ構造を balanced tree にすることで,並列にモデル検査が行えるようになると考えられる。
-これにより,状態が膨大になるモデル検査に対応できる。
+今後の課題としてモデル検査による検証、定理証明による検証、Gears Agda の今後の展望について述べる。
+モデル検査においては、有向グラフからなる有限オートマトンの遷移を全自動探索することと、live lockやLTTLも用いたアサーションなどの検証\cite{model}を行いたい。
+加えて、State List のデータ構造を balanced tree にすることで、並列にモデル検査が行えるようになると考えられる。
+これにより、状態が膨大になるモデル検査に対応できる。
 
-定理証明においては,Red Black Tree の検証を行いたいと思っている。
+定理証明においては、Red Black Tree の検証を行いたいと思っている。
 これで検証を行ったものをモデル検査や Gears OS のファイルシステムなどに転用できると考えている。
 
-Gears Agda の展望について,CbC に変換することが挙げられる。
-CbC はアセンブラに近いため記述が複雑かつ困難であるが,Gears Agda で記述したものを CbC に変換できるようになれば,その点を解決できる。更に,Gears Agda で検証を行ったプログラムであるため,プログラムの信頼性もある。
-加えて,モデル検査の実行には速度が求められるが,CbCで高速に実行できるようになることが期待される。
+Gears Agda の展望について、CbC に変換することが挙げられる。
+CbC はアセンブラに近いため記述が複雑かつ困難であるが、Gears Agda で記述したものを CbC に変換できるようになれば、その点を解決できる。更に、Gears Agda で検証を行ったプログラムであるため、プログラムの信頼性もある。
+加えて、モデル検査の実行には速度が求められるが、CbCで高速に実行できるようになることが期待される。
 

--- a/Paper/tex/dpp_impl.tex	Thu Feb 02 20:52:51 2023 +0900
+++ b/Paper/tex/dpp_impl.tex	Thu Feb 02 21:20:08 2023 +0900
@@ -5,16 +5,16 @@
   \item Gears Agda にて DPP の実装を行う
   \item プログラムが実行中に取りうる状態の網羅をする State List を作成する
   \item 上で実装したものを使用しつつ Meta DataGear を構築する Meta CodeGearを記述する
-  \item 上記 Meta CodeGear で作成された meta data を元に,dead lockを判定する Meta CodeGear を記述する
-  \item 状態を網羅した State List にある State を一つずつ Meta CodeGear に実行させて,dead lockしている状態がないか確認する
+  \item 上記 Meta CodeGear で作成された meta data を元に、dead lockを判定する Meta CodeGear を記述する
+  \item 状態を網羅した State List にある State を一つずつ Meta CodeGear に実行させて、dead lockしている状態がないか確認する
 \end{enumerate}
 
 先行研究では網羅した状態データを State DB に格納していた。しかし今回の Gears Agda では State List にて代替とした。これは List で行った方が Agda での実装がしやすい点にある。本来は branced tree をデータ構造に持って State を作成するほう正しい。
 
-dead lock の定義として,全てのプロセスが他のプロセスの実行終了待ちをしている。かつ新たに状態の分岐が作成できないものとした。
-そこでstep実行してもプロセスがすべて変動がなく,かつStateの分岐が作成されなかったものを dead lock としている。
+dead lock の定義として、全てのプロセスが他のプロセスの実行終了待ちをしている。かつ新たに状態の分岐が作成できないものとした。
+そこでstep実行してもプロセスがすべて変動がなく、かつStateの分岐が作成されなかったものを dead lock としている。
 
-最後について,今回は状態の網羅を一度終了してから dead lock の有無を検証している。しかし,これは今回のプログラムが有限オートマトンであることは事前に明らかであるためにできたことである。検証したいプログラムが無限の状態を作成する場合は,Stateを作成するたびにそれに対して dead lock や live lock などのモデル検査をすることもできる。モデル検査中に意図しない動きがあった場合に停止するようにすることで,無限の状態を作成するプログラムであっても,モデル検査ができると考える。他にも,プログラムが取る状態を制限することで有限な状態を作成するようにし,モデル検査をすることもできる。 (bounded model checking)
+最後について、今回は状態の網羅を一度終了してから dead lock の有無を検証している。しかし、これは今回のプログラムが有限オートマトンであることは事前に明らかであるためにできたことである。検証したいプログラムが無限の状態を作成する場合は、Stateを作成するたびにそれに対して dead lock や live lock などのモデル検査をすることもできる。モデル検査中に意図しない動きがあった場合に停止するようにすることで、無限の状態を作成するプログラムであっても、モデル検査ができると考える。他にも、プログラムが取る状態を制限することで有限な状態を作成するようにし、モデル検査をすることもできる。 (bounded model checking)
 
 \section{Gears Agda によるDPPの実装}
 
@@ -84,9 +84,9 @@
 
 \section{Gears Agda によるDPPの検証}
 
-これまでの実装は一般的なDPPの実装であったため,
+これまでの実装は一般的なDPPの実装であったため、
 Code / DataGear の実装であった。
-ここからは,モデル検査を行うため,Meta DataGear の定義をし,
+ここからは、モデル検査を行うため、Meta DataGear の定義をし、
 それの操作を行う Meta CodeGear の実装を行っていく。
 
 以下\coderef{dpp-mdg}がMeta DataGear の定義になる。
@@ -94,13 +94,13 @@
 % ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける
 \lstinputlisting[caption=Gears Agda で DPP のモデル検査を行うための Meta DataGear, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced}
 
-この Meta DataGear の説明をすると,
+この Meta DataGear の説明をすると、
 metadataは状態の分岐数を持っておくnum-brunchがある。
 MetaEnv はもとの DataGear を保持するDG(DataGearの省略)となる。
-meta には前述したmetadataを持っており,
-他には,deadlockしているかのフラグである deadlock ,
+meta には前述したmetadataを持っており、
+他には、deadlockしているかのフラグである deadlock 、
 最後の2つは後に必要になるフラグである。
-そのstate が step 実行済みなのかのフラグであるis-step,
+そのstate が step 実行済みなのかのフラグであるis-step、
 そのstateがモデル検査済なのかのフラグであるis-doneフラグを持っている。
 
 MetaEnv2 は1つのstate である MetaEnv の Listを metal で持てる。
@@ -119,85 +119,85 @@
 \lstinputlisting[caption=状態の分岐数をカウントする Meta DataGear の定義, label=code:dpp-mcg-branch]{src/dpp-verif/dpp-metacode.agda.replaced}
 
 
-実際にやっていることは,MetaEnv2 から state を取り出し,分岐を見る関数に遷移させている。その結果の List の length を meta データとしている。
+実際にやっていることは、MetaEnv2 から state を取り出し、分岐を見る関数に遷移させている。その結果の List の length を meta データとしている。
 
-つまり,この Meta CodeGear の実装にあたって新しい実装はほとんど行っていない。
+つまり、この Meta CodeGear の実装にあたって新しい実装はほとんど行っていない。
 
-Wait List の 作成も同じように取り出した state を step させて,そこで一致するnext-codeを状態が変わっていないとして Wait List に入れている。
+Wait List の 作成も同じように取り出した state を step させて、そこで一致するnext-codeを状態が変わっていないとして Wait List に入れている。
 
 %いちおうコード載せようかな？←棄却されました%
 
-Wait List について,Thinking と Eathing の状態に関しては状態が変わる可能性がある。
-これを Wait List に入れなければ Wait List のみで dead lock が検知できると考えられる。しかし,DPP以外の他のプログラムをモデル検査する際に,一つ一つ next-code の設定を行うのは煩雑であると考えた。そのため,step した際に状態が変化しないものを Wait List にいれた。これと分岐がない場合という条件にて,dead lock を検知する。これにより Meta CodeGear の作成が簡易化された。そのため,Thinking と Eathing のプロセスも Waithing List に入るようになっている。
+Wait List について、Thinking と Eathing の状態に関しては状態が変わる可能性がある。
+これを Wait List に入れなければ Wait List のみで dead lock が検知できると考えられる。しかし、DPP以外の他のプログラムをモデル検査する際に、一つ一つ next-code の設定を行うのは煩雑であると考えた。そのため、step した際に状態が変化しないものを Wait List にいれた。これと分岐がない場合という条件にて、dead lock を検知する。これにより Meta CodeGear の作成が簡易化された。そのため、Thinking と Eathing のプロセスも Waithing List に入るようになっている。
 
-deadlockの検出方法として,上記の2つのMeta CodeGear で作成したmeta データを使用する。
+deadlockの検出方法として、上記の2つのMeta CodeGear で作成したmeta データを使用する。
 
-そして「num-brunchの値が1であり,wait Listの数がプロセス数と一致する」ということは,「その状態から別の状態に遷移することができない」として,この状態をdead lockであると定義した。
+そして「num-brunchの値が1であり、wait Listの数がプロセス数と一致する」ということは、「その状態から別の状態に遷移することができない」として、この状態をdead lockであると定義した。
 
 以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる。
 
-複雑なことは何もしておらず,単純にstate毎のnum-brunchの値を見て,wait-listの数がプロセス数と一致していた場合に
-deadlockのフラグを立ち上げている。これが,Gears Agda におけるアサーションになっている。
+複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て、wait-listの数がプロセス数と一致していた場合に
+deadlockのフラグを立ち上げている。これが、Gears Agda におけるアサーションになっている。
 
 % judge-dead-lock-pのソースコードを貼り付ける
 \lstinputlisting[caption=DPP での dead lock を検知する Meta CodeGear, label=code:dpp-judge-mcg]{src/dpp-verif/judge-deadlock.agda.replaced}
 % こいつはmetaEnv2を受け取れるように変えないと行けない
 
-ここから前述した通り,State Listを作成する。
+ここから前述した通り、State Listを作成する。
 
 そのまま実行するだけでは無限に実行されるのみで停止しないと思われる。
-しかし,分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる。
-存在していた場合はそれを追加せず,存在しなかった場合にのみ State を追加する。
+しかし、分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる。
+存在していた場合はそれを追加せず、存在しなかった場合にのみ State を追加する。
 
-Agdaには2つの record が等しいか確かめる関数などは存在せず,
+Agdaには2つの record が等しいか確かめる関数などは存在せず、
 \coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つずつ一致しているか確認する。
-こちらはそのまま掲載すると長いので,実際のコードに手を加えて省略している。実際のコードは付録にて参照できる。
+こちらはそのまま掲載すると長いので、実際のコードに手を加えて省略している。実際のコードは付録にて参照できる。
 
 \lstinputlisting[caption=重複しているstateを除外する Meta CodeGear, label=code:dpp-exclude-state-mcg]{src/dpp-verif/exclude-same-env.agda.replaced}
 % 手を加えているので詳細は付録を参照するように促す
 
-MetaEnv2 を受け取ってその中身の state を比較するが,そこまで展開する必要がある。
- loop-metaenv と loop-target-metaenv, eq-env にてそれを行っている。
+MetaEnv2 を受け取ってその中身の state を比較するが、そこまで展開する必要がある。
+ loop-metaenv と loop-target-metaenv、 eq-env にてそれを行っている。
 
-更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し,次のstateの一致を探索するように記述されている。
+更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し、次のstateの一致を探索するように記述されている。
 
-実際にstateの一致を見ているのは22行目のeq-env関数で,一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている。
+実際にstateの一致を見ているのは22行目のeq-env関数で、一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている。
 
 State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている。
-その値が一致している場合には別の値を見て,一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている。
-他の値である,lhandやrhandなども eq-pid と同じように記述している。
+その値が一致している場合には別の値を見て、一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている。
+他の値である、lhandやrhandなども eq-pid と同じように記述している。
 
 
-これらにて,まだ分岐を見ていない1つのStateの分岐を確かめる。
+これらにて、まだ分岐を見ていない1つのStateの分岐を確かめる。
 発生した分岐を step 実行させる。
 step実行して作成された state が State Listに存在していないかを確かめる。
 これを繰り返すことで State Listを作る。
-State List に存在している全ての state の分岐を見たということは,
+State List に存在している全ての state の分岐を見たということは、
 出現するStateを全て網羅することができたと言える。
 
 あとは State List を dead lock の検査を行う Meta CodeGear に与えるとどの state が dead lockしているかを検証することができる。
 
 \section{Gears Agda による live lockの検証方法について}
-live lockとは,状態が変動しているが,その状態はループしており,実行が進んでいないことを指す。
+live lockとは、状態が変動しているが、その状態はループしており、実行が進んでいないことを指す。
 
-DPPにて例を上げると,(上の哲学者のフローだと) dead lock が発生するため,フローを変更したとする。それは以下のような動作を追加する。
-「右手にフォークを持っているが,左手のフォークがすでに取られている場合に右手のフォークを即座に置いて固定時間待つ」
-とする。これで解決すると思われるが,全員が同時に食事をしようとした場合,右手のフォークを取ったり置いたりを永遠に繰り返すことになる。
+DPPにて例を上げると、(上の哲学者のフローだと) dead lock が発生するため、フローを変更したとする。それは以下のような動作を追加する。
+「右手にフォークを持っているが、左手のフォークがすでに取られている場合に右手のフォークを即座に置いて固定時間待つ」
+とする。これで解決すると思われるが、全員が同時に食事をしようとした場合、右手のフォークを取ったり置いたりを永遠に繰り返すことになる。
 これを live lock という
 
-つまり,この状態を検知するなら,そのstateが持っているhistoryまで考慮する必要がある。つまり,今回の場合だとstateのloopができた際にコマンドが一巡しているかを確認すると良い。
+つまり、この状態を検知するなら、そのstateが持っているhistoryまで考慮する必要がある。つまり、今回の場合だとstateのloopができた際にコマンドが一巡しているかを確認すると良い。
 
-history がloopしていた際に,誰もeathingしていない場合を live lock していると定義する。
+history がloopしていた際に、誰もeathingしていない場合を live lock していると定義する。
 
-今回のはDPPであるためEatingが挙げられているが,他の実装であれば,どのコマンドが実行されるのが正常な動きなのかを決める。それがloop中に存在しているかを確認することで live lock を検知できる。
+今回のはDPPであるためEatingが挙げられているが、他の実装であれば、どのコマンドが実行されるのが正常な動きなのかを決める。それがloop中に存在しているかを確認することで live lock を検知できる。
 
 
 \section{Gears Agda でのモデル検査の評価}
 
-SPINで行ったDPPのモデル検査に比べると,Gears Agdaの方がコードも長く、制約が多いため難解に思える。しかし,Gears Agda ではプログラムの実装も含んでいる。
+SPINで行ったDPPのモデル検査に比べると、Gears Agdaの方がコードも長く、制約が多いため難解に思える。しかし、Gears Agda ではプログラムの実装も含んでいる。
 
-さらに,Gears Agda での実装をしたあとのモデル検査を行う際の Meta CodeGear の流れは変化しないため,他のプログラムに適応できることを考えると比較的容易であると言える。
+さらに、Gears Agda での実装をしたあとのモデル検査を行う際の Meta CodeGear の流れは変化しないため、他のプログラムに適応できることを考えると比較的容易であると言える。
 
-加えて,Gears Agda は CbC へコンパイルされ,高速に実行されることを踏まえると,いかに Gears Agda が検証に向いたプログラムであるか理解できる。
+加えて、Gears Agda は CbC へコンパイルされ、高速に実行されることを踏まえると、いかに Gears Agda が検証に向いたプログラムであるか理解できる。
 
 % この評価の話はまとめでしたほうがいいかもね？

--- a/Paper/tex/hoare.tex	Thu Feb 02 20:52:51 2023 +0900
+++ b/Paper/tex/hoare.tex	Thu Feb 02 21:20:08 2023 +0900
@@ -1,6 +1,6 @@
 \chapter{Gears Agda による定理証明}
-先行研究\cite{ryokka-sigos}では,Gears Agda ではないプログラムの Hoare Logic による検証\cite{agda2-hoare}を参考にそれを Gears Agda に適応して while loop の検証を行っていた\cite{cr-ryukyu}。
-本研究では,Invariant というプログラムの不変条件を定義し,それを検証することで,比較的容易に検証を行うことができるようになった(本章2節)
+先行研究\cite{ryokka-sigos}では、Gears Agda ではないプログラムの Hoare Logic による検証\cite{agda2-hoare}を参考にそれを Gears Agda に適応して while loop の検証を行っていた\cite{cr-ryukyu}。
+本研究では、Invariant というプログラムの不変条件を定義し、それを検証することで、比較的容易に検証を行うことができるようになった(本章2節)
 本章では Gears Agda による定理証明の方法について説明する。
 
 \section{Hoare Logic}

--- a/Paper/tex/intro.tex	Thu Feb 02 20:52:51 2023 +0900
+++ b/Paper/tex/intro.tex	Thu Feb 02 21:20:08 2023 +0900
@@ -1,9 +1,9 @@
 \chapter{Gears Agda でのプログラムの検証}
 
 OSやアプリケーションの信頼性の向上は重要である。
-信頼性を向上するための手段として、ログラムを検証する事が挙げられる。
+信頼性を向上するための手段として、プログラムを検証する事が挙げられる。
 
-しかし、様の形式化とその検証には膨大なコストを要する。
+しかし、仕様の形式化とその検証には膨大なコストを要する。
 そのため、他のプログラミング言語と比べて検証に適している Gears Agda を使用する。
 Gears Agda とは当研究室で開発している Continuation based C \cite{cbc-gcc}(以下CbC) の概念を取り入れた記法で記述された Agda \cite{agda} のことである。
 
@@ -16,12 +16,12 @@
 
 これにより検証を CodeGear 単位に分割することができ、比較的容易に検証を行えるようになっている。
 
-また、先行研究\cite{ryokka-sigos}では、ears Agda での並列実行の検証について課題が残っていた。
-並列実行の検証を定理証明で行うには、慮する状態の数が膨大になり困難である。
-そのため、ears Agda でモデル検査\cite{EdmundM}を行うことでこの課題に対応する。
+また、先行研究\cite{ryokka-sigos}では、Gears Agda での並列実行の検証について課題が残っていた。
+並列実行の検証を定理証明で行うには、考慮する状態の数が膨大になり困難である。
+そのため、Gears Agda でモデル検査\cite{EdmundM}を行うことでこの課題に対応する。
 
 CbCの継続の概念はモデル検査とも相性がよい。\cite{ikkun-master}
 CbCが末尾関数呼び出しであるため CodeGear をそのまま
 モデルの edge として定義することが可能である。
 
-これらのことから、論文では、ears Agda での定理証明とモデル検査について述べる。
\ No newline at end of file
+これらのことから、本論文では、Gears Agda での定理証明とモデル検査について述べる。
\ No newline at end of file

--- a/Paper/tex/spin_dpp.tex	Thu Feb 02 20:52:51 2023 +0900
+++ b/Paper/tex/spin_dpp.tex	Thu Feb 02 21:20:08 2023 +0900
@@ -1,17 +1,17 @@
 \chapter{Gears Agda によるモデル検査}
 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
 できる。しかし、専門的な知識が多く難易度が高いという欠点がある。
-加えて、
+加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、
 並列処理を定理証明するには検証する状態が膨大になり困難である。
-そのため、
+そのため、並列処理はモデル検査にて検証する方が良い。
 
 \section{モデル検査とは}
-モデル検査 (Model Cheking) とは,検証手法のひとつである。
+モデル検査 (Model Cheking) とは、検証手法のひとつである。
 これはプログラムが入力に対して仕様を満たした動作を
 行うことを網羅的に検証することを指す。
-しかし,モデル検査と定理証明を比較した際に、モデル検査は入力が無限になる
+しかし、モデル検査と定理証明を比較した際に、モデル検査は入力が無限になる
 状態爆発が起こり得るという問題がある。
-実際にモデル検査で行うことは,検証したい内容の時相理論式 $\varphi$  を作り,対象のシステムの初期状態 s のモデル M があるとき,M, s が $\varphi$ を満たすかを調べる。
+実際にモデル検査で行うことは、検証したい内容の時相理論式 $\varphi$  を作り、対象のシステムの初期状態 s のモデル M があるとき、M, s が $\varphi$ を満たすかを調べる。
 
 \section{Dining Philosophers Problem}
 今回はモデル検査を行う対象として Dining Philosophers Problem (以下DPP)
@@ -50,20 +50,20 @@
 
 \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
 
-SPIN(Simple Promela INterpreter) \cite{spin}とは一般的にモデル検査に使用されるツールである。これは使用記述言語 PROMELA(Process Meta Language) による記述を元にプログラムが取る状態を網羅し,モデル検査を行うことができる。
+SPIN(Simple Promela INterpreter) \cite{spin}とは一般的にモデル検査に使用されるツールである。これは使用記述言語 PROMELA(Process Meta Language) による記述を元にプログラムが取る状態を網羅し、モデル検査を行うことができる。
 
-今回 Gears Agda でのモデル検査と比較するために,SPINでのDPPプログラムのモデル検査に必要なコードの一部を\coderef{spin-dpp}に載せる。
+今回 Gears Agda でのモデル検査と比較するために、SPINでのDPPプログラムのモデル検査に必要なコードの一部を\coderef{spin-dpp}に載せる。
 
 \lstinputlisting[caption= SPINにてDPPをモデル検査する際のコードの一部 , label=code:spin-dpp]{src/dpp-verif/spin.pml}
 
 コードを簡単に説明する。哲学者がThinkの状態から食事をしようとしだした際の状態の変化が4行目と5行目になっている。
-forkの状態を配列で管理している。0 である状態が誰もそのforkを持っていない状態である。ここでは,5人目の人が右手にあるフォークを取ろうとした際に配列の最初を取ることが5行目に記述されている。
+forkの状態を配列で管理している。0 である状態が誰もそのforkを持っていない状態である。ここでは、5人目の人が右手にあるフォークを取ろうとした際に配列の最初を取ることが5行目に記述されている。
 
 左手のフォークを取る動作も同じように記述する。
-SPINではこのコードを元にプログラムが取りうる状態全てを網羅し,モデル検査を行うことができる。
+SPINではこのコードを元にプログラムが取りうる状態全てを網羅し、モデル検査を行うことができる。
 
 \figref{DPP-model}はこのPromelaから作成された状態遷移図になる。
-SPINではコードからプログラムの状態遷移図を出力することができる他,プログラムのstep実行など幅広くモデル検査を行うことができる。
+SPINではコードからプログラムの状態遷移図を出力することができる他、プログラムのstep実行など幅広くモデル検査を行うことができる。
 
 \begin{figure}[htpb]
     \begin{center}

--- a/Paper/tex/thanks.tex	Thu Feb 02 20:52:51 2023 +0900
+++ b/Paper/tex/thanks.tex	Thu Feb 02 21:20:08 2023 +0900
@@ -1,11 +1,11 @@
 \chapter*{謝辞}
 \addcontentsline{toc}{chapter}{謝辞}
 
-本研究の遂行、
+本研究の遂行、本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に心より感謝致します。
 共に研究を行い暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致します。
 私の研究において苦楽を共にした Manjaro Linux とその開発者には頭が上がりません。
-さらに、 Hally's Cafe に感謝しております。
-最後に、有意義な時間を共に過ごした理工学研究科工学専攻の学友、
+さらに、ゼミの前においしいご飯で元気づけてくれた Hally's Cafe に感謝しております。
+最後に、有意義な時間を共に過ごした理工学研究科工学専攻の学友、並びに物心両面で支えてくれた家族に深く感謝致します。
 
 \begin{flushright}
     2023年 3月 \\ 上地悠斗